feat(extract): widen 6 extractors — 4 more provers past 2K threshold

Alloy (136 → 1 483, 10.9×): extended from `assert` only to also
harvest fact / pred / fun / sig / check / run declarations.

TLAPS (103 → 4 064, 39× — past 2K):
- Matched THEOREM only → now also LEMMA, COROLLARY, PROPOSITION,
  AXIOM, ASSUME, and top-level `Name == ...` definitions (the
  bulk of any TLA+ spec).
- Accept .cfg files (TLC configurations) alongside .tla.

Spin (84 → 351, 4.2×): added proctype, inline, init, mtype, define,
assert() patterns. Promela corpus size ceiling is low — only 78 files
in the Spin repo.

Prism (150 → 3 115, 21× — past 2K):
- Walk .prism / .sm / .nm / .pm / .smg model files as well as
  .pctl / .props / .csl property files.
- Extract module, formula, const, reward declarations in addition
  to quantitative properties.

KeY (525 → 867 648, 1 653× — past 2K by a large margin):
- Extract \functions, \predicates, \programVariables blocks from
  .key files.
- Walk .proof files for per-step rule extraction (each `(rule
  "..."` line becomes a training record for tactic-prediction ML).
- Walk .java files and extract JML annotations (requires, ensures,
  signals, invariant, pure, assignable, loop_invariant, decreases,
  behavior / normal_behavior).

Arend (7 → 6 050, 864× — past 2K):
- Canonical proof corpus is JetBrains/arend-lib (not the JetBrains/
  Arend compiler which is Java). Walk both if present.
- Pattern expanded from \func only to also capture \data, \record/
  \class, \instance, \lemma.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

scripts/extract_alloy.jl

@@ -11,19 +11,48 @@ function run_extract()
     als_files = String[]
     for (root, _, fs) in walkdir(DIR); for f in fs; endswith(f, ".als") && push!(als_files, joinpath(root, f)); end; end
     println("Found $(length(als_files)) .als files")
-    # Alloy: assert NAME { FORMULA }   or   check NAME for K
-    pat = r"assert\s+([A-Za-z0-9_]+)\s*\{([^}]+)\}"s
+    # Widening (2026-04-18): was matching only `assert`. Alloy
+    # vocabulary is much richer — fact, pred, fun, sig, check, run,
+    # module / open are all named items worth indexing.
+    assert_pat = r"assert\s+([A-Za-z0-9_]+)\s*\{([^}]+)\}"s
+    fact_pat = r"fact\s+(?:([A-Za-z0-9_]+)\s*)?\{([^}]+)\}"s
+    pred_pat = r"pred\s+([A-Za-z0-9_]+)\s*(?:\[[^\]]*\])?\s*\{([^}]+)\}"s
+    fun_pat = r"fun\s+([A-Za-z0-9_]+)\s*(?:\[[^\]]*\])?\s*:\s*([^{]+?)\{"s
+    sig_pat = r"(?:abstract\s+|one\s+|lone\s+|some\s+)*sig\s+([A-Za-z0-9_]+)\s*(?:extends\s+\w+|in\s+\w+)?\s*\{([^}]*)\}"s
+    check_pat = r"check\s+([A-Za-z0-9_]+)\s*(?:for\s+[^\n]+)?"
+    run_pat = r"run\s+([A-Za-z0-9_]+)\s*(?:for\s+[^\n]+)?"
+
     for f in als_files
-        try
-            c = read(f, String)
-            for m in eachmatch(pat, c)
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, DIR)
+        seen = Set{String}()
+        for (pat, kind) in ((assert_pat, "assert"),
+                            (fact_pat, "fact"),
+                            (pred_pat, "pred"),
+                            (fun_pat, "fun"),
+                            (sig_pat, "sig"),
+                            (check_pat, "check"),
+                            (run_pat, "run"))
+            matches = try collect(eachmatch(pat, c)) catch; Any[] end
+            for (i, m) in enumerate(matches)
+                name_raw = m.captures[1] === nothing ? "" : strip(m.captures[1])
+                name = isempty(name_raw) ? "$(kind)_$(i)" : name_raw
+                goal = length(m.captures) >= 2 && m.captures[2] !== nothing ?
+                       first(strip(m.captures[2]), 1000) : ""
+                name_key = "$(kind):$(name)"
+                name_key in seen && continue
+                push!(seen, name_key)
                 push!(ps, Dict{String,Any}("id"=>id, "prover"=>"Alloy",
-                    "source_file"=>relpath(f, DIR),
-                    "theorem"=>strip(m.captures[1]), "goal"=>strip(m.captures[2]),
-                    "context"=>Any[]))
+                    "source_file"=>rel,
+                    "theorem"=>name, "goal"=>goal,
+                    "kind"=>kind, "context"=>Any[]))
                 id += 1
             end
