Repository navigation
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 actionable defect was found in the reviewed changes. SummaryNarrows private imports and replaces broad proof automation in
Reviews (1) · Last reviewed commit: "Optimize ConwayRefinement private import..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 3,510 tracked declarations across 225 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: 22,218,617 → 22,108,615 (-110,001, -0.5%). Commands: 8,863 → 8,863. Per-file wall sum: 3119.8 s → 3597.3 s (+15.3%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 221 compared — 5 cheaper, 9 costlier, 207 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: 1,135,734 maxHeartbeats units across 1 valid file (33 added LOC). Sum of Count-heartbeats wall-clock total: 113.35 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 | private import pruning and proof rewrites |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
The refactor makes dependencies narrower and mathematical arguments more explicit without losing reusable structure or introducing brittle automation.
Tokens: 5,144,402 in / 16,418 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $20.8239 (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.
ConwayRefinement's 775-module aggregate took about 24 minutes to build in the controlled baseline. This pass narrows private dependencies and replaces expensive general proof automation with direct mathematical arguments. The final paired clean build took 20:39.19 versus 24:19.11, an observed 15.07% reduction in wall time on the VM.
The target is an existing completed project with about 150,000 lines and a large import closure. A separate baseline native profile attributed 4.36 seconds to generic congruence in the monomial Leibniz proof, providing a concrete proof-elaboration hotspot alongside the import work.
lake shakeannotations.ringfor pure associativity/commutativity withac_rfl.The change is confined to 225 existing Lean files in ConwayRefinement. Existing mathematical statements, definitions, instances, notation, namespaces and exported declarations are preserved. Original proof steps are retained where changing them would disturb generated private declaration names or types.
Base:
d1019ceec2f68c6ff2eaa59a413bc20b3fceac0b.Head:
2371d531db7fc6b3bd6ecfef0444cf4bbb000994.origin/mainwas refetched immediately before commit and still equals the measured base.Before editing, the base source hashes and compiled environment were saved. The invariant audit walks each module's own
ModuleData.constantsrather than looking names up in the merged environment, so colliding names in different modules are checked independently. It compares structural expression DAGs, including binder names/annotations, ordered universe parameters, declaration kind, safety, reducibility, all non-theorem values, and inductive/constructor/recursor metadata and computation rules. Only theorem proof bodies and expression source metadata are omitted.Result: all 15,483 pre-existing declaration records match exactly; none are removed or changed. Two supporting declarations are added: the private finite-sum helper and the generated
intCoeffRingHom.congr_simplemma. Independent source audits also find no changed signatures, preserve 104 non-theorem source blocks in proof-edited files, and confirm the public import/export closure is unchanged.The primary comparison is the consecutive repeated-baseline/optimized pair: wall time decreases 15.07%, CPU time 5.67%, and process peak RSS 0.88%. Both builds compile all 775 project modules freshly. Only this project's build products are removed; dependencies and the compiler linter plugin are prebuilt. Both use the unchanged pin from the measured main snapshot: Lean 4.35.0, Mathlib
56a005855ea17e0b0958f73ec801ae140b0a1679.Validation passed: warning-free complete project build; slow declaration linters for all 775 modules; Mathlib style; selected-project header, forbidden-text, size, reachability, metadata/card and generated-index checks; compiled axiom and option-backdoor audits; main-declaration checks; source/API audits; and
git diff --check. Every changed module has a fresh recorded build time and passes the unchanged 600-second limit; the largest changed-module time is 40 seconds. The pool discovery root, project aggregate and repository configuration match the base.The audit harness, raw manifests, measurements, source fingerprints and logs are retained on the VM in
/data/codex/scratch/lean4lean4/optimization-20261113/. The manifest comparison usesManifestDAG.leanandcompare_dag_manifests.py; the final result ismanifest-final-diff.json. Base manifest SHA-256:1985df9bd49e5ee396dc4b8c38b58e85ce6f5c24ec7afc77d701b198d3a8b66a. Head manifest SHA-256:f74a47ca431e281aed7728b4df70974ebc175810c38c0a461353438d4827bc66.These are local measurements on a shared VM, with fixed CPU affinity but no exclusive reservation. Hosted CI and independent review still need to pass on the required revisions. This PR is for review; this cycle does not request queue entry or auto-merge.