feat(ci,ml): Tier-3 live-prover provisioning + uncap Flux training

claude · claude · commit 62e55f70ca38 · 2026-04-19T22:30:55.000Z
.github/workflows/live-provers.yml
  Replace Tier-3 placeholder with a per-backend matrix.  Live-provisioned
  (apt / upstream tarball): tamarin, proverif, metamath, twelf, ortools.
  Deferred-to-Containerfile with explicit skip note: hol4, acl2, scip,
  imandra.  Each job probes the binary and runs the single matching case
  from tests/live_prover_suite.rs with continue-on-error while Wave-3
  wires up.

tests/live_prover_suite.rs
  Add #[tokio::test] entries for all nine Tier-3 backends and extend
  kind_label with their display names.  Tests SKIP when the binary is
  absent on PATH (existing `which` probe), so running locally or in PR
  CI costs nothing; only the weekly tier3 matrix exercises them.

src/julia/run_training.jl
  Drop the hardcoded max_proof_states=50_000 cap that made the expanded
  corpus pointless.  Default 200k on GPU / 50k on CPU, overridable via
  ECHIDNA_MAX_PROOF_STATES (0 = unlimited).  ECHIDNA_NUM_EPOCHS and
  ECHIDNA_NUM_NEGATIVES gain the same treatment.  Required before
  retraining on the 2026-04 corpus expansion.
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
@@ -226,21 +226,127 @@ jobs:
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
   # ============================================================================
-  # Tier 3 — weekly.  Container-provisioned provers.  Wave-3 placeholder.
+  # Tier 3 — weekly.  Heavier upstream provers, best-effort provisioning.
+  #
+  # Backends grouped as:
+  #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
+  #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
+  #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
+  #       Provisioning step emits a skip note; test step runs the suite with
+  #       continue-on-error so the matrix stays green and the binary's absence
+  #       is logged as SKIP by the suite's `which` probe.
   # ============================================================================
   tier3:
-    name: T3 container provers
+    name: T3 / ${{ matrix.backend }}
     if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
     runs-on: ubuntu-latest
     continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        backend:
+          - tamarin
+          - proverif
+          - metamath
+          - twelf
+          - ortools
+          - hol4
+          - acl2
+          - scip
+          - imandra
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
-      - name: Announce Wave-3 TODO
+      - name: Install Rust
+        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
+      - name: Cache Cargo
+        uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
+      - name: Provision ${{ matrix.backend }} (best-effort)
+        continue-on-error: true
         run: |
