fix(extract_mathlib4): unwrap double-Regex in premise match

hyperpolymath · claude · hyperpolymath · commit b777b53b10ea · 2026-04-24T19:08:43.000+01:00
`hyp_patterns` already holds compiled `r"..."` Regex values; wrapping
them in `Regex(...)` again fails with MethodError on Julia 1.12 and
crashed every file, emitting 0 premise records. Pass the Regex
straight to `eachmatch`.

Co-Authored-By: Claude Opus 4.7 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/scripts/extract_mathlib4.jl b/scripts/extract_mathlib4.jl
@@ -108,7 +108,7 @@ function extract_mathlib4_proofs()
                         ]
                         proof_text = !isnothing(by_match) ? strip(by_match.captures[1]) : ""
                         for hyp_pattern in hyp_patterns
-                            for hyp_match in eachmatch(Regex(hyp_pattern), proof_text)
+                            for hyp_match in eachmatch(hyp_pattern, proof_text)
                                 hyps = [strip(h) for h in split(hyp_match.captures[1], ',')]
                                 for hyp in hyps
                                     if !isempty(hyp) && length(hyp) < 50

Original file line number	Diff line number	Diff line change
`@@ -108,7 +108,7 @@ function extract_mathlib4_proofs()`
`108`	`108`	`]`
`109`	`109`	`proof_text = !isnothing(by_match) ? strip(by_match.captures[1]) : ""`
`110`	`110`	`for hyp_pattern in hyp_patterns`
`111`		`- for hyp_match in eachmatch(Regex(hyp_pattern), proof_text)`
	`111`	`+ for hyp_match in eachmatch(hyp_pattern, proof_text)`
`112`	`112`	`hyps = [strip(h) for h in split(hyp_match.captures[1], ',')]`
`113`	`113`	`for hyp in hyps`
`114`	`114`	`if !isempty(hyp) && length(hyp) < 50`