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. [Low impact] No blocking code issue was found in this proof-only refactor. SummarySplits three finite-table proofs into 24 private helpers, then joins their results with exhaustive cases on
Reviews (1) · Last reviewed commit: "Reduce Erdos97ConvexOctagon peak compile..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 44 tracked declarations across 2 modified files kept their type; only proofs / definition bodies changed. Also: 24 declarations 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 (24)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 73,961 → 79,129 (+5,168, +7.0%). Commands: 30 → 54. Per-file wall sum: 29.5 s → 19.5 s (-34.0%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 2 compared — 0 cheaper, 2 costlier, 0 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 |
Three finite-table audits in
Erdos97ConvexOctagonbuild large kernel reduction caches. Check each of the eight centres independently in 24 private helper theorems, then assemble the existing public results by explicit finite case analysis. The full project build's maximum compiler RSS falls 31.33%. This is a memory optimization; full-build wall time is essentially unchanged.The selected project has 268 source modules and approximately 5 MB of Lean, including 94 certificate-fact shards. Baseline sampling identified
CoveragePairRowIndexMaskSoundnessas its largest compiler process. That module's sampled peak falls from 2,476,996 to 1,401,652 KiB (43.41%). The pass also bounds the independent legal-row enumeration and pair-mask audits inCoverageSearchRowChoiceSoundness.Only two existing project files change: three theorem proof bodies and 24 new private helper theorems.
as_aux_lemmapreserves the original generated auxiliary declarations. Existing statements, definitions, public names, imports, namespaces, notation, metadata, project cards, indexes and toolchain pins are unchanged.Both timed runs used
LEAN_NUM_THREADS=4, shared already-built pinned dependencies, and removed only this isolated worktree's selected-project Lean/IR artifacts before running:The 31.33% result is GNU time's maximum RSS of an individual compiler process across the complete project build. Sampled aggregate concurrent compiler memory improved only 0.48%, and wall time increased 0.30%; no aggregate-memory or build-speed improvement is claimed. This VM also runs unrelated jobs. Initial uncontrolled-concurrency baseline wall time was 329.12 seconds and is excluded from the controlled comparison.
Compatibility audit: before editing, a standalone Lean program imported the base environment with extensions disabled and enumerated every constant owned by every project module through
Environment.header.moduleData.constNames. It recorded public/private/generated names, owning module, declaration kind, exact elaborated type, universe parameters, safety, and exact non-theorem values. Full serialized expression records are retained; SHA-256 digests are used for comparison. After the optimized full build, all 4,066 original constants match exactly in every audited field. There are no missing declarations and no changed records, including generated private auxiliaries. The 48 additions are safe private theorem constants: 24 explicit helpers plus their kernel auxiliaries. A separate source audit recovers both original files byte-for-byte after reversing only these three proof-body rewrites and removing the new helper blocks.Validation passed:
lake env lean --run scripts/ci/lint-project.lean <all project modules>.lake exe lint-style LeanPool.Erdos97ConvexOctagon.Imports.python -m lean_pool.quality --repo <project inventory> --static-only.Quot.sound,Classical.choice, andpropext. The three pre-existing compiler-generated partial auxiliaries match the base exactly; no unsafe/partial declarations or axioms are added.lake exe mk_all --module --check; no generated changes needed.git diff --check.lake shake --keep-public --explainwas investigated; imports with reported dependencies were retained. A scratchcbvtrial exceeded its step limit and was discarded without raising limits or adding waivers.Base:
edbe5bd56f476cc2965564676b66199f281ab714. Head:6404adb824fdf9c6a3300fcf44d66e18e76c8c96. Uses current main's pinned Lean/Mathlib 4.35.0-rc3, unchanged. Whole-pool hosted validation and independent refactor review remain required. This PR is left open with auto-merge disabled; no merge or queue action is requested.Raw measurements, full compressed declaration records, manifests, and audit tools are retained on the Azure VM in
/data/codex/scratch/vilin/optimization-erdos97-20261024T1617/.