feat(extract): vendor ACL2 Community Books + MiniZinc benchmarks

ACL2 (277 → 170 455, 615×):
- Sparse clone acl2/acl2 at external_corpora/acl2_full/ with
  `books/` checked out (~ 13 478 .lisp files, 1.5 GB).
- Walk recursively alongside legacy curated cache.
- Accept .lisp and .acl2 files.
- Fix UTF-8 byte-index slice crash (switch to first(s, n)).
- ACL2 vaults to #2 corpus after Lean — Community Books are dense
  with named defthm declarations across hundreds of books.

MiniZinc (29 → 327, 11×):
- Clone MiniZinc/minizinc-benchmarks at external_corpora/minizinc_full/
  (~ 300 .mzn models + many .dzn data files).
- Walk recursively.
- Wrap three eachmatch calls in try/catch — large amalgamated data
  files caused PCRE catastrophic backtracking. Count growth limited
  by the extractor's gate (requires at least one variable or
  constraint); further uplift needs per-file lowering or data-file
  handling.

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

Author: hyperpolymath

scripts/extract_acl2.jl

@@ -74,7 +74,7 @@ function parse_acl2_file(filepath::String)::Vector{Dict{String,Any}}
         body = strip(m.captures[2])
         # Clean up body
         body_clean = replace(body, r"\s+" => " ")
-        body_clean = body_clean[1:min(300, length(body_clean))]
+        body_clean = first(body_clean, 300)
 
         # Extract hints
         hints_match = match(r":hints\s*\((.*?)\)"s, body)
@@ -251,16 +251,37 @@ function run()::Tuple{Int,Int}
     downloaded = download_acl2_files()
     println("  Downloaded/cached $downloaded files")
 
+    # Widening (2026-04-18): walk a sparse acl2/acl2 clone at
+    # external_corpora/acl2_full/ (only `books/` checked out). The
+    # ACL2 Community Books are the canonical proof corpus and hold
+    # tens of thousands of named theorems across hundreds of books.
+    # Accept .lisp and .acl2 files.
+    src_files = String[]
     for fname in readdir(EXTERNAL_DIR)
-        if endswith(fname, ".lisp")
-            fpath = joinpath(EXTERNAL_DIR, fname)
-            parsed = parse_acl2_file(fpath)
-            append!(all_entries, parsed)
-            if !isempty(parsed)
-                println("  Parsed $(length(parsed)) theorems from $fname")
+        (endswith(fname, ".lisp") || endswith(fname, ".acl2")) &&
+            push!(src_files, joinpath(EXTERNAL_DIR, fname))
+    end
+    full_root = joinpath(dirname(EXTERNAL_DIR), "acl2_full")
+    if isdir(full_root)
+        println("[ACL2] Walking full clone at $(full_root) ...")
+        for (root, _dirs, files) in walkdir(full_root)
+            for fname in files
+                (endswith(fname, ".lisp") || endswith(fname, ".acl2")) &&
+                    push!(src_files, joinpath(root, fname))
             end
         end
     end
+    println("  $(length(src_files)) ACL2 source files to parse")
+
+    processed = 0
+    for fpath in src_files
+        parsed = parse_acl2_file(fpath)
+        append!(all_entries, parsed)
+        processed += 1
+        if processed % 500 == 0
+            println("  processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
+        end
+    end
     extracted_count = length(all_entries)
 
     println("[ACL2] Phase 2: Generating synthetic proofs ...")

scripts/extract_minizinc.jl

@@ -66,17 +66,30 @@ function parse_mzn_file(filepath::String)::Vector{Dict{String,Any}}
 
     model_name = splitext(basename(filepath))[1]
 
-    # Extract variables
-    variables = [(m.captures[2], m.captures[1]) for m in eachmatch(r"var\s+([\w.]+)\s*:\s*(\w+)"i, content)]
+    # Each of these regexes can catastrophically backtrack on large
+    # data files or amalgamated benchmarks. Wrap each collection in
+    # a try/catch so a single pathological file just skips — the rest
+    # of the corpus still extracts.
+    variables = try
+        [(m.captures[2], m.captures[1]) for m in eachmatch(r"var\s+([\w.]+)\s*:\s*(\w+)"i, content)]
+    catch
+        Tuple{Any,Any}[]
+    end
 
-    # Extract constraints
-    constraints = [first(replace(strip(m.captures[1]), r"\s+" => " "), 200)
-                   for m in eachmatch(r"constraint\s+(.*?)\s*;"s, content)]
+    constraints = try
+        [first(replace(strip(m.captures[1]), r"\s+" => " "), 200)
+         for m in eachmatch(r"constraint\s+(.*?)\s*;"s, content)]
+    catch
+        String[]
+    end
 
-    # Extract objective
     objective = "satisfy"
-    for m in eachmatch(r"solve\s+(.*?)\s*;"s, content)
-        objective = first(replace(strip(m.captures[1]), r"\s+" => " "), 200)
+    try
+        for m in eachmatch(r"solve\s+(.*?)\s*;"s, content)
+            objective = first(replace(strip(m.captures[1]), r"\s+" => " "), 200)
+        end
+    catch
+        # keep default
     end
 
     if !isempty(variables) || !isempty(constraints)
@@ -320,16 +333,36 @@ function run()::Tuple{Int,Int}
     downloaded = download_mzn_files()
     println("  Downloaded/cached $(downloaded) files")
 
+    # Widening (2026-04-18): walk MiniZinc/minizinc-benchmarks at
+    # external_corpora/minizinc_full/ — the official benchmark suite
+    # with hundreds of real-world constraint models. Accepts .mzn
+    # (model) and .dzn (data) files.
+    src_files = String[]
     for fname in readdir(EXTERNAL_DIR)
-        if endswith(fname, ".mzn")
-            fpath = joinpath(EXTERNAL_DIR, fname)
-            parsed = parse_mzn_file(fpath)
-            append!(all_entries, parsed)
-            if !isempty(parsed)
-                println("  Parsed $(length(parsed)) models from $(fname)")
+        (endswith(fname, ".mzn") || endswith(fname, ".dzn")) &&
+            push!(src_files, joinpath(EXTERNAL_DIR, fname))
+    end
+    full_root = joinpath(dirname(EXTERNAL_DIR), "minizinc_full")
+    if isdir(full_root)
+        println("[MiniZinc] Walking full benchmark clone at $(full_root) ...")
+        for (root, _dirs, files) in walkdir(full_root)
+            for fname in files
+                (endswith(fname, ".mzn") || endswith(fname, ".dzn")) &&
+                    push!(src_files, joinpath(root, fname))
             end
         end
     end
+    println("  $(length(src_files)) MiniZinc source files to parse")
+
+    processed = 0
+    for fpath in src_files
+        parsed = parse_mzn_file(fpath)
+        append!(all_entries, parsed)
+        processed += 1
+        if processed % 500 == 0
+            println("  processed $(processed)/$(length(src_files)) files — running count: $(length(all_entries))")
+        end
+    end
     extracted_count = length(all_entries)
 
     println("[MiniZinc/Constraint Solvers] Phase 2: Generating synthetic models ...")