From 355497f4351259274830458dc88179090d65d67f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 1 Jul 2026 22:34:10 +0100 Subject: [PATCH] =?UTF-8?q?fix(ci):=20formal-verification=20=E2=80=94=20ma?= =?UTF-8?q?ke=20creusot-verify=20prover=20install=20actually=20installable?= =?UTF-8?q?=20(refs=20#250)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit alt-ergo has no installation candidate in Ubuntu 24.04's apt, so the 'Install Why3 and SMT solvers' step has exited 100 on every run since 2026-04-27. Drop alt-ergo from the apt line and install the pinned upstream musl static binary (v2.6.3) from OCamlPro's GitHub releases — the same provisioning pattern live-provers.yml already uses for the alt-ergo matrix cell. Also verify the binary alongside why3/z3. Deeper blockers remain behind this step (cargo install creusot has no crates.io candidate), so this does not close #250 by itself. Co-Authored-By: Claude Fable 5 --- .github/workflows/formal-verification.yml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 802ad7b5..d397b67c 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -90,8 +90,16 @@ jobs: - name: Install Why3 and SMT solvers run: | + set -euo pipefail sudo apt-get update -qq - sudo apt-get install -y --no-install-recommends why3 z3 alt-ergo + sudo apt-get install -y --no-install-recommends why3 z3 + # alt-ergo has no installation candidate in the Ubuntu 24.04 + # (noble) apt repos (#250). Install the prebuilt musl static + # binary pinned from OCamlPro's GitHub releases instead — same + # provisioning pattern as live-provers.yml. + curl -sSL --max-time 120 -o /tmp/alt-ergo \ + https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.3/alt-ergo-v2.6.3-x86_64-linux-musl + sudo install -m 0755 /tmp/alt-ergo /usr/local/bin/alt-ergo # why3 + z3 cover all current obligations. alt-ergo is included # as a fallback solver for obligations z3 times out on. @@ -99,6 +107,7 @@ jobs: run: | why3 --version z3 --version + alt-ergo --version why3 config detect - name: Install Creusot