Skip to content

Commit d17ab3d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(extract): vendor + widen Tier B provers (Why3, PVS, F*, Idris2)
Each of these provers previously had a tiny curated downloader list (~10-15 files) and a mostly-empty external_corpora/ dir, yielding 100-250 records each. Vendored upstreams: - Why3: gitlab.inria.fr/why3/why3 (1 539 .mlw/.why files) - PVS: SRI-CSL/PVS (214 .pvs files) - F*: FStarLang/FStar sparse (448 .fst/.fsti files) - Idris2: idris-lang/Idris2 sparse (1 596 .idr files) Each extractor now walks its upstream clone (external_corpora/<p>_full/) recursively in addition to the existing downloader cache. F* also accepts .fsti (interface) files; Why3 accepts .why library files in addition to .mlw. Fixed two correctness bugs along the way: - extract_fstar.jl + extract_why3.jl: eachmatch(Regex(pat, "s"), ...) where pat is already a Regex — never worked on any file that reached the body, crashing the moment a single match was attempted. - extract_why3.jl func_pattern: chains of .*? can catastrophically backtrack on large amalgamated files; wrapped eachmatch in try/catch so a pathological file skips rather than aborts the run. Rerun deltas: Why3 199 → 35 692 (+35 493, 179×) PVS 231 → 2 377 (+ 2 146, 10.3×) F* 76 → 3 046 (+ 2 970, 40×) Idris2 87 → 574 (+ 487, 6.6×) PVS, F*, Idris2 are still well below the 100 K target — the extractor gates are biased toward named lemmas with explicit specs and drop library-heavy definitional content. Further uplift needs per-language filter relaxation, tracked as follow-up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 60e27f8 commit d17ab3d

4 files changed

Lines changed: 109 additions & 29 deletions

File tree

‎scripts/extract_fstar.jl‎

Lines changed: 27 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ function parse_fstar_file(filepath::String)::Vector{Dict{String,Any}}
6262

6363
# val declarations with refinement types
6464
val_pattern = r"val\s+(\w+)\s*:\s*(.*?)(?=\nval\s|\nlet\s|\ntype\s|\nopen\s|\nmodule\s|\z)"s
65-
for m in eachmatch(Regex(val_pattern, "s"), content)
65+
for m in eachmatch(val_pattern, content)
6666
name = strip(m.captures[1])
6767
sig = replace(strip(m.captures[2]), r"\s+" => " ")
6868
sig = sig[1:min(400, length(sig))]
@@ -80,7 +80,7 @@ function parse_fstar_file(filepath::String)::Vector{Dict{String,Any}}
8080

8181
# let with refinement types or Lemma
8282
let_pattern = r"let\s+(?:rec\s+)?(\w+)\s*(?::.*?)?\s*=\s*(.*?)(?=\nlet\s|\nval\s|\ntype\s|\z)"s
83-
for m in eachmatch(Regex(let_pattern, "s"), content)
83+
for m in eachmatch(let_pattern, content)
8484
name = strip(m.captures[1])
8585
body = replace(strip(m.captures[2]), r"\s+" => " ")
8686
body = body[1:min(300, length(body))]
@@ -236,16 +236,35 @@ function run()::Tuple{Int,Int}
236236
downloaded = download_fstar_files()
237237
println(" Downloaded/cached $downloaded files")
238238

