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 reach the full DomainTheory project and its build workflow. No blocking code issue was found; the expanded proof in Findings
SummaryNarrows
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}
| · exact Or.inl (master_inter _) | ||
| · exact Or.inr (Or.inl (master_inter _)) | ||
| · exact Or.inr (Or.inr (Or.inl (master_inter _))) | ||
| · exact Or.inr (Or.inr (Or.inr (Or.inl (master_inter _)))) | ||
| · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (master_inter _))))) | ||
| · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (master_inter _)))))) | ||
| · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (master_inter _))))))) |
There was a problem hiding this comment.
inter_eq replaces one shared proof with 49 hand-written branches, each choosing a position in the same eight-way conclusion. Changes to the cases or conclusion order now require edits across that table. The existing intersection lemmas still supply every calculation. Use a shared finishing step instead of repeating the nested Or.inr constructors.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
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.8 s → 439.9 s (-12.0%). 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 |
Summary
Optimize the completed
DomainTheoryproject against currentmain(edbe5bd56f476cc2965564676b66199f281ab714). The change narrows the project entry module to terminal public imports that retain the complete API and factors repeated proof calculations across the neighborhood and continuous-lattice developments. It touches onlyLeanPool/DomainTheory.leanand files underLeanPool/DomainTheory/.Semantic invariant audit
I generated a base/head declaration manifest by importing
LeanPool.DomainTheoryin Lean and recording each project declaration’s name, kind, safety level, universe parameters, fully elaborated type hash, and value hash. The base manifest has 6,783 declarations; the optimized head has 7,380. Every pre-existing declaration signature is present at the head (zero missing signatures). The 597 additions are support declarations introduced by proof factoring. No pre-existingdef,opaque,inductive, constructor, recursor, quotient, or axiom value hash changed; theorem proof hashes changed only where the optimization rewrote proofs. No existing public statement or definition was changed.Measurements
Both measurements used
/usr/bin/time -v lake build LeanPool.DomainTheorywith the workspacebuild/andir/directories cleared between runs, the same base/head toolchain, and warm dependency caches. Each build completed 1,467 jobs.edbe5bd56f476cc2965564676b66199f281ab714: 1:13.40 wall, 1,028,464 KB peak RSS.592258de68f6a2d502fed99a883ae5fca94082b1: 1:05.40 wall, 1,009,804 KB peak RSS.Validation
lake build LeanPool.DomainTheorylake exe mk_all --module --checklake exe runLinter LeanPool.DomainTheorylake exe lint-style LeanPool.DomainTheorycd python && uv run python -m lean_pool.quality --repo .. --static-onlyThe full-pool quality environment audit is left to CI because this isolated cycle builds only the selected project.