feat(extract): unlock 7 more provers — Mercury/λProlog/Naproche/SAT trio/ABC

Vendored upstreams + extractor fixes for previously-empty provers:

  Mercury     0 → 13 173   (Mercury-Language/mercury, 2 794 .m files)
  Naproche    0 →  2 110   (naproche/naproche, sTeX .ftl.tex parser)
  λProlog     0 →  1 585   (teyjus/teyjus, 207 .mod files)
  CaDiCaL     0 →    313   (arminbiere/cadical + SAT-classical CNFs)
  Kissat      0 →    313   (same SAT corpus, mirrored)
  MiniSat     0 →    313   (same SAT corpus, mirrored)
  ABC         0 →      1   (placeholder — need proper benchmark source)

Naproche extractor fix: prior pattern required bare `.ftl` files with
`theorem NAME: ...` syntax. Real Naproche corpus ships as
`.ftl.tex` / `.ftl.en.tex` (sTeX literate form) with theorems in
\\begin{theorem}[forthel,title=...,name=...] blocks. Added both sTeX
env and legacy bare-ftl patterns.

SAT-benchmarks setup: consolidated 313 .cnf files from cadical +
kissat + SAT-classical test suites under external_corpora/sat_benchmarks/,
feeding the shared extract_sat_benchmarks.jl which emits per-prover
records for all three SAT backends.

Mercury + λProlog were pure vendoring — extractors already handled
the formats.

Three more provers past the 2K ML-useful threshold: Mercury, Naproche
(along with Boogie/SeaHorn/Frama-C from the earlier wave).

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

Author: hyperpolymath

scripts/extract_naproche.jl

@@ -11,22 +11,59 @@ function run_extract()
     ps, ts, pm = Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]; id = START_ID
     if !isdir(DIR); println("Naproche (ForTheL) corpus not found: $DIR"); println("Vendor source into $DIR and rerun."); return ps, ts, pm; end
     files = String[]
-    for (root, _, fs) in walkdir(DIR); for f in fs; endswith(f, ".ftl") && push!(files, joinpath(root, f)); end; end
-    println("Found $(length(files)) .ftl files")
-    pat = r"theorem\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"=>"naproche",
-                        "source_file"=>relpath(f, DIR), "theorem"=>n, "goal"=>g, "context"=>Any[]))
-                    id += 1
-                end
+    for (root, _, fs) in walkdir(DIR)
+        for f in fs
+            # Widening (2026-04-18): Naproche now publishes sources
+            # as .ftl.tex (sTeX literate form) rather than bare .ftl.
+            if endswith(f, ".ftl") || endswith(f, ".ftl.tex") ||
+               endswith(f, ".ftl.en.tex")
+                push!(files, joinpath(root, f))
             end
-        catch e; println("Warning: $f: $e"); end
+        end
+    end
+    println("Found $(length(files)) ForTheL files")
+
+    # sTeX/Naproche carries theorems in \begin{theorem}[forthel,
+    # title=TITLE, name=NAME] ... \end{theorem} blocks.
+    env_pat = r"\\begin\{(theorem|lemma|corollary|proposition|definition|axiom)\}(?:\[([^\]]*)\])?\s*(.*?)\\end\{\1\}"s
+    # Older bare-ftl: `Theorem NAME. BODY Proof. ... Qed.`
+    plain_pat = r"(Theorem|Lemma|Corollary|Proposition|Definition|Axiom)\s+([A-Za-z][A-Za-z0-9_ \-]*?)\.\s*(.*?)(?=\n\s*(?:Theorem|Lemma|Corollary|Proposition|Definition|Axiom|Proof|Qed)|\z)"s
+
+    for f in files
+        c = try
+            read(f, String)
+        catch
+            continue
+        end
+        rel = relpath(f, DIR)
+
+        matches = try collect(eachmatch(env_pat, c)) catch; Any[] end
+        for (i, m) in enumerate(matches)
+            kind = strip(m.captures[1])
+            opts = m.captures[2] === nothing ? "" : strip(m.captures[2])
+            body = first(strip(m.captures[3]), 2000)
+            name_match = match(r"name=([A-Za-z0-9_\-]+)", opts)
+            title_match = match(r"title=([^,\]]+)", opts)
+            name = name_match !== nothing ? strip(name_match.captures[1]) :
+                   title_match !== nothing ? replace(strip(title_match.captures[1]), r"\s+" => "_") :
+                   "$(kind)_$(i)"
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"naproche",
+                "source_file"=>rel, "theorem"=>name,
+                "kind"=>kind, "goal"=>body, "context"=>Any[]))
+            id += 1
+        end
+
+        matches = try collect(eachmatch(plain_pat, c)) catch; Any[] end
+        for m in matches
+            kind = strip(String(m.captures[1]))
+            name = replace(strip(String(m.captures[2])), r"\s+" => "_")
+            body = first(strip(String(m.captures[3])), 2000)
+            isempty(name) && continue
+            push!(ps, Dict{String,Any}("id"=>id, "prover"=>"naproche",
+                "source_file"=>rel, "theorem"=>name,
+                "kind"=>kind, "goal"=>body, "context"=>Any[]))
+            id += 1
+        end
     end
     ps, ts, pm
 end