Repository navigation
Optimize ClassificationOfSurfaces elaboration and imports - #692
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 regression was found in the proof refactor or import cleanup. SummaryThis PR shortens proofs and removes private imports across 86 existing
No actionable regression was found. The project card and headline theorem were checked against the change scope. External source fidelity and the reported benchmark logs were not independently verified. Builds, linters and performance measurements were not rerun. Reviews (1) · Last reviewed commit: "Optimize ClassificationOfSurfaces elabor..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 5,270 tracked declarations across 86 modified files kept their type; only proofs / definition bodies changed. Also: 8 declarations added, 2 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another. ➕ Declarations added (8)
➖ Declarations removed (2)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 8,890,499 → 7,653,830 (-1,236,669, -13.9%). Commands: 7,839 → 7,853. Per-file wall sum: 1421.5 s → 1446.7 s (+1.8%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 82 compared — 12 cheaper, 1 costlier, 69 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
Per-project compile cost (top 2 of 2 projects by |Δ heartbeats|):
New files — absolute profileTotal heartbeats: — maxHeartbeats units across 0 valid files (66 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 |
|
/review Exact head: |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "This ClassificationOfSurfaces refactor replaces repeated barycentric-map unfolding with coordinate projection lemmas and shared affine identities, factors the chart-restriction comparison, and uses explicit arithmetic premises, direct terms and covering-map uniqueness in existing proofs. The shared helper placement and preserved public import facade improve maintainability. The advisory profile reports 13.9% fewer heartbeats across 82 valid file comparisons; four modified-file measurements failed, so it does not establish a complete project-wide speedup.",
"assessment": {
"scope": "Proof elaboration and private-import refactor",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The refactor exposes reusable mathematical steps and reduces unnecessary elaboration without an actionable maintenance regression."
},
"verdict": "approve",
"findings": []
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof refactoring and import cleanup |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
Shared interfaces and explicit proof steps reduce duplication and automation dependence without introducing actionable maintenance debt.
Tokens: 7,120,927 in / 25,389 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $28.8645 (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.
CI was not green for this commit at review time; this review does not replace CI.
1 participant
ClassificationOfSurfaces repeatedly unfolds barycentric maps and their certificates where coordinate formulas suffice. This refactor uses projection lemmas, shared affine identities and direct proofs, and removes 246 unused private imports across the existing project’s 134 modules (143,564 source lines at the base). Profiling identified adaptive affine proofs costing 172,244 and 99,555 heartbeats as concrete starting points.
IntrinsicComplexdependency.change, and constrain a reflexivity application.shake: keep-all. The aggregate transitive module closure remains 4,672 modules; the import cleanup removes redundant edges.Base:
2aaa7220788257635be774b855528c4f0be6f3bd. Optimized head:eaaddb0e9c4f72c30250eb58d8f1aa0ea573f0e9. Only 86 existing ClassificationOfSurfaces Lean files change (361 insertions, 605 deletions). Before committing, refreshedorigin/mainwas15542c175fbeeb83666dc46fc20c4f18f0783e12; the selected project, its card, contribution/review rules and dependency pins are unchanged since the measured base. The branch retains its validated base without a rebase. The pinned Lean 4.35.0-rc3, Mathlib, project card, generated aggregate, and pool index are unchanged.The pre-edit Lean environment manifest covers 16,961 existing declarations, including private and generated declarations. It serializes constructor-level expression DAGs, universe parameters, declaration kinds, safety and reducibility/constructor metadata, non-theorem values, and export visibility. Only theorem proof values are omitted. The comparison preserves every existing kernel type, non-theorem value and public name; no declarations or exports disappear. There are 14 supporting additions: six source lemmas and eight generated equation/simplification lemmas.
Of the original records, 16,953 are byte-identical. Every other raw difference was investigated: two anonymous instance binder labels reflect the verbatim relocation of the generic lemmas; four diagnostic source-position records map through unchanged source spans (−49 bytes in
FiniteCyclicWordReduction, −191 inFiniteCyclicWordReductionCore); two internal bound-variable hygiene counters change when arithmetic proofs elaborate differently. These differences affect neither kernel expressions modulo bound-variable names and diagnostic metadata nor any universe parameter, expression child/flag, declaration metadata or definition value. An independent source audit preserves all 7,758 existing source signatures and source binder names. Original-module visibility was also checked for the two moved lemmas and three lazily generated helpers whose owning module changed.Manifest SHA256:
d0f91e53f4f0f2ebaf3b3affa555e7abc2aca187ec8c20ee51beaf98311ce10b0268891cd1db53609881f31b8bedb2cb225899c64dddd17f8e5d0914bbcee052Final frozen-source measurements, clean builds in base → optimized → optimized → base order, with
LEAN_NUM_THREADS=2:Mean wall time: 446.655 → 394.970 seconds (11.57% lower). Mean user CPU: 929.065 → 838.820 seconds (9.71% lower). Maximum compiler RSS across each pair: 1,831,944 → 1,776,048 KiB (3.05% lower). All four builds passed and compiled all 134 modules. This final sequence meets the 10% wall-time target on this VM. The six-hour optimization window also elapsed before final validation.
These are observations on a shared 16-core VM, not a guarantee of the same speedup elsewhere. An earlier checkpoint measured 4.5% wall improvement with two compiler threads and 5.4% with the normal 16-thread setting; final-source performance at 16 threads was not remeasured. Scheduling noise remains a limitation.
For each clean measurement, only that isolated worktree’s
.lake/buildis deleted; both worktrees retain identical pinned prebuilt dependencies. The command is/usr/bin/time -v lake --wfail build LeanPool.ClassificationOfSurfaces.Imports, withLEAN_NUM_THREADSfixed to the table’s setting. No other Lean compiler jobs from this cycle run during a timing sequence. Peak RSS is GNU time’s maximum child-process RSS, not aggregate VM memory. Shared-VM scheduling limits precision; repeated runs and CPU time accompany wall time.Diagnostic theorem-command profiling (
-DElab.async=false, no raised limits) covers all 18 modules with proof changes, including every newly added helper: 3,132,603 → 1,995,522 heartbeats (36.30% lower) across 1,648 base and 1,654 optimized theorem commands. These totals cover the edited modules, not the entire project. Representative reductions are affine vertex evaluation (99,555 → 693), chart coordinate equivalence (61,806 → 605), and marked-token separation (50,414 → 938).Validation on the final source:
lake --wfail build LeanPool.ClassificationOfSurfaces.Imports: both optimized clean builds pass with warnings treated as errors.lake env lean --run scripts/ci/lint-project.lean <all 134 selected-project modules>: production Mathlib linter driver passes.lake exe lint-style LeanPool.ClassificationOfSurfaces.Imports: passes.uv run --project python --locked python /data/codex/scratch/vasilin97/optimization-20261020/check-project.py: selected-project execution of unchanged production quality functions passes: headers, forbidden constructs/options, proof/file sizes, card/main declarations, axiom closure and all-constant trust audit.Imports.leanmatches the production generator format exactly; the pool index is byte-identical to base.lake shake --force --keep-public LeanPool.ClassificationOfSurfaces.Imports: passes with no remaining suggestions;--forcebypasses the unrelated full-pool build preflight after the complete project build.git diff --checkpasses.Full-repository checks remain with protected CI. No gates, options, linter settings, waivers or unrelated projects change. Raw benchmark logs, the environment inspector, manifests, comparison/investigation reports, source audit and frozen checkpoints are retained under
/data/codex/scratch/vasilin97/optimization-20261020on the VM. Auto-merge is not enabled.