-          echo "Tier-3 backends (Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath)"
-          echo "are provisioned via per-backend Containerfiles in Wave-3 of L3."
-          echo "See ~/Desktop/ECHIDNA-L3-LIVE-PROVER-CI-PROMPT.md for scope."
+          set -euo pipefail
+          sudo apt-get update
+          case "${{ matrix.backend }}" in
+            tamarin)
+              # Tamarin publishes prebuilt Linux x86_64 tarballs.
+              curl -fsSL -o /tmp/tamarin.tar.gz \
+                https://github.com/tamarin-prover/tamarin-prover/releases/latest/download/tamarin-prover-linux64-ubuntu.tar.gz || \
+                curl -fsSL -o /tmp/tamarin.tar.gz \
+                https://github.com/tamarin-prover/tamarin-prover/releases/download/1.10.0/tamarin-prover-1.10.0-linux64-ubuntu.tar.gz
+              sudo mkdir -p /opt/tamarin
+              sudo tar xzf /tmp/tamarin.tar.gz -C /opt/tamarin
+              # The tarball lays down tamarin-prover directly or in a version dir; link whichever we find.
+              TAMARIN_BIN="$(find /opt/tamarin -type f -name tamarin-prover | head -n 1)"
+              [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
+              ;;
+            proverif)
+              # ProVerif is in the Ubuntu/Debian main repos.
+              sudo apt-get install -y proverif
+              ;;
+            metamath)
+              # metamath-exe is small; apt-installable on Ubuntu with build fallback.
+              sudo apt-get install -y metamath || {
+                sudo apt-get install -y build-essential git autoconf automake
+                git clone --depth=1 https://github.com/metamath/metamath-exe.git /tmp/mm
+                (cd /tmp/mm && ./build.sh) || \
+                  (cd /tmp/mm && autoreconf -i && ./configure && make)
+                sudo install -m 0755 /tmp/mm/metamath /usr/local/bin/metamath
+              }
+              ;;
+            twelf)
+              # Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
+              sudo apt-get install -y twelf || \
+                echo "twelf unavailable via apt on this runner; test will SKIP."
+              ;;
+            ortools)
+              # Google OR-Tools ships prebuilt Linux tarballs.  The binary we
+              # expose to echidna is a small wrapper that invokes the solver CLI.
+              OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
+              curl -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
+                echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
+                exit 0
+              }
+              sudo mkdir -p /opt/ortools
+              sudo tar xzf /tmp/ortools.tar.gz -C /opt/ortools --strip-components=1
+              # Echidna's ORTools backend invokes `ortools_solve`.  The release
+              # ships `bin/solve` or similar; create the expected symlink.
+              OR_BIN="$(find /opt/ortools -type f \( -name ortools_solve -o -name solve \) | head -n 1)"
+              [ -n "$OR_BIN" ] && sudo ln -sf "$OR_BIN" /usr/local/bin/ortools_solve
+              ;;
+            hol4)
+              # HOL4 requires Poly/ML and a full tree build (~15min+); defer to
+              # container provisioning.  Test step will SKIP on this runner.
+              echo "hol4: heavy Poly/ML build deferred to Containerfile provisioning."
+              ;;
+            acl2)
+              # ACL2 requires a Common Lisp image (CCL/SBCL) and a 10min+ build;
+              # defer to container provisioning.  Test step will SKIP.
+              echo "acl2: heavy SBCL+image build deferred to Containerfile."
+              ;;
+            scip)
+              # SCIP Optimization Suite needs a full cmake build (~10min).  The
+              # upstream tarball requires a form-gated download, so CI defers to
+              # Containerfile provisioning.  Test step will SKIP.
+              echo "scip: form-gated upstream tarball; deferred to Containerfile."
+              ;;
+            imandra)
+              # Imandra is proprietary; no public Linux binary.  Handled via
+              # vendor-supplied container where a licence is available.
+              echo "imandra: proprietary; no public CI provisioning available."
+              ;;
+          esac
+          # Best-effort version probe for the matrix log.
+          case "${{ matrix.backend }}" in
+            tamarin)    tamarin-prover --version 2>&1 | head -n 1 || true ;;
+            proverif)   proverif --version 2>&1 | head -n 1 || true ;;
+            metamath)   echo exit | metamath 2>&1 | head -n 1 || true ;;
+            twelf)      twelf-server --help 2>&1 | head -n 1 || true ;;
+            ortools)    ortools_solve --help 2>&1 | head -n 1 || true ;;
+            hol4|acl2|scip|imandra) true ;;
+          esac
+      - name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-3 wires up)
+        continue-on-error: true
+        run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
   # ============================================================================
   # Tier 4 — quarterly, best-effort / allow-fail.
diff --git a/src/julia/run_training.jl b/src/julia/run_training.jl
@@ -10,6 +10,14 @@
 #   data_dir  = training_data/
 #   save_dir  = models/neural/
 #
+# Environment overrides (see below):
+#   ECHIDNA_MAX_PROOF_STATES — cap on proof states loaded (default 200000 on
+#     GPU, 50000 on CPU).  Set to 0 to disable the cap and consume the entire
+#     expanded corpus; required when re-baselining after corpus growth.
+#   ECHIDNA_NUM_EPOCHS      — training epochs (default 30).
+#   ECHIDNA_NUM_NEGATIVES   — hard-negative premise samples per example
+#     (default 20).
+#
 # This script:
 #   1. Loads JSONL training data (proof states + premises)
 #   2. Builds vocabulary from the corpus
