Repository navigation
Exposition: LML extraction methodology + verified minimal files (207/238) - #283
Conversation
…files Rebuilds the minimal-Lean-file pipeline as a faithful port of Rémy Degenne's LMLExposition extractor (leanmachinelearning.org's exposition; github.com/LeanMachineLearning/exposition), replacing the previous textual-heuristic replay. Fixes the user-reported failure on LeanModularForms (dangling `variable (hΓ : Γ.width ∣ h)` from a namespace block with no kept declarations) and two whole failure classes. - Extractor: each module is re-elaborated against its project's environment (`IO.processCommands`; declarations fail fast as already declared), classifying every top-level command from real syntax with byte-exact ranges: theorem proofs are cut at the `declVal` node, `by`-blocks inside definition values become `sorry`, `variable` commands carry per-binder decompositions, notation commands carry their kinds and expansion dependencies, and `elab`/`macro` commands replay as context. Dependency recovery per LML: coercion instances (unfolded out of elaborated terms), notation expansions (embedded `Name` data), and structure field defaults. Extraction runs per-project (scripts/exposition/extract-all.sh): a whole-pool environment superposes all projects' parser extensions, and foreign notations tokenize other projects' identifiers, silently truncating re-parsed commands. - Shards (schema 1.3): moduleData carries the per-module command tables; the builder slices fetched source bytes with the precomputed edits. - minimal.js: ported assembly — per-target filtering, per-binder variable pruning with bound-name and namespace-prefix awareness, `open NS (…)` trimming, namespace stubs, dotted-namespace scope arity, empty-scope stripping, and the notation-usage closure. - Validation: 8 rounds of really-compiling generated files against Mathlib oleans; final suite 17/22 across 14 projects (was 13/20 at best before the port), including the reported LMF case, with the elaboration-consumed-instance and tactic-brittle-definition failure classes eliminated. Remaining: three small known items and two deep tails (vendored logic DSL replay, section-variable-heavy algebra), documented in the generated file header. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | repository exposition infrastructure |
| Mode | mixed |
| Obscure problem | no |
| Code quality | 4 / 5 |
This is not a mathematics contribution, but it is a substantial infrastructure improvement to a user-facing documentation feature with source anchoring to LMLExposition and a verification harness.
Tokens: 46,255 in / 1,743 out · Tier: flex · Cost: $0.1418
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Push the minimal-Lean-file builder from a 17/22 sample to a verified 193/238 (81%) across every main_declarations entry in the pool, and add the harness that keeps score: - Extract.lean: per-member surgery for mutual blocks, registration/tactic commands (macro/elab/syntax/attr registrations) always classified as context, end-scope names captured for dotted `end A.B`, syntactic deps scoped to each module's import closure. - minimal.js: two-pass assembly that extends the cone with binder references instead of pruning variables, locally-registered attribute stripping, `omit ... in` handling, wholesale inclusion of notation modules, per-component namespace/end splitting. - verify.py + build-minimal.mjs: assemble each headline theorem with the real client builder under node and compile it against the built pool; report.json lists every failure. - exposition-verify.yml: weekly + on-PR compilation gate for the exposition pipeline. Verified locally: 193/238 headline declarations compile end-to-end; the remaining 45 are DSL-replay and section-variable tails tracked by the new gate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Vilin97
changed the title
…vironment The CI gate ran `lake env` from python/, which is not the Lake workspace root, so `lean` got an empty LEAN_PATH and all 244 targets failed at `import Mathlib` — reported as 1/244 rather than as a setup error. Resolve LEAN_PATH at the repository root before entering python/, and add a preflight that compiles `import Mathlib` first and aborts with the fix instructions instead of emitting a report full of false failures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Fixes driven by a root-cause classification of all 45 failing files. The recurring theme: a minimal file is not a topological sort of the dependency cone. Dependency edges come from the elaborated term while the file is re-elaborated from surface syntax, and the non-declaration commands (`variable`, `open`, `section`/`end`, attribute registrations) are positional and stateful rather than referential. - source_text.py: `_IMPORT_RE` now matches the module system's `public`/`meta`/`private import` and `import all`. 668 import lines in the pool were invisible, so affected projects recorded no imports at all, the module DAG collapsed, and emission order degenerated to alphabetical — MisereGames emitted `inductive Player` ~1960 lines after its first use. - generate.py: order modules by walking the project's entry module and emitting each module after the ones it imports, instead of alphabetically. Both orders are topologically legal; only one reproduces the environment the code was written against (Polylean's `groupRingMul` otherwise hijacks `binop%` elaboration and suppresses an coercion). - Extract.lean: classify `Mathlib.Tactic.scopedNS` as a notation command, and map each range start to every name declared there — `irreducible_def` declares two constants at one range and last-write-wins dropped one. - minimal.js: split dotted `section A.B` into one frame per component so the matching `end A.B` pops what was pushed; resolve `Class.field` tokens to the owning declaration; record syntax-only wholesale modules as involved. Two changes that looked right were measured and reverted, with the results recorded in comments: making the wholesale-module rule monotone regressed 7 targets against 2 fixed, and adding elaborator-body constants to notation dependencies was net negative. Larger cones drag in instances that break elaboration elsewhere. Verified end-to-end: 207/238 assemble and compile against the built pool, 14 newly fixed and no regressions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Vilin97
changed the title
A gate that stays red until 100% carries no signal — a real regression looks identical to the known tail. --baseline fails only when the passing count drops below the recorded number, and prints the new figure to lock in when it rises. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Greptile SummaryThis PR rebuilds the minimal-Lean-file pipeline on Rémy Degenne's LMLExposition methodology: the Lean extractor now emits per-module command tables alongside the declaration dump, and a new pure-JS builder (
Confidence Score: 4/5The PR is safe to merge; all three findings are non-blocking quality notes rather than functional regressions. The core pipeline is thoughtfully designed and well-commented. All three findings are non-blocking: missing OSError catch in _compile_one, abbreviations in the shell script, and a hard-coded baseline that won't auto-ratchet. None affect the 207/238 result or the normal CI path. Files Needing Attention:
|
| Filename | Overview |
|---|---|
| python/lean_pool/exposition/verify.py | New verification harness: builds minimal files via Node and compiles with lean; the preflight guard is well-designed, but _compile_one doesn't catch OSError so a mid-run lean failure skips writing report.json. |
| python/lean_pool/exposition/static/assets/minimal.js | Major rewrite porting LMLExposition's assembly phases; IIFE exports correctly for both browser and Node require; notation-fixpoint loop and scope-stack reconstruction are well-documented. |
| scripts/exposition/Extract.lean | Substantially extended to produce per-module command tables (JSONL) in addition to the declaration dump; source-replay per-project extraction is well-commented. |
| scripts/exposition/extract-all.sh | New per-project parallel extraction driver; lean_cmd / out_cmds abbreviate against the naming convention. |
| .github/workflows/exposition-verify.yml | New weekly + PR-path workflow gate; --baseline 207 is functional but requires manual ratcheting as more tests pass. |
| python/lean_pool/exposition/generate.py | Added read_command_tables and _remap_command_entries to pipe the new extractor command tables through to shards. |
| scripts/exposition/build-minimal.mjs | New Node CLI bridge between verify.py and minimal.js; correctly uses createRequire for CommonJS interop. |
| python/lean_pool/exposition/source_text.py | Simplified to only export module imports and declaration statement slicing; ModuleSkeleton docstring updated. |
| .github/workflows/docs.yml | Switches extraction to per-project extract-all.sh; artifact wait deadline extended from 1800 to 2700 s. |
Reviews (2): Last reviewed commit: "Exposition: make the minimal-file gate a..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| with ThreadPoolExecutor(max_workers=jobs) as pool: | ||
| outcomes.extend( | ||
| pool.map(lambda item: _compile_one(lean_command, *item), compile_queue) | ||
| ) | ||
|
|
There was a problem hiding this comment.
OSError escapes pool.map → report.json never written
_compile_one catches subprocess.TimeoutExpired but not OSError (e.g. FileNotFoundError if the lean binary is unavailable, or PermissionError). When such an exception propagates through ThreadPoolExecutor.map, it is re-raised the moment outcomes.extend tries to consume the iterator — skipping the report.json write below. The Upload verification report step then uploads nothing, and the failure appears as an opaque Python traceback rather than a diagnostic compile report. Wrapping the subprocess.run call in _compile_one to also catch OSError and return Outcome(target, "compile", str(error)) would ensure the report is always written.
|
|
||
| out_dump="${1:-exposition-dump.jsonl}" | ||
| out_cmds="${2:-exposition-commands.jsonl}" | ||
| jobs="${EXTRACT_JOBS:-2}" |
There was a problem hiding this comment.
lean_cmd and out_cmds use shortened forms; the project naming convention (CLAUDE.md) requires full words (lean_command, out_commands). The companion env variable LEAN_CMD in the workflow YAML is a conventional all-caps env var name and is fine, but the lowercase shell-local names used inside the script should match the style guide.
Context Used: CLAUDE.md (source)
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
| --out ../exposition-verify \ | ||
| --jobs 2 \ | ||
| --lean /home/runner/.elan/bin/lean \ | ||
| --baseline 207 |
There was a problem hiding this comment.
--baseline 207 ensures the gate never fires when 208+ targets pass. The verify.py CLI already prints "raise --baseline to {passed} to lock in the gain" when the count exceeds the baseline, but there is nothing enforcing that update. Once 20 more targets are fixed in follow-up PRs, a regression of 19 passes would still not be caught. A comment in the workflow noting that this value must be manually ratcheted (or a small script that reads report.json and bumps it) would prevent silent drift.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
CI measured 214/245 passing on the merge of #283 — the branch was gated at 207, the count from a local run over a smaller target set. At 207 a six-target regression would have gone unnoticed. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
#293) An audit of all 148 reviews the bot has posted, against what actually happened to those PRs, says the project review was looking in the wrong place. **It approved a duplicate.** #275 (de Bruijn-Erdos compactness) came back `approve` / `good_fit` / 0 findings and was closed by hand: the headline follows in a few lines from Mathlib's `Finsubgraph`. #225 was likewise subsumed by the pool's own `Incompleteness`. REVIEW_RULES.md never had a duplication check — only the challenge rules did. **It could not see what the axiom gate misses.** #225's diagonal lemma was postulated as an `inductive` constructor, invisible to `#print axioms`; the review filed it as a card-wording nit. Same class: #215 (a rescaled surrogate tableau proved in place of the real one), #240 (a card informal that was false), #265 (a synthetic residue model presented as the geometry it models), #199 (NP-hardness claimed for a reduction-correctness result). **Infra PRs were graded for mathematical fit.** A .lean file under scripts/ clears the workflow's "touches Lean?" filter, so the exposition PRs landed on the project rules: #279 and #282 came back `not_a_fit`/`undergraduate`, #283 came back `good_fit`/`graduate`/`approve` over a summary opening "This is not a mathematics contribution." All three merged. So the project rules gain the four checks the challenge rules already had, adapted for finished proofs — claim-vs-Lean faithfulness, what is assumed rather than proved, prior art, and source fidelity — plus the generated-bulk criterion #278 was closed on after a 0-finding approval, and an AI-slop list. Tau Ceti and ArkLib converge on the same shape. Calibration fixes from the same audit: `obscure_problem` was `no` in all 147 project reviews and is gone; card metadata moves to out-of-scope (#216 and #243 were rejected on nothing else, then merged unchanged); a partial review may no longer `approve`, since code_quality cannot be scored on elided files; and the comment now says `request_changes` is an ask, not a close — 39% of those verdicts were merged after a human looked. Two of the four approve examples (sphere packing, Erdos 124) were not in the pool at all. The reviewer also now receives the PR title and description, which the rules have always allowed to carry the source anchor. Both are contributor-written, as is the diff, so they are fenced with a per-request random token and framed as claims to verify rather than instructions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Rebuilds the minimal-Lean-file pipeline on Rémy Degenne's LMLExposition methodology and adds an end-to-end compilation gate.
Verified
207 of 238 headline declarations (every
main_declarationsentry in the pool) now assemble with the real client builder and compile against the built pool — up from roughly 30% before this branch. Includes the user-reportedSubgroup.widthfailure in LeanModularForms and that project'svalence_formula_textbook_orbit_finsum.The remaining 31 are tracked by the new gate, which writes a
report.jsonnaming every failure.What changed
Extractor (Extract.lean) — source-replay extraction: each module's commands are re-elaborated per project, classified declaration vs context, and dumped with byte-exact edit ranges that replace proofs with
sorrywhile definitions keep their bodies.Client builder (minimal.js) — a pure module shared by the browser and node: byte-slice assembly, cone extension for binder references, scope-tree reconstruction with synthesized
endlines, notation-module inclusion.Verification harness —
python -m lean_pool.exposition.verifyassembles every headline declaration exactly as the browser does and compiles it;exposition-verify.ymlruns it weekly and on PRs touching the pipeline.Why this was hard
A minimal file is not a topological sort of the dependency cone. Dependency edges are harvested from the elaborated term while the file is re-elaborated from surface syntax, so erased coercion instances have no in-edges at all. A declaration's type can depend on its body, so sorrying changes signatures. A valid topological order is not unique and the tie-break is semantic. And some commands —
register_label_attr,initialize registerBuiltinAttribute— have no legal position in a single file, because they only take effect on import.Two plausible-looking fixes were measured and reverted rather than kept on principle: a monotone wholesale-module rule (7 regressions against 2 fixes) and elaborator-body notation dependencies (net negative). Both results are recorded in comments so they are not re-derived.
🤖 Generated with Claude Code