Skip to content

Commit 1211f02

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Add Tier 3 weekly CI for upstream provers and corpus provisioning (#19)
## Summary This PR introduces infrastructure for provisioning and testing heavier upstream theorem provers and verification tools in a weekly CI tier. It adds: 1. **Corpus provisioning script** (`scripts/provision_corpora.sh`) — a non-interactive tool to clone/download 40+ upstream prover repositories and benchmarks into `external_corpora/` 2. **Extractor runner** (`scripts/extract_all.sh`) — orchestrates all `extract_*.jl` scripts against provisioned corpora 3. **Tier 3 weekly CI matrix** — tests 9 backends (Tamarin, ProVerif, Metamath, Twelf, OR-Tools, HOL4, ACL2, SCIP, Imandra) with per-backend provisioning 4. **Justfile recipes** — convenient targets for the corpus pipeline: `provision-corpora`, `extract-corpora`, `retrain`, and `corpus-refresh` 5. **Training script environment overrides** — `ECHIDNA_MAX_PROOF_STATES`, `ECHIDNA_NUM_EPOCHS`, `ECHIDNA_NUM_NEGATIVES` for flexible retraining ## Key Changes - **`scripts/provision_corpora.sh`** (281 lines) - Catalogues 40+ upstream sources (git repos, tarballs, form-gated/proprietary) - Clones with `--depth=1 --filter=blob:none` for bandwidth efficiency (~4-8 GB total) - Idempotent (skips existing directories unless `--force`) - Retries once on network failure; continues on error so one offline mirror doesn't abort the batch - Supports `--list`, `--status`, `--all`, and selective provisioning by name - **`scripts/extract_all.sh`** (89 lines) - Runs every `extract_*.jl` script non-interactively - Collects failures and exits with count of failed extractors - Suitable for nightly cron workflows - **`.github/workflows/live-provers.yml`** — Tier 3 job - Replaced placeholder with a 9-job matrix (one per backend) - Each job provisions its backend via apt, upstream tarball, or defers to Containerfile - Runs `cargo test --test live_prover_suite` with `continue-on-error: true` so absences are logged as SKIP - Includes version probes in the matrix log for debugging - **`tests/live_prover_suite.rs`** - Added 9 new async tests for Tier 3 backends (Tamarin, ProVerif, Metamath, Twelf, OR-Tools, HOL4, ACL2, SCIP, Imandra) - Each test calls `assert_version_reachable()` with the expected CLI binary name - Tests SKIP gracefully if the binary is absent (via `which` probe in the suite) - **`src/julia/run_training.jl`** - Made `max_proof_states` configurable via `ECHIDNA_MAX_PROOF_STATES` env var (default: 200k on GPU, 50k on CPU; 0 = unlimited) - Made `num_epochs` configurable via `ECHIDNA_NUM_EPOCHS` (default: 30) - Made `num_negatives` configurable via `ECHIDNA_NUM_NEGATIVES` (default: 20) - Logs the active configuration at startup - **`Justfile`** - Added `provision-corpora`, `corpora-status`, `extract-corpora`, `retrain`, and `corpus-refresh` recipes - `corpus-refresh` chains the full pipeline: provision → extract → retrain ## Implementation Details - **Provisioning strategy**: Heavy builds (HOL4, ACL2, SCIP) and proprietary tools (Imandra) are marked `skip` in the catalogue; the CI workflow defers them to Containerfile provisioning or notes them as unavailable. - **Graceful degradation**: Tests use ` https://claude.ai/code/session_01NFEuqk68SFBy49KRSSVL8N --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 2200dcf commit 1211f02

6 files changed

Lines changed: 613 additions & 9 deletions

File tree

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

Lines changed: 112 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -226,21 +226,127 @@ jobs:
226226
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
227227

228228
# ============================================================================
229-
# Tier 3 — weekly. Container-provisioned provers. Wave-3 placeholder.
229+
# Tier 3 — weekly. Heavier upstream provers, best-effort provisioning.
230+
#
231+
# Backends grouped as:
232+
# A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
233+
# metamath, twelf, ortools). Version-check runs, skip-if-absent.
234+
# B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
235+
# Provisioning step emits a skip note; test step runs the suite with
236+
# continue-on-error so the matrix stays green and the binary's absence
237+
# is logged as SKIP by the suite's `which` probe.
230238
# ============================================================================
231239
tier3:
232-
name: T3 container provers
240+
name: T3 / ${{ matrix.backend }}
233241
if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
234242
runs-on: ubuntu-latest
235243
continue-on-error: true
244+
strategy:
245+
fail-fast: false
246+
matrix:
247+
backend:
248+
- tamarin
249+
- proverif
250+
- metamath
251+
- twelf
252+
- ortools
253+
- hol4
254+
- acl2
255+
- scip
256+
- imandra
236257
steps:
237258
- name: Checkout
238259
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
239-
- name: Announce Wave-3 TODO
260+
- name: Install Rust
261+
uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
262+
- name: Cache Cargo
263+
uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
264+
- name: Provision ${{ matrix.backend }} (best-effort)
265+
continue-on-error: true
240266
run: |
241-
echo "Tier-3 backends (Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath)"
242-
echo "are provisioned via per-backend Containerfiles in Wave-3 of L3."
243-
echo "See ~/Desktop/ECHIDNA-L3-LIVE-PROVER-CI-PROMPT.md for scope."
267+
set -euo pipefail
268+
sudo apt-get update
269+
case "${{ matrix.backend }}" in
270+
tamarin)
271+
# Tamarin publishes prebuilt Linux x86_64 tarballs.
272+
curl -fsSL -o /tmp/tamarin.tar.gz \
273+
https://github.com/tamarin-prover/tamarin-prover/releases/latest/download/tamarin-prover-linux64-ubuntu.tar.gz || \
274+
curl -fsSL -o /tmp/tamarin.tar.gz \
275+
https://github.com/tamarin-prover/tamarin-prover/releases/download/1.10.0/tamarin-prover-1.10.0-linux64-ubuntu.tar.gz
276+
sudo mkdir -p /opt/tamarin
277+
sudo tar xzf /tmp/tamarin.tar.gz -C /opt/tamarin
278+
# The tarball lays down tamarin-prover directly or in a version dir; link whichever we find.
279+
TAMARIN_BIN="$(find /opt/tamarin -type f -name tamarin-prover | head -n 1)"
280+
[ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
281+
;;
282+
proverif)
283+
# ProVerif is in the Ubuntu/Debian main repos.
284+
sudo apt-get install -y proverif
285+
;;
286+
metamath)
287+
# metamath-exe is small; apt-installable on Ubuntu with build fallback.
288+
sudo apt-get install -y metamath || {
289+
sudo apt-get install -y build-essential git autoconf automake
290+
git clone --depth=1 https://github.com/metamath/metamath-exe.git /tmp/mm
291+
(cd /tmp/mm && ./build.sh) || \
292+
(cd /tmp/mm && autoreconf -i && ./configure && make)
293+
sudo install -m 0755 /tmp/mm/metamath /usr/local/bin/metamath
294+
}
295+
;;
296+
twelf)
297+
# Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
298+
sudo apt-get install -y twelf || \
299+
echo "twelf unavailable via apt on this runner; test will SKIP."
300+
;;
301+
ortools)
302+
# Google OR-Tools ships prebuilt Linux tarballs. The binary we
303+
# expose to echidna is a small wrapper that invokes the solver CLI.
304+
OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
305+
curl -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
306+
echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
307+
exit 0
308+
}
309+
sudo mkdir -p /opt/ortools
310+
sudo tar xzf /tmp/ortools.tar.gz -C /opt/ortools --strip-components=1
311+
# Echidna's ORTools backend invokes `ortools_solve`. The release
312+
# ships `bin/solve` or similar; create the expected symlink.
313+
OR_BIN="$(find /opt/ortools -type f \( -name ortools_solve -o -name solve \) | head -n 1)"
314+
[ -n "$OR_BIN" ] && sudo ln -sf "$OR_BIN" /usr/local/bin/ortools_solve
315+
;;
316+
hol4)
317+
# HOL4 requires Poly/ML and a full tree build (~15min+); defer to
318+
# container provisioning. Test step will SKIP on this runner.
319+
echo "hol4: heavy Poly/ML build deferred to Containerfile provisioning."
320+
;;
321+
acl2)
322+
# ACL2 requires a Common Lisp image (CCL/SBCL) and a 10min+ build;
323+
# defer to container provisioning. Test step will SKIP.
324+
echo "acl2: heavy SBCL+image build deferred to Containerfile."
325+
;;
326+
scip)
327+
# SCIP Optimization Suite needs a full cmake build (~10min). The
328+
# upstream tarball requires a form-gated download, so CI defers to
329+
# Containerfile provisioning. Test step will SKIP.
330+
echo "scip: form-gated upstream tarball; deferred to Containerfile."
331+
;;
332+
imandra)
333+
# Imandra is proprietary; no public Linux binary. Handled via
334+
# vendor-supplied container where a licence is available.
335+
echo "imandra: proprietary; no public CI provisioning available."
336+
;;
337+
esac
338+
# Best-effort version probe for the matrix log.
339+
case "${{ matrix.backend }}" in
340+
tamarin) tamarin-prover --version 2>&1 | head -n 1 || true ;;
341+
proverif) proverif --version 2>&1 | head -n 1 || true ;;
342+
metamath) echo exit | metamath 2>&1 | head -n 1 || true ;;
343+
twelf) twelf-server --help 2>&1 | head -n 1 || true ;;
344+
ortools) ortools_solve --help 2>&1 | head -n 1 || true ;;
345+
hol4|acl2|scip|imandra) true ;;
346+
esac
347+
- name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-3 wires up)
348+
continue-on-error: true
349+
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
244350