@@ -74,10 +82,24 @@ println("═══════════════════════
 println("Loading training data...")
 println("═══════════════════════════════════════════════════════════")
 
+# Default cap: 200k on GPU (enough to exercise the expanded corpus without
+# OOM on a 24GB card), 50k on CPU (keeps wall-clock finite).  An operator
+# re-baselining after corpus growth sets ECHIDNA_MAX_PROOF_STATES=0 to lift
+# the cap entirely.
+default_cap = has_gpu ? 200_000 : 50_000
+cap_env = get(ENV, "ECHIDNA_MAX_PROOF_STATES", "")
+max_proof_states = isempty(cap_env) ? default_cap : parse(Int, cap_env)
+# `load_training_data` treats any value `<= 0` as "load everything".
+cap_label = max_proof_states <= 0 ? "unlimited" : string(max_proof_states)
+println("  max_proof_states = $cap_label")
+
+num_negatives = parse(Int, get(ENV, "ECHIDNA_NUM_NEGATIVES", "20"))
+println("  num_negatives    = $num_negatives")
+
 train_data, val_data, vocab = load_training_data(data_dir;
     train_split=0.8f0,
-    max_proof_states=50000,  # Cap for reasonable training time
-    num_negatives=20
+    max_proof_states=max_proof_states,
+    num_negatives=num_negatives,
 )
 
 if isempty(train_data.examples)
@@ -101,8 +123,9 @@ println("Model created successfully")
 println()
 
 # Configure training
+num_epochs = parse(Int, get(ENV, "ECHIDNA_NUM_EPOCHS", "30"))
 training_config = TrainingConfig(
-    num_epochs=30,
+    num_epochs=num_epochs,
     learning_rate=1f-4,
     lr_schedule=:cosine,
     weight_decay=1f-5,
diff --git a/tests/live_prover_suite.rs b/tests/live_prover_suite.rs
@@ -110,6 +110,15 @@ fn kind_label(kind: ProverKind) -> &'static str {
         ProverKind::Dafny => "Dafny",
         ProverKind::FStar => "F*",
         ProverKind::TLAPS => "TLAPS",
+        ProverKind::Tamarin => "Tamarin",
+        ProverKind::ProVerif => "ProVerif",
+        ProverKind::Metamath => "Metamath",
+        ProverKind::Twelf => "Twelf",
+        ProverKind::ORTools => "OR-Tools",
+        ProverKind::HOL4 => "HOL4",
+        ProverKind::ACL2 => "ACL2",
+        ProverKind::SCIP => "SCIP",
+        ProverKind::Imandra => "Imandra",
         _ => "<other>",
     }
 }
@@ -214,3 +223,65 @@ async fn live_tlaps_version() {
     // TLA+ Proof System's prover is `tlapm` (per provers/mod.rs).
     assert_version_reachable(ProverKind::TLAPS, "tlapm").await;
 }
+
+// ==========================================================================
+// Tier 3 — weekly.  Upstream-tarball or heavier-build provers.  Most of
+// these SKIP locally and in PR CI; the weekly tier3 matrix in
+// live-provers.yml provisions each binary in its own job before running
+// `cargo test ... <backend>`, so only the matching test runs per job.
+// ==========================================================================
+
+#[tokio::test]
+async fn live_tamarin_version() {
+    assert_version_reachable(ProverKind::Tamarin, "tamarin-prover").await;
+}
+
+#[tokio::test]
+async fn live_proverif_version() {
+    assert_version_reachable(ProverKind::ProVerif, "proverif").await;
+}
+
+#[tokio::test]
+async fn live_metamath_version() {
+    assert_version_reachable(ProverKind::Metamath, "metamath").await;
+}
+
+#[tokio::test]
+async fn live_twelf_version() {
+    // Twelf's CLI entry is `twelf-server` per provers/mod.rs.
+    assert_version_reachable(ProverKind::Twelf, "twelf-server").await;
+}
+
+#[tokio::test]
+async fn live_ortools_version() {
+    // Echidna's ORTools backend invokes `ortools_solve` (wrapper around the
+    // OR-Tools C++ solve CLI).  Provisioned via upstream tarball.
+    assert_version_reachable(ProverKind::ORTools, "ortools_solve").await;
+}
+
+#[tokio::test]
+async fn live_hol4_version() {
+    // HOL4 requires Poly/ML + a tree build; provisioning is deferred to
+    // Containerfile.  Test SKIPs on runners without `hol` on PATH.
+    assert_version_reachable(ProverKind::HOL4, "hol").await;
+}
+
+#[tokio::test]
+async fn live_acl2_version() {
+    // ACL2 requires a Common Lisp image; provisioning deferred to Containerfile.
+    assert_version_reachable(ProverKind::ACL2, "acl2").await;
+}
+
+#[tokio::test]
+async fn live_scip_version() {
+    // SCIP requires a cmake build of SCIP Optimization Suite; deferred to
+    // Containerfile.  Test SKIPs until provisioned.
+    assert_version_reachable(ProverKind::SCIP, "scip").await;
+}
+
+#[tokio::test]
+async fn live_imandra_version() {
+    // Imandra is proprietary; handled via vendor-supplied container where a
+    // licence is available.  Test SKIPs on public CI.
+    assert_version_reachable(ProverKind::Imandra, "imandra").await;
+}
