Repository navigation
Add Tier 3 weekly CI for upstream provers and corpus provisioning - #19
Merged
Merged
Conversation
.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.
scripts/provision_corpora.sh Single source of truth for every prover's upstream corpus mirror. A catalogue entry per source (52 total: 45 git clones, 7 manual/gated) binds the external_corpora/<name>/ path the extractors expect to a concrete clone URL, replacing the comments-scattered-across-54-files pattern. Idempotent, non-interactive, retries once on network failure, continues past a dead mirror so one 404 doesn't abort a 40-source run. --list, --status, --force, --all, and named-subset selection. Meant for a nightly cron or a Justfile recipe. scripts/extract_all.sh Composable companion. Runs every scripts/extract_*.jl (or a named subset) under the src/julia Julia project and collects failures into a non-zero exit code. Short-circuits gracefully when an extractor's upstream is absent (the extractors themselves already handle that). Together with provision_corpora.sh + run_training.jl this gives a three-step end-to-end retrain recipe: provision → extract → train. Motivation: the existing expand_training_data.sh was interactive (read -p) and only knew about three sources, so no CI job could grow the corpus without human input. Closing that gap unblocks the 100k per-prover target.
Justfile Three new recipes that compose the scripts landed in 9df340c into an idiomatic end-to-end retrain flow: just provision-corpora [NAMES...] # scripts/provision_corpora.sh just corpora-status # on-disk report just extract-corpora [NAMES...] # scripts/extract_all.sh just retrain # src/julia/run_training.jl just corpus-refresh # all three, in order Each step is idempotent; re-running the pipeline only touches what has changed. The retrain recipe honours the env-var knobs added in 5611cb2 (ECHIDNA_MAX_PROOF_STATES, ECHIDNA_NUM_EPOCHS, ECHIDNA_NUM_NEGATIVES), so: ECHIDNA_MAX_PROOF_STATES=0 just corpus-refresh re-baselines MRR against the full expanded corpus on GPU hardware.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR introduces infrastructure for provisioning and testing heavier upstream theorem provers and verification tools in a weekly CI tier. It adds:
scripts/provision_corpora.sh) — a non-interactive tool to clone/download 40+ upstream prover repositories and benchmarks intoexternal_corpora/scripts/extract_all.sh) — orchestrates allextract_*.jlscripts against provisioned corporaprovision-corpora,extract-corpora,retrain, andcorpus-refreshECHIDNA_MAX_PROOF_STATES,ECHIDNA_NUM_EPOCHS,ECHIDNA_NUM_NEGATIVESfor flexible retrainingKey Changes
scripts/provision_corpora.sh(281 lines)--depth=1 --filter=blob:nonefor bandwidth efficiency (~4-8 GB total)--force)--list,--status,--all, and selective provisioning by namescripts/extract_all.sh(89 lines)extract_*.jlscript non-interactively.github/workflows/live-provers.yml— Tier 3 jobcargo test --test live_prover_suitewithcontinue-on-error: trueso absences are logged as SKIPtests/live_prover_suite.rsassert_version_reachable()with the expected CLI binary namewhichprobe in the suite)src/julia/run_training.jlmax_proof_statesconfigurable viaECHIDNA_MAX_PROOF_STATESenv var (default: 200k on GPU, 50k on CPU; 0 = unlimited)num_epochsconfigurable viaECHIDNA_NUM_EPOCHS(default: 30)num_negativesconfigurable viaECHIDNA_NUM_NEGATIVES(default: 20)Justfileprovision-corpora,corpora-status,extract-corpora,retrain, andcorpus-refreshrecipescorpus-refreshchains the full pipeline: provision → extract → retrainImplementation Details
skipin the catalogue; the CI workflow defers them to Containerfile provisioning or notes them as unavailable.https://claude.ai/code/session_01NFEuqk68SFBy49KRSSVL8N