245351
# ============================================================================
246352
# Tier 4 — quarterly, best-effort / allow-fail.

‎Justfile‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,40 @@ vocab-canon:
7474
julia scripts/vocabulary_mine_corpus.jl
7575
julia scripts/vocabulary_canonicalize.jl
7676

77+
# ── Corpus / training pipeline ─────────────────────────────────
78+
#
79+
# Three steps in order: provision upstream mirrors, run every extractor,
80+
# then retrain. Each step is idempotent; re-running only touches what
81+
# has changed. See scripts/provision_corpora.sh --list for the source
82+
# catalogue.
83+
84+
# Clone every upstream prover corpus into external_corpora/.
85+
# Pass specific names to provision a subset: `just provision-corpora metamath mathlib4`.
86+
provision-corpora *NAMES:
87+
@if [ -z "{{NAMES}}" ]; then \
88+
scripts/provision_corpora.sh --all; \
89+
else \
90+
scripts/provision_corpora.sh {{NAMES}}; \
91+
fi
92+
93+
# Report which upstream corpora are on disk and their sizes.
94+
corpora-status:
95+
scripts/provision_corpora.sh --status
96+
97+
# Run every scripts/extract_*.jl against the provisioned corpora.
98+
# Pass names to run a subset: `just extract-corpora metamath mathlib4`.
99+
extract-corpora *NAMES:
100+
scripts/extract_all.sh {{NAMES}}
101+
102+
# Full retrain from provisioned corpora. Honours ECHIDNA_MAX_PROOF_STATES
103+
# (0 = unlimited), ECHIDNA_NUM_EPOCHS, ECHIDNA_NUM_NEGATIVES.
104+
retrain:
105+
julia --project=src/julia src/julia/run_training.jl
106+
107+
# End-to-end pipeline: provision → extract → retrain.
108+
# Use `ECHIDNA_MAX_PROOF_STATES=0 just corpus-refresh` to lift the sample cap.
109+
corpus-refresh: provision-corpora extract-corpora retrain
110+
77111
# Run the eight-axis metrics suite against the current corpus and post
78112
# results to VeriSimDB. Falls back to training_data/metrics_<run_id>.jsonl
79113
# if VERISIM_URL is unreachable. Target values are documented in