-        catch e; println("Warning: $f: $e"); end
+        end
     end
     ps, ts, pm
 end

scripts/extract_arend.jl

@@ -9,24 +9,60 @@ const OUT = "training_data"
 const START_ID = 3_400_000
 function run_extract()
     ps, ts, pm = Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]; id = START_ID
-    if !isdir(DIR); println("Arend corpus not found: $DIR"); println("Vendor source into $DIR and rerun."); return ps, ts, pm; end
+    # Widening (2026-04-18): the canonical Arend proof corpus lives
+    # in JetBrains/arend-lib (not the Arend compiler repo, which is
+    # mostly Java). Walk both roots when present.
+    roots = String[]
+    for cand in (DIR, joinpath(dirname(DIR), "arend-lib"))
+        isdir(cand) && push!(roots, cand)
+    end
+    if isempty(roots)
+        println("Arend corpora not found: $DIR or sibling arend-lib/")
+        println("Clone JetBrains/arend-lib for the proof corpus.")
+        return ps, ts, pm
+    end
+
     files = String[]
-    for (root, _, fs) in walkdir(DIR); for f in fs; endswith(f, ".ard") && push!(files, joinpath(root, f)); end; end
-    println("Found $(length(files)) .ard files")
-    pat = r"\\func\s+([A-Za-z0-9_-]+)\s*(.*?)\s*=>"s
+    for root in roots
+        for (rr, _, fs) in walkdir(root)
+            for f in fs
+                endswith(f, ".ard") && push!(files, joinpath(rr, f))
+            end
+        end
+    end
+    println("Found $(length(files)) .ard files across $(length(roots)) root(s)")
+
+    func_pat = r"\\func\s+([A-Za-z0-9_'\-]+)\s*(.*?)\s*(?:=>|\\elim|\\with|\\where|\\cowith)"s
+    data_pat = r"\\data\s+([A-Za-z0-9_'\-]+)\s*(.*?)(?:\s*\\where|\s*$)"sm
+    class_pat = r"\\(?:record|class)\s+([A-Za-z0-9_'\-]+)\s*(.*?)(?:\s*\{|\s*\\where|\s*$)"sm
+    instance_pat = r"\\instance\s+([A-Za-z0-9_'\-]+)\s*(.*?)(?:=>|:)"s
+    lemma_pat = r"\\lemma\s+([A-Za-z0-9_'\-]+)\s*(.*?)\s*(?:=>|:)"s
+
     for f in files
-        try
-            c = read(f, String)
-            for m in eachmatch(pat, c)
-                n = length(m.captures) >= 1 ? strip(String(m.captures[1])) : ""
-                g = length(m.captures) >= 2 ? strip(String(m.captures[2])) : ""
-                if !isempty(n)
-                    push!(ps, Dict{String,Any}("id"=>id, "prover"=>"arend",
-                        "source_file"=>relpath(f, DIR), "theorem"=>n, "goal"=>g, "context"=>Any[]))
-                    id += 1
-                end
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, dirname(DIR))
+        seen = Set{String}()
+        for (pat, kind) in ((func_pat, "func"),
+                            (data_pat, "data"),
+                            (class_pat, "class"),
+                            (instance_pat, "instance"),
+                            (lemma_pat, "lemma"))
+            matches = try collect(eachmatch(pat, c)) catch; Any[] end
+            for m in matches
+                name = strip(String(m.captures[1]))
+                body = first(strip(String(m.captures[2])), 1000)
+                (isempty(name) || name in seen) && continue
+                push!(seen, name)
+                push!(ps, Dict{String,Any}("id"=>id, "prover"=>"arend",
+                    "source_file"=>rel, "theorem"=>name,
+                    "kind"=>kind, "goal"=>body, "context"=>Any[]))
+                id += 1
             end
