feat(ci): L3 Wave-2 — wire idris2/isabelle/dafny/fstar/tlaps + fstar+tlaps tests

Tier-2 (nightly) live-prover CI now has real provisioning, not TODO
placeholders, for every backend except hol-light (which defers to
Wave-3 container provisioning — no prebuilt binary, opam build is
~20 min and pulls camlp5).

- idris2:  bootstrap from source tarball against Chez Scheme.
- isabelle: Isabelle2024 tarball, symlink /usr/local/bin/isabelle.
- dafny:   dotnet tool install --global Dafny (ubuntu-latest has sdk-8).
- fstar:   GitHub release tarball; binary is fstar.exe even on Linux.
- tlaps:   self-extracting installer from tlapm releases; binary is tlapm.
- hol-light: deferred with explicit exit 0 + comment.

Also adds live_fstar_version and live_tlaps_version to the Rust test
suite (matches provers/mod.rs executable names: fstar.exe, tlapm) and
fills in the missing library_paths field on ProverConfig that had made
the test file fail to compile.

Local verification: `cargo test --test live_prover_suite --features
live-provers` runs all 18 tests; 13 real binaries (Z3, CVC5, EProver,
Alt-Ergo, Why3, Vampire, Dafny, Isabelle, Idris2, F*, Coq, Agda, Lean4)
return real versions; 5 auto-skip (GLPK/SPASS/MiniZinc/TLAPS/Chuffed
not on this host). No mock tests were modified.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/live-provers.yml

@@ -155,17 +155,71 @@ jobs:
           set -euo pipefail
           sudo apt-get update
           case "${{ matrix.backend }}" in
-            coq)        sudo apt-get install -y coq ;;
-            agda)       sudo apt-get install -y agda ;;
-            idris2)     echo "idris2 Wave-2 TODO: install via upstream installer or flake" ;;
-            lean4)      curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain leanprover/lean4:stable
-                        echo "$HOME/.elan/bin" >> "$GITHUB_PATH" ;;
-            isabelle)   echo "isabelle Wave-2 TODO: install Isabelle2024+ tarball" ;;
-            why3)       sudo apt-get install -y why3 ;;
-            dafny)      echo "dafny Wave-2 TODO: install via dotnet" ;;
-            fstar)      echo "fstar Wave-2 TODO" ;;
-            hol-light)  echo "hol-light Wave-2 TODO" ;;
-            tlaps)      echo "tlaps Wave-2 TODO" ;;
+            coq)
+              sudo apt-get install -y coq
+              ;;
+            agda)
+              sudo apt-get install -y agda
+              ;;
+            idris2)
+              # Idris2 has no apt package; build from the self-hosting tarball.
+              # Chez Scheme is the recommended backend.
+              sudo apt-get install -y chezscheme make
+              curl -fsSL -o /tmp/idris2.tar.gz https://github.com/idris-lang/Idris2/releases/latest/download/idris2-src-latest.tgz || \
+                curl -fsSL -o /tmp/idris2.tar.gz https://www.idris-lang.org/download/idris2-0.7.0.tgz
+              mkdir -p /tmp/idris2-src
+              tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
+              (cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
+              ;;
+            lean4)
+              curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain leanprover/lean4:stable
+              echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+              ;;
+            isabelle)
+              # Isabelle2024 tarball (~500MB); keep on nightly only.
+              curl -fsSL -o /tmp/isabelle.tar.gz https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
+              sudo mkdir -p /opt
+              sudo tar xzf /tmp/isabelle.tar.gz -C /opt
+              sudo ln -sf /opt/Isabelle2024/bin/isabelle /usr/local/bin/isabelle
+              ;;
+            why3)
+              sudo apt-get install -y why3
+              ;;
+            dafny)
+              # Dafny 4.x is distributed as a standalone .NET global tool.
+              # ubuntu-latest ships dotnet-sdk 8 in setup images; install via apt if absent.
+              command -v dotnet >/dev/null 2>&1 || sudo apt-get install -y dotnet-sdk-8.0
+              dotnet tool install --global Dafny
+              echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
+              ;;
+            fstar)
+              # F* ships prebuilt Linux binaries; binary is `fstar.exe` even on Linux.
+              curl -fsSL -o /tmp/fstar.tar.gz https://github.com/FStarLang/FStar/releases/latest/download/fstar-linux_x86_64.tar.gz
+              sudo mkdir -p /opt/fstar
+              sudo tar xzf /tmp/fstar.tar.gz -C /opt/fstar --strip-components=1
+              sudo ln -sf /opt/fstar/bin/fstar.exe /usr/local/bin/fstar.exe
+              ;;
+            hol-light)
+              # No prebuilt binary; opam build is ~20min and pulls camlp5.
+              # Deferred to Wave-3 (container-based provisioning) per the
+              # production-wiring plan.
+              echo "hol-light deferred to Wave-3 container provisioning"
+              exit 0
+              ;;
+            tlaps)
+              # TLA+ Proof System ships a self-extracting installer; provides tlapm.
+              curl -fsSL -o /tmp/tlaps.sh https://github.com/tlaplus/tlapm/releases/latest/download/tlaps-installer-linux-x86_64.sh
+              chmod +x /tmp/tlaps.sh
+              sudo /tmp/tlaps.sh --prefix=/opt/tlaps
+              sudo ln -sf /opt/tlaps/bin/tlapm /usr/local/bin/tlapm
+              ;;
+          esac
+          # Best-effort version probe for the matrix log.
+          case "${{ matrix.backend }}" in
+            fstar)     fstar.exe --version || true ;;
+            tlaps)     tlapm --version || true ;;
+            hol-light) true ;;
+            *)         "${{ matrix.backend }}" --version 2>/dev/null || true ;;
           esac
       - name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-2 wires up)
         continue-on-error: true

tests/live_prover_suite.rs

@@ -41,6 +41,7 @@ fn binary_on_path(name: &str) -> Option<PathBuf> {
 fn live_config(executable: &str) -> ProverConfig {
     ProverConfig {
         executable: PathBuf::from(executable),
+        library_paths: vec![],
         args: vec![],
         timeout: 30,
         neural_enabled: false,
@@ -107,6 +108,8 @@ fn kind_label(kind: ProverKind) -> &'static str {
         ProverKind::Isabelle => "Isabelle",
         ProverKind::Why3 => "Why3",
         ProverKind::Dafny => "Dafny",
+        ProverKind::FStar => "F*",
+        ProverKind::TLAPS => "TLAPS",
         _ => "<other>",
     }
 }
@@ -198,3 +201,16 @@ async fn live_why3_version() {
 async fn live_dafny_version() {
     assert_version_reachable(ProverKind::Dafny, "dafny").await;
 }
+
+#[tokio::test]
+async fn live_fstar_version() {
+    // Canonical binary name is `fstar.exe` (per ProverKind::FStar executable()
+    // in src/rust/provers/mod.rs — F* uses the `.exe` suffix even on Linux).
+    assert_version_reachable(ProverKind::FStar, "fstar.exe").await;
+}
+
+#[tokio::test]
+async fn live_tlaps_version() {
+    // TLA+ Proof System's prover is `tlapm` (per provers/mod.rs).
+    assert_version_reachable(ProverKind::TLAPS, "tlapm").await;
+}