‎scripts/extract_all.sh‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
#
5+
# ECHIDNA — run every scripts/extract_*.jl once, non-interactively.
6+
#
7+
# Assumes scripts/provision_corpora.sh has already populated
8+
# external_corpora/; extractors whose upstream is absent short-circuit
9+
# with a print line (they already handle missing inputs gracefully).
10+
#
11+
# Usage
12+
# -----
13+
# scripts/extract_all.sh # run every extractor
14+
# scripts/extract_all.sh NAME ... # run only the named extractors
15+
# # (matches scripts/extract_<NAME>.jl)
16+
# scripts/extract_all.sh --list # list available extractors
17+
#
18+
# Environment
19+
# ECHIDNA_JULIA_PROJECT — path passed to `julia --project=`
20+
# (default: src/julia).
21+
#
22+
# Exit code is the number of extractors that failed (0 on clean run,
23+
# N on partial failure). Suitable for a nightly cron.
24+
25+
set -uo pipefail # NOTE: not `set -e` — we want to collect failures, not abort.
26+
27+
ECHIDNA_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
28+
JULIA_PROJECT="${ECHIDNA_JULIA_PROJECT:-$ECHIDNA_ROOT/src/julia}"
29+
30+
list_extractors() {
31+
( cd "$ECHIDNA_ROOT/scripts" && ls extract_*.jl 2>/dev/null | sed 's/^extract_//; s/\.jl$//' )
32+
}
33+
34+
# Handle info flags before probing the environment.
35+
case "${1:-}" in
36+
--list)
37+
list_extractors
38+
exit 0
39+
;;
40+
-h|--help)
41+
sed -n '4,22p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
42+
exit 0
43+
;;
44+
esac
45+
46+
if ! command -v julia >/dev/null 2>&1; then
47+
echo "error: julia not on PATH; install Julia to run the extractors." >&2
48+
exit 127
49+
fi
50+
51+
# Build the list of extractors to run.
52+
if [[ $# -gt 0 ]]; then
53+
targets=()
54+
for name in "$@"; do
55+
path="$ECHIDNA_ROOT/scripts/extract_${name}.jl"
56+
if [[ ! -f "$path" ]]; then
57+
echo "error: no such extractor: extract_${name}.jl" >&2
58+
exit 2
59+
fi
60+
targets+=("$path")
61+
done
62+
else
63+
mapfile -t targets < <(find "$ECHIDNA_ROOT/scripts" -maxdepth 1 -name 'extract_*.jl' | sort)
64+
fi
65+
66+
echo "Running ${#targets[@]} extractor(s) with --project=$JULIA_PROJECT"
67+
echo
68+
69+
failed=()
70+
for script in "${targets[@]}"; do
71+
name="$(basename "$script" .jl)"
72+
echo "========================================"
73+
echo " $name"
74+
echo "========================================"
75+
if julia --project="$JULIA_PROJECT" "$script"; then
76+
echo " [ok] $name"
77+
else
78+
echo " [FAIL] $name"
79+
failed+=("$name")
80+
fi
81+
echo
82+
done
83+
84+
if [[ ${#failed[@]} -gt 0 ]]; then
85+
echo "Extractors that failed: ${failed[*]}"
86+
exit "${#failed[@]}"
87+
fi
88+
89+
echo "All extractors completed."

0 commit comments

Comments
 (0)