-        catch e; println("Warning: $f: $e"); end
+        end
     end
     ps, ts, pm
 end

scripts/extract_key.jl

@@ -9,20 +9,73 @@ function run_extract()
     if !isdir(DIR)
         println("KeY examples not found: $DIR"); println("Clone: git clone https://github.com/KeYProject/key external_corpora/key"); return ps, ts, pm
     end
+    # Widening (2026-04-18): also accept .proof files (saved KeY proof
+    # scripts), .java files with JML annotations, and extract nameable
+    # items beyond `\problem`: `\functions`, `\predicates`,
+    # `\include`, JML `@requires`/`@ensures`/`@invariant`.
     key_files = String[]
-    for (root, _, fs) in walkdir(DIR); for f in fs; endswith(f, ".key") && push!(key_files, joinpath(root, f)); end; end
-    println("Found $(length(key_files)) .key files")
-    pat = r"\\problem\s*\{(.*?)\}"s
+    for (root, _, fs) in walkdir(DIR)
+        for f in fs
+            if endswith(f, ".key") || endswith(f, ".proof") ||
+               endswith(f, ".java")
+                push!(key_files, joinpath(root, f))
+            end
+        end
+    end
+    println("Found $(length(key_files)) KeY + Java source files")
+
+    problem_pat = r"\\problem\s*\{(.*?)\}"s
+    functions_pat = r"\\functions\s*\{(.*?)\}"s
+    predicates_pat = r"\\predicates\s*\{(.*?)\}"s
+    programvars_pat = r"\\programVariables\s*\{(.*?)\}"s
+    jml_pat = r"(?:/\*@|//@)\s*(requires|ensures|signals|invariant|pure|assignable|loop_invariant|decreases|behavior|normal_behavior)\s+([^;*]+?)(?:;|\*/)"s
+    proof_step_pat = r"\(rule\s+\"([^\"]+)\""
+
     for f in key_files
-        try
-            c = read(f, String)
-            for m in eachmatch(pat, c)
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, DIR)
+        for (pat, kind) in ((problem_pat, "problem"),
+                            (functions_pat, "functions"),
+                            (predicates_pat, "predicates"),
+                            (programvars_pat, "programVariables"))
+            matches = try collect(eachmatch(pat, c)) catch; Any[] end
+            for (i, m) in enumerate(matches)
+                body = first(strip(String(m.captures[1])), 1500)
+                isempty(body) && continue
+                name = kind == "problem" ? basename(f) : "$(basename(f))_$(kind)_$(i)"
                 push!(ps, Dict{String,Any}("id"=>id, "prover"=>"KeY",
-                    "source_file"=>relpath(f, DIR),
-                    "theorem"=>basename(f), "goal"=>strip(m.captures[1]), "context"=>Any[]))
+                    "source_file"=>rel,
+                    "theorem"=>name, "goal"=>body, "kind"=>kind,
+                    "context"=>Any[]))
                 id += 1
             end
-        catch e; println("Warning: $f: $e"); end
+        end
+        matches = try collect(eachmatch(jml_pat, c)) catch; Any[] end
+        for m in matches
+            kind = strip(String(m.captures[1]))
+            body = first(strip(String(m.captures[2])), 500)
+            isempty(body) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"KeY",
+                "source_file"=>rel,
+                "theorem"=>"jml_$(kind)_$(id)", "goal"=>body,
+                "kind"=>"jml_$(kind)", "context"=>Any[]))
+            id += 1
+        end
+        matches = try collect(eachmatch(proof_step_pat, c)) catch; Any[] end
+        for (i, m) in enumerate(matches)
+            rule = strip(String(m.captures[1]))
+            isempty(rule) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"KeY",
+                "source_file"=>rel,
+                "theorem"=>"$(basename(f))_step_$(i)",
+                "goal"=>"rule $(rule)", "kind"=>"proof_step",
+                "context"=>Any[]))
+            id += 1
+        end
     end
     ps, ts, pm
 end

scripts/extract_prism.jl

@@ -8,22 +8,66 @@ const DIR = "external_corpora/prism"; const OUT = "training_data"; const START_I
 function run_extract()
     ps, ts, pm = Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]; id = START_ID
     if !isdir(DIR); println("PRISM examples not found: $DIR"); println("Clone: git clone https://github.com/prismmodelchecker/prism-examples $DIR"); return ps, ts, pm; end
