Skip to content

Commit e8854ab

Browse files
claudeclaude
committed
feat(corpus): non-interactive upstream provisioning + extractor driver
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.
1 parent 62e55f7 commit e8854ab

2 files changed

Lines changed: 370 additions & 0 deletions

File tree

‎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."

‎scripts/provision_corpora.sh‎

Lines changed: 281 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,281 @@
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 — Non-interactive upstream corpus provisioning.
6+
#
7+
# Clones the upstream mirror of every theorem-prover corpus the extractors
8+
# under scripts/extract_*.jl expect at external_corpora/<name>/. Each
9+
# clone uses --depth=1 to keep the bandwidth bill finite (~4-8 GB total
10+
# when all sources are selected).
11+
#
12+
# Usage
13+
# -----
14+
# scripts/provision_corpora.sh [NAME ...] # provision the named sources
15+
# scripts/provision_corpora.sh --all # provision every source
16+
# scripts/provision_corpora.sh --list # print the source catalogue
17+
# scripts/provision_corpora.sh --status # show which sources are on disk
18+
#
19+
# Selection names match the external_corpora/<name>/ directory each extractor
20+
# expects. Unknown names exit non-zero so typos fail loudly in CI.
21+
#
22+
# Behaviour
23+
# * If external_corpora/<name>/ already exists the source is skipped
24+
# (idempotent; safe to re-run). Pass --force to re-clone into a
25+
# fresh directory.
26+
# * Network failures are retried once; a failure after that is logged
27+
# and the script continues to the next source (so a single offline
28+
# mirror doesn't abort a 40-source provisioning).
29+
# * Designed to be callable from a Justfile recipe or a nightly CI
30+
# workflow. No interactive prompts, ever.
31+
32+
set -euo pipefail
33+
34+
ECHIDNA_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
35+
CORPORA_DIR="${ECHIDNA_CORPORA_DIR:-$ECHIDNA_ROOT/external_corpora}"
36+
FORCE=0
37+
38+
# ------------------------------------------------------------------
39+
# Upstream catalogue
40+
#
41+
# Each entry: "<name>|<kind>|<url>|<subpath?>"
42+
# kind = git — `git clone --depth=1 <url> <CORPORA_DIR>/<name>`
43+
# kind = tar — `curl <url> | tar xz` into <CORPORA_DIR>/<name>
44+
# kind = skip — metadata only (proprietary / form-gated / non-public)
45+
#
46+
# Adding a source:
47+
# 1. Add a row here with the real upstream URL.
48+
# 2. Update scripts/extract_<name>.jl to read from external_corpora/<name>.
49+
# ------------------------------------------------------------------
50+
CATALOGUE=(
51+
# Interactive proof assistants
52+
"abella|git|https://github.com/abella-prover/abella"
53+
"agda-stdlib|git|https://github.com/agda/agda-stdlib"
54+
"agda-cubical|git|https://github.com/agda/cubical"
55+
"agda-unimath|git|https://github.com/UniMath/agda-unimath"
56+
"arend|git|https://github.com/JetBrains/Arend"
57+
"CoqGym|git|https://github.com/princeton-vl/CoqGym"
58+
"mathcomp|git|https://github.com/math-comp/math-comp"
59+
"mathcomp-analysis|git|https://github.com/math-comp/analysis"
60+
"mathcomp-finmap|git|https://github.com/math-comp/finmap"
61+
"mathcomp-algebra-tactics|git|https://github.com/math-comp/algebra-tactics"
62+
"mathlib3|git|https://github.com/leanprover-community/mathlib"
63+
"mathlib4|git|https://github.com/leanprover-community/mathlib4"
64+
"hol4|git|https://github.com/HOL-Theorem-Prover/HOL"
65+
"hol_light|git|https://github.com/jrh13/hol-light"
66+
"fstar|git|https://github.com/FStarLang/FStar"
67+
"idris2|git|https://github.com/idris-lang/Idris2"
68+
"matita|git|https://github.com/rocq-prover/matita"
69+
"mizar|git|https://github.com/MizarProject/mml"
70+
"metamath|git|https://github.com/metamath/set.mm"
71+
"opentheory|git|https://github.com/gilith/opentheory"
72+
"pvs|git|https://github.com/nasa/pvslib"
73+
"afp|git|https://foss.heptapod.net/isa-afp/afp-devel.git"
74+
75+
# ACL2 family
76+
"acl2|git|https://github.com/acl2/acl2"
77+
"acl2s|git|https://github.com/acl2s/acl2s"
78+
79+
# Auto-active verifiers
80+
"dafny|git|https://github.com/dafny-lang/dafny"
81+
"why3|git|https://gitlab.inria.fr/why3/why3"
82+
"boogie|git|https://github.com/boogie-org/boogie"
83+
"cameleer|git|https://github.com/ocaml-gospel/cameleer"
84+
"framac|git|https://git.frama-c.com/pub/frama-c"
85+
"viper|git|https://github.com/viperproject/silver"
86+
"key|git|https://github.com/KeYProject/key"
87+
88+
# Model checkers / CI verifiers
89+
"cbmc|git|https://github.com/diffblue/cbmc"
90+
"seahorn|git|https://github.com/seahorn/seahorn"
91+
"spin|git|https://github.com/nimble-code/Spin"
92+
"prism|git|https://github.com/prismmodelchecker/prism-examples"
93+
"nusmv|skip|http://nusmv.fbk.eu/distrib/" # distro ships examples
94+
"uppaal|skip|https://uppaal.org/documentation/" # commercial; examples gated
95+
"tlaplus_examples|git|https://github.com/tlaplus/Examples"
96+
97+
# SAT / SMT / FO-ATP benchmarks
98+
"abc|git|https://github.com/berkeley-abc/abc"
99+
"dreal4|git|https://github.com/dreal/dreal4"
100+
"smtlib|skip|https://smtlib.cs.uiowa.edu/benchmarks.shtml" # tarball index
101+
"sat_benchmarks|skip|https://www.satcompetition.org/" # annual tarballs
102+
"tptp|skip|https://www.tptp.org/" # form-free tarball
103+
104+
# Security protocol verifiers
105+
"tamarin|git|https://github.com/tamarin-prover/tamarin-prover"
106+
"proverif|git|https://gitlab.inria.fr/bblanche/proverif"
107+
108+
# Constraint / optimisation
109+
"alloy|git|https://github.com/AlloyTools/models"
110+
"minizinc|git|https://github.com/MiniZinc/minizinc-benchmarks"
111+
112+
# Logic frameworks / misc
113+
"dedukti|git|https://github.com/Deducteam/Libraries"
114+
"elpi-lang|git|https://github.com/LPCIC/elpi"
115+
"naproche|git|https://github.com/naproche/naproche"
116+
"mercury-lang|git|https://github.com/Mercury-Language/mercury"
117+
"nunchaku|git|https://github.com/nunchaku-inria/nunchaku"
118+
"athena|git|https://github.com/AthenaFoundation/athena"
119+
)
120+
121+
# ------------------------------------------------------------------
122+
123+
usage() {
124+
sed -n '4,25p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
125+
}
126+
127+
list_catalogue() {
128+
printf "%-28s %-5s %s\n" "NAME" "KIND" "URL"
129+
printf "%-28s %-5s %s\n" "----" "----" "---"
130+
for entry in "${CATALOGUE[@]}"; do
131+
IFS='|' read -r name kind url _ <<<"$entry"
132+
printf "%-28s %-5s %s\n" "$name" "$kind" "$url"
133+
done
134+
}
135+
136+
show_status() {
137+
local present=0
138+
local missing=0
139+
printf "%-28s %-9s %s\n" "NAME" "STATUS" "SIZE"
140+
printf "%-28s %-9s %s\n" "----" "------" "----"
141+
for entry in "${CATALOGUE[@]}"; do
142+
IFS='|' read -r name kind _ _ <<<"$entry"
143+
local path="$CORPORA_DIR/$name"
144+
if [[ -d "$path" ]]; then
145+
local size
146+
size="$(du -sh "$path" 2>/dev/null | awk '{print $1}')"
147+
printf "%-28s %-9s %s\n" "$name" "present" "$size"
148+
present=$((present + 1))
149+
elif [[ "$kind" == "skip" ]]; then
150+
printf "%-28s %-9s %s\n" "$name" "manual" "(gated upstream)"
151+
else
152+
printf "%-28s %-9s %s\n" "$name" "missing" "-"
153+
missing=$((missing + 1))
154+
fi
155+
done
156+
echo
157+
echo "Summary: $present present, $missing missing, $(( ${#CATALOGUE[@]} - present - missing )) manual."
158+
echo "Root: $CORPORA_DIR"
159+
}
160+
161+
find_entry() {
162+
local want="$1"
163+
for entry in "${CATALOGUE[@]}"; do
164+
IFS='|' read -r name _ _ _ <<<"$entry"
165+
if [[ "$name" == "$want" ]]; then
166+
echo "$entry"
167+
return 0
168+
fi
169+
done
170+
return 1
171+
}
172+
173+
provision_one() {
174+
local entry="$1"
175+
IFS='|' read -r name kind url _ <<<"$entry"
176+
local dest="$CORPORA_DIR/$name"
177+
178+
if [[ "$kind" == "skip" ]]; then
179+
echo " [skip] $name: provision manually from $url"
180+
return 0
181+
fi
182+
183+
if [[ -d "$dest" && $FORCE -eq 0 ]]; then
184+
echo " [ok] $name: already present at $dest"
185+
return 0
186+
fi
187+
188+
if [[ -d "$dest" && $FORCE -eq 1 ]]; then
189+
echo " [force] removing $dest"
190+
rm -rf "$dest"
191+
fi
192+
193+
mkdir -p "$CORPORA_DIR"
194+
195+
case "$kind" in
196+
git)
197+
echo " [clone] $name <- $url"
198+
if ! git clone --depth=1 --filter=blob:none "$url" "$dest" 2>&1 | tail -n 3; then
199+
echo " [retry] $name"
200+
sleep 2
201+
if ! git clone --depth=1 "$url" "$dest" 2>&1 | tail -n 3; then
202+
echo " [FAIL] $name: clone failed; continuing"
203+
return 1
204+
fi
205+
fi
206+
;;
207+
tar)
208+
echo " [tar] $name <- $url"
209+
mkdir -p "$dest"
210+
if ! curl -fsSL "$url" | tar xz -C "$dest" --strip-components=1; then
211+
echo " [FAIL] $name: tarball extraction failed; continuing"
212+
return 1
213+
fi
214+
;;
215+
*)
216+
echo " [WARN] unknown kind '$kind' for $name"
217+
return 1
218+
;;
219+
esac
220+
echo " [done] $name"
221+
}
222+
223+
provision_all() {
224+
local ok=0 fail=0 skip=0
225+
for entry in "${CATALOGUE[@]}"; do
226+
IFS='|' read -r _ kind _ _ <<<"$entry"
227+
if [[ "$kind" == "skip" ]]; then
228+
skip=$((skip + 1))
229+
provision_one "$entry" || true
230+
continue
231+
fi
232+
if provision_one "$entry"; then
233+
ok=$((ok + 1))
234+
else
235+
fail=$((fail + 1))
236+
fi
237+
done
238+
echo
239+
echo "Provisioning complete: $ok ok, $fail failed, $skip manual."
240+
}
241+
242+
# ------------------------------------------------------------------
243+
244+
case "${1:-}" in
245+
""|--help|-h)
246+
usage
247+
exit 0
248+
;;
249+
--list)
250+
list_catalogue
251+
exit 0
252+
;;
253+
--status)
254+
show_status
255+
exit 0
256+
;;
257+
--all)
258+
shift
259+
[[ "${1:-}" == "--force" ]] && { FORCE=1; shift; }
260+
provision_all
261+
;;
262+
--force)
263+
FORCE=1
264+
shift
265+
if [[ "${1:-}" == "--all" ]]; then
266+
shift
267+
provision_all
268+
else
269+
for name in "$@"; do
270+
entry="$(find_entry "$name")" || { echo "unknown source: $name (run --list)"; exit 2; }
271+
provision_one "$entry" || true
272+
done
273+
fi
274+
;;
275+
*)
276+
for name in "$@"; do
277+
entry="$(find_entry "$name")" || { echo "unknown source: $name (run --list)"; exit 2; }
278+
provision_one "$entry" || true
279+
done
280+
;;
281+
esac

0 commit comments

Comments
 (0)