Skip to content

Commit 83a1540

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
fix(live-provers): harden T2 installer steps — four known nightly failure modes
1. Isabelle download timeout: add --retry 3 --max-time 600; use `find` to locate the isabelle binary so the symlink survives an Isabelle2025 release. 2. F* broken URL: fstar-linux_x86_64.tar.gz no longer exists at /latest; asset name changed to fstar-v{ver}-Linux-x86_64.tar.gz. Pinned to v2026.04.17; `find` locates fstar.exe regardless of tarball layout. 3. tlapm URL broken: releases/latest has no tlaps-installer-linux-x86_64.sh; actual asset is tlaps-1.5.0-x86_64-linux-gnu-inst.bin (tag 202210041448). Corrected filename, --max-time 120 added, `find` for symlink. 4. apt mirror failures: change all `apt-get update` to `apt-get update -qq || apt-get update -qq --fix-missing`; add `--fix-missing` to all apt-get install calls across T1/T2/T3/guix jobs. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent bc03a78 commit 83a1540

1 file changed

Lines changed: 48 additions & 28 deletions

File tree

‎.github/workflows/live-provers.yml‎

Lines changed: 48 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,10 @@ jobs:
7676
- name: Provision prover (${{ matrix.backend }})
7777
run: |
7878
set -euo pipefail
79-
sudo apt-get update
79+
# Retry apt-get update once on mirror failure before proceeding.
80+
sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
8081
case "${{ matrix.backend }}" in
81-
z3) sudo apt-get install -y z3 ;;
82+
z3) sudo apt-get install -y --fix-missing z3 ;;
8283
cvc5) # Since cvc5 1.2.0 releases ship as a zip with the binary at
8384
# bin/cvc5; the old bare `cvc5-Linux-static` asset no longer exists.
8485
curl -sSL --max-time 120 -o /tmp/cvc5.zip \
@@ -92,17 +93,17 @@ jobs:
9293
https://github.com/vprover/vampire/releases/download/v5.0.1/vampire-Linux-X64.zip
9394
unzip -j -o /tmp/vampire.zip -d /tmp
9495
sudo install -m 0755 /tmp/vampire /usr/local/bin/vampire ;;
95-
eprover) sudo apt-get install -y eprover ;;
96-
spass) sudo apt-get install -y spass ;;
96+
eprover) sudo apt-get install -y --fix-missing eprover ;;
97+
spass) sudo apt-get install -y --fix-missing spass ;;
9798
alt-ergo) # alt-ergo is not in the Ubuntu 24.04 (noble) apt repos.
9899
# Install the prebuilt musl static binary from OCamlPro's
99100
# GitHub releases instead.
100101
curl -sSL --max-time 120 -o /tmp/alt-ergo \
101102
https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.3/alt-ergo-v2.6.3-x86_64-linux-musl
102103
sudo install -m 0755 /tmp/alt-ergo /usr/local/bin/alt-ergo ;;
103-
glpk) sudo apt-get install -y glpk-utils ;;
104-
minizinc) sudo apt-get install -y minizinc ;;
105-
chuffed) sudo apt-get install -y minizinc # chuffed bundled with minizinc-ide on recent ubuntu
104+
glpk) sudo apt-get install -y --fix-missing glpk-utils ;;
105+
minizinc) sudo apt-get install -y --fix-missing minizinc ;;
106+
chuffed) sudo apt-get install -y --fix-missing minizinc # chuffed bundled with minizinc-ide on recent ubuntu
106107
;;
107108
esac
108109
"${{ matrix.backend }}" --version 2>/dev/null || "${{ matrix.backend }}" --help 2>/dev/null || true
@@ -125,8 +126,8 @@ jobs:
125126
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
126127
- name: Install Guix
127128
run: |
128-
sudo apt-get update
129-
sudo apt-get install -y guix
129+
sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
130+
sudo apt-get install -y --fix-missing guix
130131
- name: Resolve manifest (doesn't run tests — just proves the .scm parses)
131132
run: |
132133
guix describe || true
@@ -165,13 +166,13 @@ jobs:
165166
continue-on-error: true
166167
run: |
167168
set -euo pipefail
168-
sudo apt-get update
169+
sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
169170
case "${{ matrix.backend }}" in
170171
coq)
171-
sudo apt-get install -y coq
172+
sudo apt-get install -y --fix-missing coq
172173
;;
173174
agda)
174-
sudo apt-get install -y agda
175+
sudo apt-get install -y --fix-missing agda
175176
;;
176177
idris2)
177178
# Idris2 has no apt package; build from the self-hosting tarball.
@@ -188,14 +189,20 @@ jobs:
188189
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
189190
;;
190191
isabelle)
191-
# Isabelle2024 tarball (~500MB); keep on nightly only.
192-
curl -fsSL -o /tmp/isabelle.tar.gz https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
193-
sudo mkdir -p /opt
194-
sudo tar xzf /tmp/isabelle.tar.gz -C /opt
195-
sudo ln -sf /opt/Isabelle2024/bin/isabelle /usr/local/bin/isabelle
192+
# Isabelle2024 tarball (~500MB); nightly only.
193+
# --retry 3 + --max-time 600 guard the large download.
194+
# find locates the binary regardless of extracted dir name,
195+
# so the symlink survives a future Isabelle2025 release.
196+
curl -fsSL --max-time 600 --retry 3 --retry-delay 15 \
197+
-o /tmp/isabelle.tar.gz \
198+
https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
199+
sudo mkdir -p /opt/isabelle
200+
sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
201+
ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
202+
[ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
196203
;;
197204
why3)
198-
sudo apt-get install -y why3
205+
sudo apt-get install -y --fix-missing why3
199206
;;
200207
dafny)
201208
# Dafny 4.x is distributed as a standalone .NET global tool.
@@ -205,11 +212,19 @@ jobs:
205212
echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
206213
;;
207214
fstar)
208-
# F* ships prebuilt Linux binaries; binary is `fstar.exe` even on Linux.
209-
curl -fsSL -o /tmp/fstar.tar.gz https://github.com/FStarLang/FStar/releases/latest/download/fstar-linux_x86_64.tar.gz
215+
# F* ships prebuilt Linux binaries; binary is fstar.exe even on Linux.
216+
# Asset naming changed in 2025: fstar-linux_x86_64.tar.gz (old) →
217+
# fstar-v{version}-Linux-x86_64.tar.gz (new). Pinned to v2026.04.17.
218+
# Update FSTAR_VER when a newer release lands.
219+
# find locates fstar.exe regardless of extracted directory layout.
220+
FSTAR_VER="v2026.04.17"
221+
curl -fsSL --max-time 300 --retry 2 \
222+
-o /tmp/fstar.tar.gz \
223+
"https://github.com/FStarLang/FStar/releases/download/${FSTAR_VER}/fstar-${FSTAR_VER}-Linux-x86_64.tar.gz"
210224
sudo mkdir -p /opt/fstar
211-
sudo tar xzf /tmp/fstar.tar.gz -C /opt/fstar --strip-components=1
212-
sudo ln -sf /opt/fstar/bin/fstar.exe /usr/local/bin/fstar.exe
225+
sudo tar xzf /tmp/fstar.tar.gz -C /opt/fstar
226+
FSTAR_BIN="$(find /opt/fstar -type f -name fstar.exe | head -n 1)"
227+
[ -n "$FSTAR_BIN" ] && sudo ln -sf "$FSTAR_BIN" /usr/local/bin/fstar.exe
213228
;;
214229
hol-light)
215230
# No prebuilt binary; opam build is ~20min and pulls camlp5.
@@ -219,11 +234,16 @@ jobs:
219234
exit 0
220235
;;
221236
tlaps)
222-
# TLA+ Proof System ships a self-extracting installer; provides tlapm.
223-
curl -fsSL -o /tmp/tlaps.sh https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-installer-linux-x86_64.sh
224-
chmod +x /tmp/tlaps.sh
225-
sudo /tmp/tlaps.sh --prefix=/opt/tlaps
226-
sudo ln -sf /opt/tlaps/bin/tlapm /usr/local/bin/tlapm
237+
# tlapm ships a self-extracting binary installer.
238+
# Latest release (tag 202210041448) asset is a .bin file, not .sh.
239+
# find locates tlapm regardless of installer's extraction layout.
240+
curl -fsSL --max-time 120 \
241+
-o /tmp/tlaps.bin \
242+
"https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-x86_64-linux-gnu-inst.bin"
243+
chmod +x /tmp/tlaps.bin
244+
sudo /tmp/tlaps.bin --prefix=/opt/tlaps || sudo /tmp/tlaps.bin /opt/tlaps
245+
TLAPM_BIN="$(find /opt/tlaps /usr/local -type f -name tlapm 2>/dev/null | head -n 1)"
246+
[ -n "$TLAPM_BIN" ] && sudo ln -sf "$TLAPM_BIN" /usr/local/bin/tlapm
227247
;;
228248
esac
229249
# Best-effort version probe for the matrix log.
@@ -277,7 +297,7 @@ jobs:
277297
continue-on-error: true
278298
run: |
279299
set -euo pipefail
280-
sudo apt-get update
300+
sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
281301
case "${{ matrix.backend }}" in
282302
tamarin)
283303
# Tamarin publishes prebuilt Linux x86_64 tarballs.

0 commit comments

Comments
 (0)