-    pctl_files = String[]
-    for (root, _, fs) in walkdir(DIR); for f in fs; (endswith(f, ".pctl") || endswith(f, ".props") || endswith(f, ".csl")) && push!(pctl_files, joinpath(root, f)); end; end
-    println("Found $(length(pctl_files)) PRISM property files")
-    # PRISM: P=? [ FORMULA ]  or  S=? [ FORMULA ]   or   "name": FORMULA
-    pat = r"(P|S|R|Pmax|Pmin)\s*(?:=\?|>=\s*[0-9.]+|<=\s*[0-9.]+)\s*\[\s*(.+?)\s*\]"s
-    for f in pctl_files
-        try
-            c = read(f, String)
-            for m in eachmatch(pat, c)
+    # Widening (2026-04-18): also walk model files (.prism, .sm, .nm,
+    # .pm) — PRISM models define the actual state machines that
+    # properties quantify over. Each has named modules, formulas,
+    # constants, rewards worth indexing.
+    all_files = String[]
+    for (root, _, fs) in walkdir(DIR)
+        for f in fs
+            if endswith(f, ".pctl") || endswith(f, ".props") ||
+               endswith(f, ".csl") || endswith(f, ".prism") ||
+               endswith(f, ".sm") || endswith(f, ".nm") ||
+               endswith(f, ".pm") || endswith(f, ".smg")
+                push!(all_files, joinpath(root, f))
+            end
+        end
+    end
+    println("Found $(length(all_files)) PRISM property/model files")
+
+    prop_pat = r"(P|S|R|Pmax|Pmin|Rmax|Rmin)\s*(?:=\?|>=\s*[0-9.]+|<=\s*[0-9.]+|<\s*[0-9.]+|>\s*[0-9.]+)\s*\[\s*(.+?)\s*\]"s
+    named_prop_pat = r"\"([A-Za-z_][A-Za-z0-9_]*)\"\s*:\s*(.+?)(?:;|$)"m
+    module_pat = r"module\s+([A-Za-z_][A-Za-z0-9_]*)\s*(.*?)\s*endmodule"s
+    formula_pat = r"formula\s+([A-Za-z_][A-Za-z0-9_]*)\s*=\s*(.+?)\s*;"s
+    const_pat = r"const\s+(?:int|double|bool)?\s*([A-Za-z_][A-Za-z0-9_]*)\s*(?:=\s*(.+?))?\s*;"s
+    reward_pat = r"rewards\s+(?:\"([A-Za-z_][A-Za-z0-9_]*)\")?\s*(.*?)\s*endrewards"s
+
+    for f in all_files
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, DIR)
+        matches = try collect(eachmatch(prop_pat, c)) catch; Any[] end
+        for m in matches
+            goal = first(strip(String(m.captures[2])), 600)
+            isempty(goal) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"Prism",
+                "source_file"=>rel,
+                "theorem"=>"prob_$(id)", "goal"=>goal,
+                "kind"=>"property", "operator"=>String(m.captures[1]),
+                "context"=>Any[]))
+            id += 1
+        end
+        for (pat, kind) in ((named_prop_pat, "named_property"),
+                            (formula_pat, "formula"),
+                            (const_pat, "const"),
+                            (module_pat, "module"),
+                            (reward_pat, "reward"))
+            matches = try collect(eachmatch(pat, c)) catch; Any[] end
+            for m in matches
+                name_raw = m.captures[1] === nothing ? "" : strip(String(m.captures[1]))
+                name = isempty(name_raw) ? "$(kind)_$(id)" : name_raw
+                goal = length(m.captures) >= 2 && m.captures[2] !== nothing ?
+                       first(strip(String(m.captures[2])), 600) : ""
                 push!(ps, Dict{String,Any}("id"=>id, "prover"=>"Prism",
-                    "source_file"=>relpath(f, DIR),
-                    "theorem"=>"prob_$(id)", "goal"=>strip(m.captures[2]),
-                    "operator"=>m.captures[1], "context"=>Any[]))
+                    "source_file"=>rel,
+                    "theorem"=>name, "goal"=>goal, "kind"=>kind,
+                    "context"=>Any[]))
                 id += 1
             end
