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] The changes affect proof building across the DomainTheory library. No blocking defect was found; replacing the generated helper call would make the proof easier to maintain. Findings
SummaryRefactors
Vilin97 explicitly describes the finite intersection cases as intentional and the retained import prefix in Review covered the full diff and relevant source relationships. The reported timings and raw declaration audit were not independently rerun. External source fidelity, upstream license evidence, and Mathlib-wide prior art were not independently verified. Reviews (1) · Last reviewed commit: "Optimize DomainTheory imports and repeat..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| · have hsub : ({m} : Set ℕ) ⊆ {n} := | ||
| (flat.principal_le_iff (flat_mem_singleton n) (flat_mem_singleton m)).mp hle | ||
| simp_all | ||
| exact principal.congr_simp flat (congrArg singleton (hsub rfl)) (flat_mem_singleton m) |
There was a problem hiding this comment.
flat_atom_maximal now calls principal.congr_simp directly. This is a generated helper, so changes to how Lean generates congruence proofs can break this proof even when principal is unchanged. Derive m = n from hsub rfl, substitute it, and finish with rfl instead.
| exact principal.congr_simp flat (congrArg singleton (hsub rfl)) (flat_mem_singleton m) | |
| have hmn : m = n := hsub rfl | |
| subst m | |
| rfl |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 3,516 tracked declarations across 127 modified files kept their type; only proofs / definition bodies changed. Also: 4 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 (4)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 1,181,799 → 938,674 (-243,125, -20.6%). Commands: 4,885 → 4,888. Per-file wall sum: 499.9 s → 355.8 s (-28.8%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 120 compared — 29 cheaper, 0 costlier, 91 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 (215 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 |
DomainTheory repeatedly loads broad numeric-tactic dependencies and recomputes finite-set and functor facts. This refactor reduces that compilation work while preserving every pre-existing declaration. The completed project has 148 mathematical modules and about 51,000 lines, providing both import and proof-reuse opportunities.
Base:
edbe5bd56f476cc2965564676b66199f281ab714. Head:d8a4e4a1ff57584e2eab3617a079d850ab5a8fde.Changes:
shake: keep, and prune redundant import edges. The entry module uses 84 terminal public imports instead of 148, with the same transitive public module coverage.The declaration audit imports all 150 owned modules with
importAll, including private/generated declarations. It compares rawExprrepresentations of types and all non-theorem values, declaration kinds, universe parameters, safety, partiality, and names. Theorem proof bodies are the only omitted values. All 6,783 base declarations are retained with zero differences, without normalization exceptions. The head has 7,380 declarations: four new source support lemmas and 593 generated proof auxiliaries. Four canonicalcongr_simpcaches have different import-origin metadata; their names and types are unchanged. An independent source audit finds no statement, binder, definition-body, attribute, or other code edits outside theorem proofs/imports and the four new lemmas. All 218,113 old exported names remain; exactly the four support lemmas are added.LEAN_NUM_THREADSEach timing run starts with empty project build outputs and the same warm pinned dependency cache, using
env LEAN_NUM_THREADS=N lake --wfail build LeanPool.DomainTheory. The order is base/head/head/base/base/head, with three repetitions per revision. Both variants build the same 148 mathematical modules plus the entry module. The two-thread runs include the same lightweight process-tree sampler; the sixteen-thread runs use GNU time only. Source hashes are checked after restoring the optimized tree. The raw runs and medians are reported, without selecting the fastest run.Validation passed on the exact frozen source:
env LEAN_NUM_THREADS=2 lake --wfail build LeanPool.DomainTheory.Importslake env lean --run scripts/ci/lint-project.lean <all 150 owned modules>: 7,380 declarationslake exe lint-style LeanPool.DomainTheory.Importslake exe mk_all --module --checkandgit diff --checklake shake --force --keep-public --explain LeanPool.DomainTheorywas also run for import analysis. It reports remaining redundant imports; parser dependencies, public coverage, and the source-coordinate-sensitive prefix are preserved. Its--forceflag skips the workspace-wide freshness precheck because unrelated projects are unbuilt; the selected project was rebuilt warning-free.No gates, configuration, toolchain, project registry, generated indexes, or other projects changed. The base already pins Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; those pins are unchanged.
These measurements are observations from a shared Azure VM, not a uniform speedup guarantee across thread counts. No 10% physical-RAM improvement is claimed. Full-pool hosted CI and independent review remain pending. Do not merge automatically; the infrastructure priority hold and all normal protections remain in force. Audit manifests, source checkpoints, commands, and timing logs are retained under
/data/codex/scratch/vilin/optimization-20261024-evening.