fix(extractors): UTF-8 byte indexing + empty-captures guards

extract_mathlib4.jl: `length(m.match)` counts characters but `content[]`
indexes bytes; fall back to `ncodeunits(m.match)` so multi-byte Lean
sources (Unicode operators) don't hit StringIndexError mid-file.

extract_hol4.jl: DISCH_TAC-style regex have zero capture groups; guard
`hyp_match.captures[1]` with `isempty(hyp_match.captures)` to stop the
crash that killed the premise pass after writing all 127k proof_states.

Corpus impact: hol4 now emits ~140k premise records, mathlib4 no longer
flags every file.

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

Author: hyperpolymath

scripts/extract_hol4.jl

@@ -542,6 +542,9 @@ function run()::Tuple{Int,Int}
         thm_name = entry["theorem"]
         for hyp_pattern in hol4_hyp_patterns
             for hyp_match in eachmatch(hyp_pattern, proof_text)
+                # `DISCH_TAC` et al. match without capturing; skip rather than
+                # indexing into an empty captures vector (BoundsError).
+                isempty(hyp_match.captures) && continue
                 raw = hyp_match.captures[1] === nothing ? "" : hyp_match.captures[1]
                 hyps = [strip(h) for h in split(raw, ',')]
                 for hyp in hyps

scripts/extract_mathlib4.jl

@@ -74,9 +74,12 @@ function extract_mathlib4_proofs()
                         )
                         push!(proof_states, proof_state)
 
-                        # Look for proof tactics (simplified)
-                        proof_start = m.offset + length(m.match)
-                        remaining_content = content[min(proof_start, end):end]
+                        # Look for proof tactics (simplified).  Use byte lengths:
+                        # `length(m.match)` counts characters, not bytes, and indexing
+                        # a `String` by a char index that lands mid-UTF-8 throws
+                        # StringIndexError — common for mathlib4 files with Unicode.
+                        proof_start = m.offset + ncodeunits(m.match)
+                        remaining_content = content[min(proof_start, ncodeunits(content)+1):end]
 
                         # Extract tactics from the "by" clause
                         by_match = match(r"by\s+([^\n]+)", remaining_content)