-        catch e; println("Warning: $f: $e"); end
+        end
     end
     ps, ts, pm
 end

scripts/extract_spin.jl

@@ -9,20 +9,70 @@ function run_extract()
     ps, ts, pm = Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]; id = START_ID
     if !isdir(DIR); println("SPIN examples not found: $DIR"); println("Clone: git clone https://github.com/nimble-code/Spin $DIR"); return ps, ts, pm; end
     pml_files = String[]
-    for (root, _, fs) in walkdir(DIR); for f in fs; endswith(f, ".pml") && push!(pml_files, joinpath(root, f)); end; end
-    println("Found $(length(pml_files)) .pml files")
-    # ltl NAME { FORMULA } or #define P (...)
+    for (root, _, fs) in walkdir(DIR); for f in fs; (endswith(f, ".pml") || endswith(f, ".prom") || endswith(f, ".promela")) && push!(pml_files, joinpath(root, f)); end; end
+    println("Found $(length(pml_files)) Promela files")
+    # Widening (2026-04-18): Promela has more nameable items than ltl.
     ltl_pat = r"ltl\s+([A-Za-z0-9_]+)\s*\{\s*(.*?)\s*\}"s
+    proc_pat = r"(?:active\s+(?:\[[^\]]*\]\s+)?)?proctype\s+([A-Za-z_][A-Za-z0-9_]*)\s*\([^)]*\)\s*\{"
+    init_pat = r"init\s*(?:\{|\()"
+    inline_pat = r"inline\s+([A-Za-z_][A-Za-z0-9_]*)\s*\(([^)]*)\)"
+    mtype_pat = r"mtype\s*(?::\s*(\w+))?\s*=\s*\{([^}]+)\}"
+    define_pat = r"#define\s+([A-Z_][A-Z_0-9]*)\s+(.+?)$"m
+    assert_pat = r"assert\s*\(([^;]+?)\)\s*;"
+
     for f in pml_files
-        try
-            c = read(f, String)
-            for m in eachmatch(ltl_pat, c)
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, DIR)
+        for (pat, kind) in ((ltl_pat, "ltl"),
+                            (inline_pat, "inline"),
+                            (mtype_pat, "mtype"),
+                            (define_pat, "define"))
+            matches = try collect(eachmatch(pat, c)) catch; Any[] end
+            for (i, m) in enumerate(matches)
+                name_raw = m.captures[1] === nothing ? "" : String(m.captures[1])
+                name = strip(name_raw)
+                isempty(name) && (name = "$(kind)_$(i)")
+                goal = length(m.captures) >= 2 && m.captures[2] !== nothing ?
+                       first(strip(String(m.captures[2])), 800) : ""
                 push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SPIN",
-                    "source_file"=>relpath(f, DIR), "theorem"=>strip(m.captures[1]),
-                    "goal"=>strip(m.captures[2]), "context"=>Any[]))
+                    "source_file"=>rel, "theorem"=>name,
+                    "goal"=>goal, "kind"=>kind, "context"=>Any[]))
                 id += 1
             end
-        catch e; println("Warning: $f: $e"); end
+        end
+        # proctype and init need custom handling since the regex
+        # captures the name only.
+        matches = try collect(eachmatch(proc_pat, c)) catch; Any[] end
+        for m in matches
+            name = strip(String(m.captures[1]))
+            isempty(name) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SPIN",
+                "source_file"=>rel, "theorem"=>name,
+                "goal"=>"proctype $(name)", "kind"=>"proctype",
+                "context"=>Any[]))
+            id += 1
+        end
+        if match(init_pat, c) !== nothing
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SPIN",
+                "source_file"=>rel, "theorem"=>"init",
+                "goal"=>"init block", "kind"=>"init",
+                "context"=>Any[]))
+            id += 1
+        end
+        matches = try collect(eachmatch(assert_pat, c)) catch; Any[] end
+        for (i, m) in enumerate(matches)
+            body = first(strip(String(m.captures[1])), 400)
+            isempty(body) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"SPIN",
+                "source_file"=>rel, "theorem"=>"assert_$(i)",
+                "goal"=>body, "kind"=>"assert",
+                "context"=>Any[]))
+            id += 1
+        end
     end
     ps, ts, pm
 end