Repository navigation
Optimize LeanModularForms proof elaboration - #698
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking defect was found in the proof changes or private-import removals. SummaryThis PR narrows proof searches across
Reviews (1) · Last reviewed commit: "Optimize LeanModularForms proof elaborat..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 2,921 tracked declarations across 122 modified files kept their type; only proofs / definition bodies changed. Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 20,674,479 → 16,314,715 (-4,359,764, -21.1%). Commands: 7,187 → 7,187. Per-file wall sum: 2080.8 s → 1756.6 s (-15.6%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 122 compared — 87 cheaper, 0 costlier, 35 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%). Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from disjoint root command traces with
Advisory only — never blocks merge. Full log uploaded as the |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "c1cabfd5a66380143891085980d5d20ba47f4c56",
"summary": "This refactor replaces broad proof search with explicit arithmetic and simplifier inputs, reuses direct analytic lemma chains, and removes private imports while retaining the public interfaces. The inverse/conjugation reflection proof and the eta differentiability proofs expose the mathematical argument more directly.",
"assessment": {
"scope": "proof search restriction, analytic lemma reuse and private import pruning",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The complete 122-file refactor improves maintainability without an actionable new robustness problem."
},
"verdict": "approve",
"findings": [],
"validation": {
"source_review": "All 642 changed hunks reviewed across the team; full base/head Git hashes and boundaries checked. No independent build or reproduction of the author's compiled-manifest/timing audit.",
"advisory_profile": "Comment6303807189 reports all122 files compared:20,674,479 to16,314,715 heartbeats,87 cheaper/0 costlier/35 within noise. Wall-time measurements remain noisy; the report is advisory.",
"own_CI": "Run39511302121/core118932858698 remains pending complete validation.",
"independent_configured_review": "Existing automatic job2241 at this exact head is queued; no duplicate request.",
"integration": "Source assessment is favorable. Configured review, complete current-head CI and every normal protection/native-queue requirement still apply."
}
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof elaboration optimization and private-import pruning |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
Explicit proof dependencies and preserved argument structure improve maintainability without introducing actionable technical debt.
Tokens: 5,305,564 in / 7,586 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $21.3360 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
1 participant
LeanModularForms spends substantial time searching large local contexts for arithmetic and simplification proofs and synthesizing routine analytic properties. This constrains those searches to explicit facts and replaces several expensive arguments with direct Mathlib lemma chains. It also removes 45 redundant private imports identified by
lake shake --force --keep-public --explain.The selected project has 190 modules and 67,906 baseline source lines. The source hashes of all 190 modules match the source profile used for selection (about 756 seconds in summed module durations), which identified the analytic and geometric bottlenecks addressed here. The exact base is
66f6943c594e459c4d2bd2901d66f6f6ab677f8b. The repository's pinned Lean/Mathlib4.35.0-rc3is used throughout.Concrete changes include inverse/conjugation and norm invariance for the complex reflection argument; direct differentiability/composition lemmas for exponential series and eta products; explicit square-root and chord bounds; direct interval/set arguments; and bounded arithmetic and simplifier inputs.
The invariant audit imports the complete project at Lean's private environment level and serializes every kernel declaration's name, declaration kind, universe parameters, fully elaborated expression tree, safety flags, inductive/constructor/recursor metadata, and every non-theorem body. Only expression metadata is omitted; theorem proof bodies may change. It covers public, private, and compiler-generated declarations. All 6,865 pre-existing declarations compare identically on the audited fields, with zero removed. The resulting environment contains 496 additional generated proof helpers. A separate textual audit finds no changed signatures or binder names; all public imports are preserved.
Elapsed samples: baseline 272.942 / 292.478 s; optimized 248.353 / 249.555 s.
The whole-project benchmark re-elaborates and kernel-checks every module against imports built from the same revision, using its generated Lake setup and pinned options. Each Lean process uses
-j1, with four compiler workers. The order is baseline → optimized → optimized → baseline, with two samples per revision and warm dependency artifacts. Elapsed figures are the complete sweep, CPU figures sum user+system time, and RSS averages each sweep’s largest individual compiler process. These measurements exclude cold dependency fetching and artifact/C emission; hosted CI timing is unmeasured. The VM is shared.The synchronous command profiler also confirms the following heartbeat reductions (the outer declaration command, in standard heartbeat units):
norm_shift_neg_inv_eqeta_logDeriv'tsum_uexp_contDiffOnavoids_chord_i_to_rhoavoids_chord_rho'_to_iValidation passed:
lake build LeanPool.LeanModularForms.Imports, with no warnings.lake exe runLinter --no-build LeanPool.LeanModularForms.Importsandlake exe lint-style LeanPool.LeanModularForms.Imports.lake exe mk_all --module --checkandgit diff --check.No merge or auto-merge is requested. Repository CI and independent review remain applicable.
Validated head:
c1cabfd5a66380143891085980d5d20ba47f4c56.