Skip to content

Commit 3c0b4a2

Browse files
hyperpolymathclaude
andcommitted
fix(live-provers): complete T2 backend hardening — idris2, lean4, dafny, tlapm
idris2: idris2-src-latest.tgz is a 404 on v0.8.0 (no release assets). Try apt install first (available in Ubuntu 24.04 universe). Fallback uses GitHub archive API (always resolves for any tag), pins IDRIS2_VER, adds libgmp-dev, --max-time 300 --retry 2 on curl. lean4: add --max-time 120 to the elan-init.sh curl pipe to prevent stalled downloads hanging the job indefinitely. dafny: add --fix-missing to dotnet-sdk-8.0 apt install to guard against mirror lag (dotnet is large; partial mirror failures happen). tlapm: remove bogus --prefix=/opt/tlaps arg — the makeself installer installs to /usr/local/lib/tlaps and symlinks into /usr/local/bin without needing a prefix. Fallback find+ln only fires when command -v tlapm fails (layout variation safety net). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 83a1540 commit 3c0b4a2

1 file changed

Lines changed: 35 additions & 18 deletions

File tree

.github/workflows/live-provers.yml

Lines changed: 35 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -175,17 +175,29 @@ jobs:
175175
sudo apt-get install -y --fix-missing agda
176176
;;
177177
idris2)
178-
# Idris2 has no apt package; build from the self-hosting tarball.
179-
# Chez Scheme is the recommended backend.
180-
sudo apt-get install -y chezscheme make
181-
curl -fsSL -o /tmp/idris2.tar.gz https://github.com/idris-lang/Idris2/releases/latest/download/idris2-src-latest.tgz || \
182-
curl -fsSL -o /tmp/idris2.tar.gz https://www.idris-lang.org/download/idris2-0.7.0.tgz
183-
mkdir -p /tmp/idris2-src
184-
tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
185-
(cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
178+
# Idris2 v0.8.0 has no pre-built Linux release binary (assets array
179+
# is empty on the GitHub release). Try apt first (available as idris2
180+
# in Ubuntu 24.04 universe); fall back to building from the source
181+
# archive. The old idris2-src-latest.tgz URL is a 404 on releases
182+
# without assets — use the GitHub archive API instead, which always
183+
# resolves for any tag.
184+
sudo apt-get install -y --fix-missing idris2 2>/dev/null || {
185+
IDRIS2_VER="v0.8.0"
186+
sudo apt-get install -y --fix-missing chezscheme make libgmp-dev
187+
curl -fsSL --max-time 300 --retry 2 \
188+
-o /tmp/idris2.tar.gz \
189+
"https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VER}.tar.gz"
190+
mkdir -p /tmp/idris2-src
191+
tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
192+
(cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
193+
}
186194
;;
187195
lean4)
188-
curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain leanprover/lean4:stable
196+
# elan bootstraps the Lean toolchain manager and downloads lean4:stable.
197+
# --max-time guards the pipe against a stalled download.
198+
curl -sSL --max-time 120 \
199+
https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
200+
| sh -s -- -y --default-toolchain leanprover/lean4:stable
189201
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
190202
;;
191203
isabelle)
@@ -205,9 +217,11 @@ jobs:
205217
sudo apt-get install -y --fix-missing why3
206218
;;
207219
dafny)
208-
# Dafny 4.x is distributed as a standalone .NET global tool.
209-
# ubuntu-latest ships dotnet-sdk 8 in setup images; install via apt if absent.
210-
command -v dotnet >/dev/null 2>&1 || sudo apt-get install -y dotnet-sdk-8.0
220+
# Dafny 4.x is distributed as a .NET global tool.
221+
# ubuntu-latest ships dotnet-sdk-8.0 in the default image; install
222+
# via apt only if absent (--fix-missing guards against mirror lag).
223+
command -v dotnet >/dev/null 2>&1 || \
224+
sudo apt-get install -y --fix-missing dotnet-sdk-8.0
211225
dotnet tool install --global Dafny
212226
echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
213227
;;
@@ -234,16 +248,19 @@ jobs:
234248
exit 0
235249
;;
236250
tlaps)
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.
251+
# tlapm 1.5.0 ships a makeself .bin installer (not .sh).
252+
# The installer installs to /usr/local/lib/tlaps and links
253+
# tlapm into /usr/local/bin — no --prefix needed or supported.
254+
# find is a safety net for any layout variation.
240255
curl -fsSL --max-time 120 \
241256
-o /tmp/tlaps.bin \
242257
"https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-x86_64-linux-gnu-inst.bin"
243258
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
259+
sudo /tmp/tlaps.bin
260+
command -v tlapm >/dev/null 2>&1 || {
261+
TLAPM_BIN="$(find /usr /opt -type f -name tlapm 2>/dev/null | head -n 1)"
262+
[ -n "$TLAPM_BIN" ] && sudo ln -sf "$TLAPM_BIN" /usr/local/bin/tlapm
263+
}
247264
;;
248265
esac
249266
# Best-effort version probe for the matrix log.

0 commit comments

Comments
 (0)