239+
# Widening (2026-04-18): also walk a sparse FStarLang/FStar clone
240+
# at external_corpora/fstar_full/ with ulib/ + examples/ checked
241+
# out. Accepts .fst (source) and .fsti (interface) files.
242+
src_files = String[]
239243
for fname in readdir(EXTERNAL_DIR)
240-
if endswith(fname, ".fst")
241-
fpath = joinpath(EXTERNAL_DIR, fname)
242-
parsed = parse_fstar_file(fpath)
243-
append!(all_entries, parsed)
244-
if !isempty(parsed)
245-
println(" Parsed $(length(parsed)) from $fname")
244+
(endswith(fname, ".fst") || endswith(fname, ".fsti")) &&
245+
push!(src_files, joinpath(EXTERNAL_DIR, fname))
246+
end
247+
full_root = joinpath(dirname(EXTERNAL_DIR), "fstar_full")
248+
if isdir(full_root)
249+
println("[F*] Walking full clone at $(full_root) ...")
250+
for (root, _dirs, files) in walkdir(full_root)
251+
for fname in files
252+
(endswith(fname, ".fst") || endswith(fname, ".fsti")) &&
253+
push!(src_files, joinpath(root, fname))
246254
end
247255
end
248256
end
257+
println(" $(length(src_files)) F* source files to parse")
258+
259+
processed = 0
260+
for fpath in src_files
261+
parsed = parse_fstar_file(fpath)
262+
append!(all_entries, parsed)
263+
processed += 1
264+
if processed % 100 == 0
265+
println(" processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
266+
end
267+
end
249268
extracted_count = length(all_entries)
250269

251270
println("[F*] Phase 2: Generating synthetic proofs ...")

‎scripts/extract_idris2.jl‎

Lines changed: 23 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -244,16 +244,33 @@ function run()::Tuple{Int,Int}
244244
downloaded = download_idris2_files()
245245
println(" Downloaded/cached $downloaded files")
246246

247+
# Widening (2026-04-18): also walk a sparse idris-lang/Idris2
248+
# clone at external_corpora/idris2_full/ with libs/ + tests/
249+
# checked out.
250+
src_files = String[]
247251
for fname in readdir(EXTERNAL_DIR)
248-
if endswith(fname, ".idr")
249-
fpath = joinpath(EXTERNAL_DIR, fname)
250-
parsed = parse_idris2_file(fpath)
251-
append!(all_entries, parsed)
252-
if !isempty(parsed)
253-
println(" Parsed $(length(parsed)) from $fname")
252+
endswith(fname, ".idr") && push!(src_files, joinpath(EXTERNAL_DIR, fname))
253+
end
254+
full_root = joinpath(dirname(EXTERNAL_DIR), "idris2_full")
255+
if isdir(full_root)
256+
println("[Idris2] Walking full clone at $(full_root) ...")
257+
for (root, _dirs, files) in walkdir(full_root)
258+
for fname in files
259+
endswith(fname, ".idr") && push!(src_files, joinpath(root, fname))
254260
end
255261
end
256262
end
263+
println(" $(length(src_files)) Idris2 source files to parse")
264+
265+
processed = 0
266+
for fpath in src_files
267+
parsed = parse_idris2_file(fpath)
268+
append!(all_entries, parsed)
269+
processed += 1
270+
if processed % 200 == 0
271+
println(" processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
272+
end
273+
end
257274
extracted_count = length(all_entries)
258275

259276
println("[Idris2] Phase 2: Generating synthetic proofs ...")

‎scripts/extract_pvs.jl‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -242,16 +242,32 @@ function run()::Tuple{Int,Int}
242242
downloaded = download_pvs_files()
243243
println(" Downloaded/cached $downloaded files")
244244

245+
# Widening (2026-04-18): also walk a full SRI-CSL/PVS clone at
246+
# external_corpora/pvs_full/ when present.
247+
src_files = String[]
245248
for fname in readdir(EXTERNAL_DIR)
246-
if endswith(fname, ".pvs")
247-
fpath = joinpath(EXTERNAL_DIR, fname)
248-
parsed = parse_pvs_file(fpath)
249-
append!(all_entries, parsed)
250-
if !isempty(parsed)
251-
println(" Parsed $(length(parsed)) theorems from $fname")
249+
endswith(fname, ".pvs") && push!(src_files, joinpath(EXTERNAL_DIR, fname))
250+
end
251+
full_root = joinpath(dirname(EXTERNAL_DIR), "pvs_full")
252+
if isdir(full_root)
253+
println("[PVS] Walking full clone at $(full_root) ...")
254+
for (root, _dirs, files) in walkdir(full_root)
255+
for fname in files
256+
endswith(fname, ".pvs") && push!(src_files, joinpath(root, fname))
252257
end
253258
end
254259
end
260+
println(" $(length(src_files)) PVS source files to parse")
261+
262+
processed = 0
263+
for fpath in src_files
264+
parsed = parse_pvs_file(fpath)
265+
append!(all_entries, parsed)
266+
processed += 1
267+
if processed % 50 == 0
268+
println(" processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
269+
end
270+
end
255271
extracted_count = length(all_entries)
256272

257273
println("[PVS] Phase 2: Generating synthetic proofs ...")

‎scripts/extract_why3.jl‎

Lines changed: 37 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ function parse_why3_file(filepath::String)::Vector{Dict{String,Any}}
7171

7272
# Extract lemma/goal declarations
7373
pattern = r"(lemma|goal|axiom)\s+(\w+)\s*:\s*(.*?)(?=\n\s*(?:lemma|goal|axiom|let|val|predicate|function|end|use|module)|\z)"si
74-
for m in eachmatch(Regex(pattern), content)
74+
for m in eachmatch(pattern, content)
7575
kind = strip(m.captures[1])
7676
name = strip(m.captures[2])
7777
body = first(replace(strip(m.captures[3]), r"\s+" => " "), 300)
@@ -94,9 +94,17 @@ function parse_why3_file(filepath::String)::Vector{Dict{String,Any}}
9494
))
9595
end
9696

97-
# Extract function specs (ensures/requires)
97+
# Extract function specs (ensures/requires). Wrap in try/catch:
98+
# the `.*?` chains in func_pattern can catastrophically backtrack
99+
# on large amalgamated library files — skipping the whole file on
100+
# PCRE match-limit error is strictly better than aborting the run.
98101
func_pattern = r"let\s+(?:rec\s+)?(\w+).*?(?:requires\s*\{(.*?)\})?.*?(?:ensures\s*\{(.*?)\})"s
99-
for m in eachmatch(Regex(func_pattern), content)
102+
func_matches = try
103+
collect(eachmatch(func_pattern, content))
104+
catch e
105+
Any[]
106+
end
107+
for m in func_matches
100108
name = m.captures[1]
101109
requires = m.captures[2]
102110
ensures = m.captures[3]
@@ -286,16 +294,36 @@ function run()::Tuple{Int,Int}
286294
downloaded = download_why3_files()
287295
println(" Downloaded/cached $(downloaded) files")
288296

297+
# Widening (2026-04-18): additionally walk a full clone of the
298+
# Why3 project at external_corpora/why3_full/ (canonical source
299+
# is gitlab.inria.fr/why3/why3.git). Accepts .mlw (source) and
300+
# .why (library) files.
301+
src_files = String[]
289302
for fname in readdir(EXTERNAL_DIR)
290-
if endswith(fname, ".mlw")
291-
fpath = joinpath(EXTERNAL_DIR, fname)
292-
parsed = parse_why3_file(fpath)
293-
append!(all_entries, parsed)
294-
if !isempty(parsed)
295-
println(" Parsed $(length(parsed)) theorems from $(fname)")
303+
(endswith(fname, ".mlw") || endswith(fname, ".why")) &&
304+
push!(src_files, joinpath(EXTERNAL_DIR, fname))
305+
end
306+
full_root = joinpath(dirname(EXTERNAL_DIR), "why3_full")
307+
if isdir(full_root)
308+
println("[Why3] Walking full clone at $(full_root) ...")
309+
for (root, _dirs, files) in walkdir(full_root)
310+
for fname in files
311+
(endswith(fname, ".mlw") || endswith(fname, ".why")) &&
312+
push!(src_files, joinpath(root, fname))
296313
end
297314
end
298315
end
316+
println(" $(length(src_files)) Why3 source files to parse")
317+
318+
processed = 0
319+
for fpath in src_files
320+
parsed = parse_why3_file(fpath)
321+
append!(all_entries, parsed)
322+
processed += 1
323+
if processed % 200 == 0
324+
println(" processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
325+
end
326+
end
299327
extracted_count = length(all_entries)
300328

301329
println("[Why3] Phase 2: Generating synthetic proofs ...")

0 commit comments

Comments
 (0)