Repository navigation
Optimize LeanModularForms proofs and elaboration - #782
Conversation
Reuse calculus and Hecke-algebra lemmas, share FTC transport, and narrow proof searches and private imports while preserving all original declarations.
|
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 code issue was found; the separately required CI and independent review remain outstanding. SummaryThis refactor replaces repeated proof searches with explicit dependencies and library lemmas. It also shares integral transport between the two boundary proofs and removes private imports.
Reviews (1) · Last reviewed commit: "Optimize LeanModularForms proofs and ela..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 3,290 tracked declarations across 147 modified files kept their type; only proofs / definition bodies changed. Also: 1 declaration added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another. ➕ Declarations added (1)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 17,178,792 → 16,023,651 (-1,155,141, -6.7%). Commands: 8,063 → 8,064. Per-file wall sum: 1960.1 s → 1532.3 s (-21.8%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 145 compared — 81 cheaper, 3 costlier, 61 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
New files — absolute profileTotal heartbeats: — maxHeartbeats units across 0 valid files (75 added LOC). Sum of Count-heartbeats wall-clock total: 0.00 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Advisory only — never blocks merge. Full log uploaded as the |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof optimization and dependency cleanup |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
The refactor reduces duplicated proof machinery and implicit tactic dependencies while preserving useful proof structure and reusable helpers.
Tokens: 3,804,095 in / 6,938 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $15.3204 (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.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head c26c93c48f731f943964b5e5408afa6431fab801 under the refactor rubric. No blocking findings; the source is acceptable for protected integration.
The 147 changed files preserve existing written declaration headers and non-theorem values. All 190 public import lists are unchanged. The private import cleanup removes 84 edges and adds three, without removing project modules or changing gates.
The shared LogDerivFTC.intervalIntegrable_integral_eq_congr_ae correctly transports both integrability and the evaluated integral on the unordered interval. Its ten uses retain the left/right telescopes’ actual intervals, cutoff bounds, logarithm signs and endpoint cancellation. The iterated derivative proof keeps the integer translation, factorial and denominator formula while reusing the existing derivative API. The Hecke commutation and diagonal/matrix proofs likewise reuse the relevant library facts on the original objects. The remaining changes generally replace broad search with explicit facts or associative/commutative normalization; no material loss of proof structure was found.
The public profile reports 6.7% fewer heartbeats across 145 compared files. LeftEdge and RightEdge have no usable timings, so this does not establish a whole-project speedup or the stated 10% target. Profiling remains advisory.
The six applicable workflow namespaces pass at the reviewed head. I independently bound their actual checkout to these source changes combined with current main 2b205bf, including the full planned 190-module project and current control files. The configured refactor review also approves this exact head. Queue validation must still pass normally; no waiver or branch update is needed.
LeanModularForms repeatedly elaborates large arithmetic/simplifier contexts and duplicate FTC transport arguments. This pass replaces bespoke proofs with library lemmas, shares the FTC argument, and narrows elaboration dependencies while preserving every existing declaration.
The selected completed project has 190 owned modules and about 68,000 lines. Initial clean builds and declaration profiles identified expensive residue-limit, boundary, iterated-derivative and Hecke-algebra proofs, alongside redundant private imports.
Changes:
LogDerivFTC.intervalIntegrable_integral_eq_congr_aeand use it in both boundary FTC telescopes, removing repeated integrability/equality transport and redundant interval assembly.Invariant audit:
faac47acb64cd8e2022370e59892faf9f5688c43; head:c26c93c48f731f943964b5e5408afa6431fab801.b8bb0d01d000220303da39266dc6bc65eef1e2600ff6d49c4baacf380a100767. Final aggregate source SHA-256:8fbbd584ab157c69c8aec28a729dba17f2ba9b7a3a910de77aeeb55196604925.Measurements:
Observed mean wall reduction: 7.94%; user CPU reduction: 5.09%. Largest-child RSS reduction: -0.09%. Negative reductions denote increases.
Each sample deletes only this project's build/IR artifacts, retains the same warm pinned dependencies and lint plugin, and runs
/usr/bin/time -v env LEAN_NUM_THREADS=2 lake --wfail build LeanPool.LeanModularForms.Imports. The predeclared balanced order is head–base–base–head; all four samples are included, with no other Lean compiler from this task running concurrently. Settings and source hashes are recorded per sample. GNU time RSS is the largest child process, not total simultaneous build memory. Shared VM workloads limit timing precision.The six-hour optimization effort threshold was reached. The 10% whole-project wall/RAM target was not established. The significant hot-proof allocation reductions and reusable proof simplifications are the material improvements retained from the pass.
Final diagnostic allocation profiles covered 17 modules and 420 matched primitive theorem commands, with macro/include wrappers excluded. Examples:
aut_iter_deriv80.66% fewer allocations;mulVecLin_injective_of_det_ne_zero96.25%;cpv_at_endpoint50.54%; right/left FTC telescopes 44.44%/41.86%;EQ2278.06%. These are elaboration counters, not whole-project time or RAM measurements.Validation passed:
scripts/ci/lint-project.leanover all 190 owned modules;lake exe lint-style LeanPool.LeanModularForms.Imports.git diff --check.Uses the unchanged repository pins: Lean 4.35.0 and Mathlib
56a005855ea17e0b0958f73ec801ae140b0a1679. Only this project's Lean sources change. No index or card update is needed; no new modules are introduced. Whole-pool CI and independent refactor review remain required. The tested base is preserved rather than rebased to chase main; current main2b205bf904013a5e06d8ef03069430dd79e1c8bdhas identical selected-project sources/card, pins, applicable policies and validation tools.This optimization run does not request queue entry, auto-merge or a merge. Existing rollout and protected-review requirements remain in force.