Part of #12 campaign.
Observation: ECHIDNA has 235 MB of CoqGym corpus at
`external_corpora/CoqGym/` but `stats_coqgym.json` reports only
14 records. This is a ~4-order-of-magnitude shortfall vs the roughly
70 K proof states CoqGym is known to contain.
Action: audit `scripts/extract_coqgym.jl`; likely a regex /
gating bug. Rerun after fix and confirm ≥ 50 K records before
moving on.
Size estimate: CoqGym upstream ≈ 70 K, mathcomp adds ≈ 15 K,
Iris adds ≈ 10 K → realistic target 100 K+ without vendoring
anything new.
Part of #12 campaign.
Observation: ECHIDNA has 235 MB of CoqGym corpus at
`external_corpora/CoqGym/` but `stats_coqgym.json` reports only
14 records. This is a ~4-order-of-magnitude shortfall vs the roughly
70 K proof states CoqGym is known to contain.
Action: audit `scripts/extract_coqgym.jl`; likely a regex /
gating bug. Rerun after fix and confirm ≥ 50 K records before
moving on.
Size estimate: CoqGym upstream ≈ 70 K, mathcomp adds ≈ 15 K,
Iris adds ≈ 10 K → realistic target 100 K+ without vendoring
anything new.