perf: adopt modules and reduce Lean Pool build cost

[Vilin97]

Lean Pool's legacy imports load proof bodies and broad transitive dependencies, and several closed certificates repeat expensive evaluation. This refactor adopts Lean modules and minimizes imports across the existing project scope, shares mathematical arguments, and replaces repeated certificate work with proved evaluators. The historical fixed-workload benchmark reports 17.13% fewer retired instructions; its workload and source snapshot are documented below and do not cover later incoming projects.

The branch is reconciled with current main. PolynomialMethodRestrictedSums keeps upstream proof repairs together with the module import headers. GapCVP remains byte-identical to main: its incomplete mechanical module conversion was removed because exposed definitions referred to private helpers and failed to compile. The root index retains legacy imports so it can aggregate both migrated projects and newly imported legacy projects. This does not revert the module conversions inside the other projects.

The branch incorporates main 6850d487333f4eff5388859a02a7c91eb2304ee7, including Lean/Mathlib 4.34, the latest imported projects, and the separately merged CI performance work. Current head ddc2a6a92837d8c01fe8e87342feab60f5aac958 preserves the resolution of 126 conflicted files and adds explicit dependencies exposed by full CI after Mathlib's module splits. The repairs cover public p-adic valuation and pullback APIs, matrix order and spectral APIs, countability, polynomial mapping, dominated convergence, and other moved analysis lemmas. Two Incompleteness proof fields now use proof blocks to reference their private helper, and one Poincare continuity composition explicitly identifies its intermediate point. Mathematical statements and computational definitions are preserved.

Current repair validation: all 19 affected projects build with warnings treated as errors and pass declaration linting. The three build batches completed 4,768, 4,543, and 2,488 jobs respectively; these counts include overlapping dependencies and are not a whole-pool job count. The incoming InfiniteConnesRigidity changes are byte-identical to main and separately pass a 3,755-job build and declaration linting. Whole-pool source style and generated-index checks pass on the current head. Earlier Lean 4.34 integration builds and linters also passed for AndersonConjecture, BrauerGroupNew, Brouwer, Chudnovsky, MetricCodes, MRiscX, Lentil, RellichKondrachov, OSforGFF, ArtinWedderburn, BollobasNikiforov, and Erdos132ConvexK3; those project sources are unchanged by the latest repair.

All active non-documentation CI passes on current head ddc2a6a92837d8c01fe8e87342feab60f5aac958. Lean CI run 35387422721 completed successfully: all ten build shards, assembled whole-pool build, Challenge/Solution builds, declaration linters, source style, generated indexes, and repository quality checks pass. Greptile, separation and advisory checks, and Documentation preflight also pass. The long exposition and doc-gen4 jobs remain running and are excluded from the merge decision at the maintainer's explicit request. The superseded runs exposed the repaired failures; they are not reported as passing. Earlier heads 75a8a905 and 137da926 passed all active non-documentation CI on the previous toolchain, which does not validate the current Lean 4.34 integration.

Earlier scoped checks on the preceding toolchain passed: the generated index; complete GapCVP build (3,222 jobs, warnings treated as errors); PolynomialMethodRestrictedSums build (1,998 jobs, warnings treated as errors); both projects’ declaration/style linters; whole-pool style; repository source-quality scans; scoped axiom audits (2,976 GapCVP and 60 PolynomialMethodRestrictedSums declarations); and the compiled environment option/soundness audit. No checks, gates, resource limits, or waivers have been changed. The PR diff contains only permitted content paths.

Per the maintainer's explicit instruction, merge after all current-head active non-documentation checks pass without waiting for long-running documentation jobs. Required branch protection, including Documentation preflight, remains in force. The documentation investigation is complete and the performance fixes landed separately in #450; this PR adds no workflow changes relative to main.

Historical benchmarks, implementation details, and earlier scoped validation

The following records describe earlier checkpoints. In particular, references to a pending GapCVP module repair and a module-mode root index are superseded by the integration described above. Historical full-suite passes are not validation of the current head.

Four of the five newly reconciled projects now pass their scoped checks: QuantumParallelRepetition, MetricCodes, NonSoficGroup and InfiniteConnesRigidity. GapCVP passes its build, linters, quality and axiom checks; its final compiled kernel comparisons are still running, so that repair is not included in this checkpoint. The full frozen PASS below predates all five incoming projects and is not a full validation of the current PR head. Upstream also merged 1,585 Navier–Stokes/Euler module files; they remain byte-identical to main and are outside the measured and fully validated snapshots.

Lean Pool's legacy imports load proof bodies and broad transitive dependencies, while several closed certificates repeatedly evaluate large expressions. This PR adopts Lean's module system, minimizes imports with lake shake, and replaces expensive repeated work with proved evaluators and shared mathematical arguments. Public import edges fall from 22,410 to 15,488 in the original measured snapshot.

Project entry points and intentional API exports are preserved. Dependencies of generated tactic code are explicit, including the standalone public ring-tactic dependency. The migration also fixes generated Lentil proofs whose universe mismatches were hidden by a command-elaborator round trip, gives new public helpers suitable names and documentation, and ports the legacy sensitivity proof into its project.

Certificate changes include a proved coefficient-combining algorithm for Gardam's product, six symplectic pairings for Connes, an early-exit ternary scanner for GKP, and a finite-support evaluator for TwoColoring. Hypergraph, octagon, and geometric finite checks evaluate directly in the Lean kernel. Other proofs reuse existing algebra equivalences, finite-set and finite-sum lemmas, order bounds, and folded homeomorphisms. Shared arguments remove hundreds of lines from Nesterov assembly, Scarf, Anderson union constructions, and planar mesh proofs. Adic-completion proofs now reuse Mathlib’s completeness and evaluation-kernel theorems, with repeated subring closure arguments shared privately. Jensen's final construction reuses the completion equivalence already supplied by the Heitmann proposition; a compiled rfl probe preserves its private wrapper. Vlasov's global flow bounds use existing local theorems. Čech and Laurent-tail proofs use existing restriction maps, direct-limit induction, and finite-support sum maps. Skyscraper's vanishing criterion now reuses coboundary linearity and the existing global-section gluing theorem, removing 90 lines. ZF function proofs use existing graph, lambda, and product facts, removing 170 lines. Existing public statements and computational definitions are preserved; new shared constructions have explicit correctness or carrier-equality checks.

The cold full-pool comparison uses the same 180-project/4,624-import workload, pinned dependencies/configuration, empty pool caches, and CPU affinity 0–7. All six historical snapshots remain below: legacy 9e514186, modules/imports 8c7997a5, proof benchmark f1f05501e, cumulative 07e9f1804, 4114a7b84, and f6dc6c0d1. The seventh column freezes source e25b6810f at 98e24aed6.

Metric	Legacy 9e51418	Modules 8c7997a	Proofs f1f0550	Cumulative 07e9f18	Cumulative 4114a7b	Cumulative f6dc6c0	Current 98e24ae
Retired userspace instructions	124.499 T	119.373 T	107.931 T	105.716 T	104.639 T	103.655 T	103.172 T
Largest single-process RSS	12.605 GiB	11.720 GiB	2.825 GiB	2.892 GiB	2.892 GiB	2.892 GiB	2.891 GiB
Sampled peak tree anonymous memory	13.222 GiB	12.912 GiB	5.680 GiB	5.618 GiB	5.428 GiB	5.264 GiB	5.594 GiB
Inherited task-clock	9.491 CPU-hours	5.461 CPU-hours	7.905 CPU-hours	5.157 CPU-hours	4.877 CPU-hours	5.440 CPU-hours	5.068 CPU-hours
Wall time	83.934 min	43.252 min	103.416 min	40.806 min	38.957 min	43.623 min	41.147 min

The latest fixed-selection run completed all 10,110 jobs and exactly 4,625 pool modules without warnings or errors. Instructions are 17.13% below legacy, 13.57% below the module snapshot, and 0.47% below the preceding warning-free cumulative benchmark. All 4,802 source/configuration hashes and nine pinned dependency repositories stayed unchanged; counters have no errors or multiplexing. Wall time is 41.147 minutes from the harness monotonic clock. These are single shared-host runs, so elapsed times do not isolate causality. Sampled peak tree anonymous memory rises 6.27% from the previous run; process RSS is effectively flat. This is not a memory-improvement claim. Raw wrapper UTC and monotonic spans differ by 109.396 seconds; the cause remains unestablished. Harness and reproduction details, original results, and earlier cumulative results.

Representative scoped measurements are below. These use their own before/after sources and include substantial changes after the cold full-pool snapshot; they are not additive or whole-pool reductions.

Measured scope	Instruction reduction
Gardam product proofs	91.1%
Connes detector, eight shards, and assembly	80.8%
Hypergraph booster certificates	74.8%
GKP finite-range certificate	91.3%
Two representative TwoColoring blocks	71.8%
Nesterov family-estimate assembly	70.1%
Weighted-circle module	90.5%
Scarf module	47.9%
Krull-domain intersection module	50.2%
Prime-adjoining module	53.6%
Regular-tridecagon module	36.7%
Word-closure module	77.5%
Two-generator close-up module	75.9%
Adic evaluation-kernel module	57.4%
Bruhat–Tits block-matrix module	47.8%
Obreschkoff module	48.4%
ComputableRSeq module	74.7%
Anderson combined extension steps	30.8%
Chudnovsky coefficients	33.4%
Anderson main proofs	27.3%
Anderson local power series	22.4%
Anderson Jensen	25.5%
Permanent formula lower bound	12.3%
Brauer group	13.6%
Brauer separable subfields	21.3%
Chudnovsky valence	24.8%
Anderson completion construction	79.0%
Anderson quotient recurrence	37.8%
Nesterov generalized local argument	58.7%
Čech multiplication	29.8%
Laurent-tail comparison	22.2%
Vlasov characteristic flow	7.4%
Convex geometry uniqueness	84.8%
Anderson transcendental adjoining	29.4%
Zeta H1 exchange	32.9%
Convex metric dichotomy	73.9%
Convex diameter lens	81.4%
Čech six-term sequence	35.5%
Čech skyscraper cohomology	78.4%
ZF function graphs and products	10.7%
PFR endgame	14.6%
Runge–Kutta closed certificates	85.8%
Bounded Laurent trade	44.6%
Dolbeault comparison	44.0%
Abel Dolbeault bridge	41.3%
PFR mutual-information chain rule	42.6%
Bounded cocycle restrictions	25.5%
Leray restriction and quotient proofs	34.0%
Čech refinement maps	44.5%
Riemann–Roch residue filtration	16.9%
Pebbling concentration and budget bounds	21.1%
Čech patch restrictions and injectivity	16.32%
Čech window dimension	11.55%
Laurent-tail order bounds and map identities	7.19%
LatticeTriangle order bounds and symmetric proofs	4.51%
Rellich chart range coercions	7.06%
Riemann–Roch residue-field instance synthesis	5.43%
LatticeTriangle quotient and reciprocal estimates	3.11%
LatticeTriangle sum reindexing and telescoping	4.24%
Weil differential inequalities and quotient dimension	9.90%

The new NSubringChain.unionNSubring removes 234 lines by sharing the union's structure and cardinality arguments. Three alternating cold builds of all 50 Anderson modules, including the new constructor and every caller, reduce median instructions from 1.481933T to 1.459215T (1.53%). Individual-process RSS is flat; the concurrent anonymous-memory peak rises about 5%, so this is not a memory-improvement claim. A compiled client proves the constructor's carrier equals the existing union by rfl.

The frozen checkpoint ede6e24fdbce180ef331ccd01dc3dac259b1f6df has validation status PASS for all eleven full checks. The full suite covers the pool build, generated indexes, Challenge/Solution build script, all six declaration/style linters, the unchanged full quality CLI, and a supplemental parser-delta audit. The quality parser finds 75,711 pooled declaration occurrences; the supplement checks 24 additional names under the same axiom whitelist. Thirty-four known inline-include/omit public Anderson names are explicitly audited as well. The shared union and new private subring carriers have compiled rfl probes. A standalone client imports the Čech colimit module and applies the new public cocycle induction principle under its intended assumptions; its axiom audit passes.

A separate read-only compiled axiom-closure audit also passes at that exact frozen checkpoint. It covers all 214,328 serialized pool declarations (213,791 distinct names) across 4,678 modules, and traverses 398,360 reachable serialized declaration bodies, including private/generated declarations, theorem and opaque bodies, constructor types, and earlier serialized variants of duplicate names. Its axiom union is exactly propext, Classical.choice, and Quot.sound, with zero missing constants or metadata errors. Adversarial fixtures cover hidden private/opaque axioms and overwritten duplicate theorem bodies; an unused foreign duplicate correctly remains outside the reachable graph. All 4,724 source/gate hashes remain unchanged. This external audit supplements the unchanged repository checks; it is not an independent kernel replay. Later changes have full per-project builds, declaration/style checks, and scoped source/axiom/environment validation. No authored quality-gate, source-limit, or waiver changes are included.

Shared public lemmas also remove duplicate proofs across callers. The Čech colimit/multiplication pair saves 2.66% in three alternating compilations of both modules including artifact emission. Reusing the existing factorial bound between two Chudnovsky modules saves 7.39% under the same inclusive protocol. These are separate scoped comparisons: the Čech pair's process RSS is flat and sampled anonymous memory rises 1.20%; factorial sharing adds 1,824 bytes across the two public artifacts while shrinking the consumer's private artifact by 56.64%.

The latest warning-free cold benchmark stops at source e25b6810fd280bb52c2e9e2a5f58c1f5b5ba15ff. Its unchanged historical selection excludes the five newly reconciled project scopes; it also predates the additional proof commits reported in this update. Those have separate scoped measurements and are not included in the latest cold column.

Upstream main fec1e89f48 and the automated PR update 196cd5279 are preserved by reconciliation aadad161f, integrated at c07200bc2. MinimumDegreeMatching's six files now use modules, explicit field definitions, and private implementation imports. Its public facade and all 59 compiled public types/axiom lists match the original legacy project; computational definitions and instances are preserved. The matching proof bounds are shorter. Three alternating compilations of all six modules, including provider/consumer artifacts, reduce median instructions from 106.128B to 92.677B (12.67%) for the combined import and proof changes. This project is included in the latest frozen validation; the historical cold benchmark selection excludes it. All upstream non-Lean files remain byte-identical to main, and the PR diff contains only allowed content paths.

Companion tooling work remains separate: #416 preserves module exports when automatic rebases regenerate indexes. The prepared quality-parser compatibility patch handles module import/card syntax, explicit public declarations, and section modifiers, with 92 scratch tests passing. It remains unapplied pending the explicit authorization required by the contributing rules; inline declaration wrappers still need further parser coverage.

A supplementary audit of the three round-44 Borel files now verifies all 143 named compiled public types and axiom sets against their original versions; the logs are warning-free.

Correction to earlier Borel evidence: a redundant Classical.not_imp argument introduced a compiler warning in Zero/Strat. Earlier scoped reports missed that warning; seven summaries have been corrected and their original logs preserved. Commit e55f6bf5b removes the unused argument. The affected three final timing runs are superseded by three fresh original/final pairs: 33.390B → 32.158B instructions (3.69%), with all six logs warning-free and all 14 named compiled types/axiom sets identical. Wall time is effectively flat; the private artifact grows by 7,424 bytes while public/IR artifacts remain unchanged. The latest frozen whole-pool build also has no unexpected compiler warnings.

A newer fixed-selection cold benchmark freezes source a1aa4f42f at 7585918ef. That source predates the Borel warning fix. The run retains its original source and logs and is classified separately from the warning-free results above. It completed with 103.379T measured instructions and the known warning; it is not a warning-free validation checkpoint. Its monotonic elapsed time is 41.457 minutes. Raw UTC and monotonic clock spans differ; their cause remains unestablished.

Upstream main ae6d5445d and automated PR update e7b024e6a are reconciled. They add 110 Lean files across GapCVP, InfiniteConnesRigidity, MetricCodes, NonSoficGroup and QuantumParallelRepetition. The 99 legacy files receive module/public-import headers; 11 existing module files are unchanged. The root facade preserves its prior public exports and adds the new modules. Its existing generated header marker, dropped during reconciliation, is restored exactly from the earlier validated checkpoint; all 4,787 public imports remain byte-identical and mk_all --check passes. NonSoficGroup and InfiniteConnesRigidity pass their complete scoped builds, linters and quality/axiom checks with unchanged upstream source. All upstream non-Lean changes are preserved. The frozen full PASS and historical cold benchmarks exclude this incoming scope.

QuantumParallelRepetition now has 123 compiler-required helper promotions, 110 meaningful helper/field docstrings, and one private proof import. Reversing those edits and the mechanical headers reconstructs all 13 upstream sources byte-for-byte: all original mathematical statements and proof/computational bodies are preserved. Its 3,147-job build, declaration/style linters, unchanged scoped quality checks, option audit, and conservative compiled axiom closure pass without warnings. All 3,379 stable serialized declarations preserve types, universes, safety and computational values after the explicit private-name mapping and proof normalization; 31 remaining expressions pass direct Lean kernel definitional-equality checks. This includes 2,245 originally public declarations and 650 originally public computational definitions. All 1,689 source-public names also pass an actual module-mode client. Compiler-generated proof/match auxiliary names are not claimed unchanged; their bodies remain covered by the full axiom closure. No performance reduction is claimed for this compatibility repair.

Three further JacobianDiffgeo proof refactors remove 86 lines in total: shared Čech patch restrictions, quotient membership for window dimensions, and direct Laurent-tail map/order identities. Each has three warning-free matched measurements, complete compiled named-interface/axiom equality, a full 3,399-job project build, declaration/style linters, unchanged scoped quality checks, and a conservative compiled axiom closure. All original computational definitions remain byte-identical. The Laurent-tail comparison begins after its earlier optimization, so its 7.19% is a follow-up scope, not a replacement whole-pool result.

MetricCodes now passes its 16-file scoped repair: 570 compiler-required helper promotions, 565 required docstrings, two private proof imports, 11 helper renames, and four explicit instance names retaining the original generated names. Exact inverse reconstruction preserves the upstream source modulo those recorded edits. All 6,625 stable project declarations, including 1,570 computational definitions and 5,379 parsed source-named declarations, preserve their compiled interfaces/values through typed normalization, three explicit raw noConfusion matches, and 99 kernel equality checks. Build, linters, unchanged quality/option checks and all 10,372 serialized-root axiom closures pass without warnings. The parsed-name count is not a complete lexical declaration count; the stronger compiled inventory also covers local/anonymous declarations. One foreign compiler artifact changes visibility: the lazily generated Real.binEntropy.eq_1 is now private, so an ordinary public client can no longer reference that incidental name. Its raw statement is unchanged; this exception is recorded explicitly. No performance saving is claimed for this repair.

Upstream main 76d244430 and automatic PR update 0dc7314fe are preserved. The incoming NavierStokesAndEuler project already uses modules: all 1,585 source files are byte-identical to main, with no authored project changes or performance claim. The automatic update regenerated the root as legacy imports; its established module/public-import form is restored with all 6,372 module names and their order preserved, and mk_all --check passes. Upstream NOTICE, README and registry data remain byte-identical to main. This additional inherited project is also excluded from the fixed cold selection and previous full frozen validation.

The latest 6 measured proof scopes remove 242 lines net. Each has three warning-free matched actual-source compilations, preserved named compiled types, a complete project build, declaration/style checks, unchanged scoped quality/option checks and conservative serialized axiom closure. The LatticeTriangle quotient-product proof additionally drops its dependencies on Classical.choice and Quot.sound, retaining only propext; its other axiom lists are unchanged. Divisor's local instance is explicitly included in its API probe. These are incremental scoped reductions, not additive whole-pool savings.

[Vilin97]

Measurement setup and first migration checkpoint

• Baseline commit: 9e51418621fcd2050d89dd5cfe593abc9a3976d4.
• Initial module conversion: 378712919 (4,214 files changed). Lean v4.34.0-rc1’s Modulize.lean preserves public declarations and exposed definitions; mk_all --module --lib LeanPool regenerates the public aggregate.
• Baseline build is running in a separate checkout with an initially empty pool build directory and the existing Mathlib dependency cache. Command: LEAN_NUM_THREADS=8 taskset -c 0-7 lake build LeanPool.
• Measurements: monotonic wall-clock; Linux perf_event_open inherited task-clock and retired userspace instructions; wait4 user/system time and maximum per-process RSS; summed RssAnon over the build process group sampled every 200 ms. The anonymous-memory peak is a sampled lower bound, excludes file-backed .olean mappings, and is not summed RSS.
• Both perf counters work on this WSL2 host. A nested-process sanity check gave 0.774 s task-clock versus 0.778 s user+system CPU, and 9.490 billion userspace instructions; counters were scheduled 100% of their enabled time.
• This is a shared 32-logical-CPU / 45-GiB host. Baseline and final timed builds use the same CPU affinity and thread setting. Unrelated activity can affect wall time, so CPU instructions and memory measurements will accompany every claimed speedup.

The baseline is not finished yet; no performance improvement is claimed at this checkpoint. The first repair build has found tactic implementations needing explicit meta marking and a declaration visibility issue. All kernel, axiom, and quality checks remain enabled.

[Vilin97]

First measured pilot: LeanPool.AgreeToDisagree (two proof files and their public entry module)

Each version was compiled with a fresh pool build directory, prebuilt Mathlib, LEAN_NUM_THREADS=8, and CPU affinity 8-15. All three builds succeeded. This is a small pilot, not a whole-pool result.

Metric	Original	Modules	Modules + shake
Wall time (s)	12.68	8.31	10.37
Task-clock (s)	16.23	11.27	13.98
User CPU (s)	12.01	8.21	7.52
System CPU (s)	4.39	3.18	6.64
Userspace instructions (billions)	48.50	46.59	40.60
Maximum process RSS (GiB)	2.26	1.17	1.15
Sampled peak anonymous memory (MiB)	358.61	358.14	320.21

The module-only step roughly halves maximum RSS, largely by excluding private imported data. Shake removes unnecessary tactic imports and makes the SFinite/infinite-sum proof dependencies private; both public project re-exports remain. Relative to the original, the shaken pilot executes 16.3% fewer userspace instructions and has 10.7% lower sampled peak anonymous memory.

The shaken run has higher system time and wall time than the module-only run despite fewer instructions. These are single samples on a shared WSL host; I am repeating the pilot before drawing timing conclusions. Neither full-pool build has finished yet.

The initial draft also exposed the existing CI planner’s oversized CHANGED_FILES environment variable (Argument list too long). #412 addresses that prerequisite. #416 separately preserves module-style indexes during automatic rebases, as required by the content/infrastructure separation rule.

[Vilin97]

Pilot repeats: the memory result is robust; the first shake-speedup inference was premature

I repeated all three configurations twice, again removing the pool build directory before each run and rotating execution order. All nine builds passed. Medians across the three runs:

Metric	Original	Modules	Modules + shake
Wall time (s)	12.68	11.16	10.37
Task-clock (s)	14.49	12.73	13.15
Userspace instructions (billions)	42.55	40.63	40.60
Maximum process RSS (GiB)	2.25	1.17	1.17
Sampled peak anonymous memory (MiB)	357.28	362.67	356.22

The initial baseline and module runs each executed about 6 billion more instructions than their subsequent runs, while the copied shake checkout did not show that initial overhead. The earlier 16.3% instruction reduction and 10.7% anonymous-memory reduction should not be used as conclusions. Across the repeated samples, module conversion reduces instructions by about 4.5% and maximum per-process RSS by about 48%; additional shake savings in this particular small project are negligible. Anonymous memory is essentially unchanged.

Wall time varies substantially on the shared host (original: 7.50–14.26 s; modules: 8.31–12.03 s; shaken: 6.49–12.06 s), so I am not treating the wall-time medians as a reliable speedup estimate. The full-pool comparison remains in progress.

[Vilin97]

Module-port repair checkpoint

The first 30 failing files have localized repairs, verified with targeted Lake builds. Examples:

• tactic extensions explicitly use meta;
• private proof helpers stay private, using structure-field private or private_decl% for proof subterms in exposed definitions (the same technique used in Ullrich’s port);
• data helpers needed by exposed definitions receive public names;
• missing Mathlib dependencies are imported explicitly;
• ambiguous inferred arguments are made explicit, and newly redundant proof steps are removed.

The full library textual style checker passes. The initial whole-pool build is still collecting later failures; this checkpoint is not a claim that the full migrated library passes yet. No checking options or gates were disabled.

[Vilin97]

A larger benchmark checkpoint: 92 Lean modules in the complete LeanPool.Feige dependency set, including its cross-project Isoperimetric dependency. All three builds below succeeded. These are first samples, not final whole-pool results.

Version	Wall time	Inherited task-clock	User-space instructions	Maximum process RSS	Sampled peak total anonymous memory
baseline	116.27 s	429.09 s	958.16 B	3.090 GiB	1.779 GiB
module	89.63 s	323.65 s	887.65 B	1.496 GiB	1.726 GiB
shaken	209.57 s	418.93 s	883.48 B	1.514 GiB	1.762 GiB

The mechanical module migration reduces instructions by 7.4% and maximum process RSS by 51.6%. The much smaller change in total anonymous memory is consistent with the module system chiefly reducing imported proof/olean data. Shake applied 73 import suggestions; its first sample saves a further 0.5% of instructions.

Do not read the wall/task-clock columns as a controlled speedup estimate yet. Other full builds are running on this host, and the shaken sample has much worse timing despite almost unchanged instruction count. I am running two more interleaved rounds of all three versions and retaining every sample.

Method: identical pinned toolchain and prebuilt package dependencies, empty per-copy .lake/build, LEAN_NUM_THREADS=8, affinity CPUs 22–29. The monitor uses inherited Linux perf events for task-clock and instructions:u, wait4 for maximum process RSS, and samples the process group's summed /proc/*/status RssAnon every 0.2 seconds. Both counters report 100% scheduling; anonymous-memory peaks are sampled lower bounds. No proof/kernel or axiom checks were disabled. This is a local benchmark; the full original baseline and migration repair build are still running.

[Vilin97]

Feige import optimization is now in e54e55a, and the integration build in this PR worktree passes. The separate benchmark has also completed three clean builds of each version, all successfully.

Medians (92 modules in the original dependency set, same toolchain/cache/CPU affinity; methods as in the previous comment):

Version	Wall	Task-clock	Instructions (:u)	Maximum process RSS	Peak total anonymous memory
baseline	116.27 s	429.09 s	958.10 B	3.090 GiB	1.791 GiB
module	89.63 s	359.92 s	887.69 B	1.503 GiB	1.726 GiB
shaken	205.72 s	400.95 s	883.52 B	1.506 GiB	1.808 GiB

The repeatable result is 7.4% fewer instructions from modules, then another 0.5% from Shake; maximum process RSS is approximately halved. This benchmark does not establish a wall-time improvement from Shake. The shaken wall times were 209.57, 205.72, and 94.26 seconds, while the other variants also varied substantially. All timings remain visible below; the host was shared with the full baseline and migration builds.

Shake changes 73 files. Public import lines fall from 234 to 164; total direct import lines rise from 234 to 292, because Shake adds explicit dependencies while removing redundant imports and re-exports. A smaller direct-import count is not the optimization target: the accessible dependency set and import visibility matter.

All nine samples (seconds, billion instructions, KiB)

Sample	Wall s	Task-clock s	Instructions B	Max RSS KiB	Peak anonymous KiB
baseline 1	116.27	429.09	958.160	3239628	1865736
baseline 2	162.53	434.46	958.096	3239236	1877852
baseline 3	101.70	402.59	958.090	3242764	1914020
module 1	89.63	323.65	887.650	1568280	1809992
module 2	100.93	371.71	887.716	1578088	1737500
module 3	84.35	359.92	887.686	1576088	1840592
shaken 1	209.57	418.93	883.478	1587068	1847988
shaken 2	205.72	400.95	883.523	1579252	1895472
shaken 3	94.26	354.22	883.554	1570280	1961532

The content PR remains a draft. The first full migration scan is still running, with failures repaired and checked locally as they surface. These are project-level measurements, not a completed whole-pool result.

[Vilin97]

The full original baseline completed successfully at base 9e51418621fcd2050d89dd5cfe593abc9a3976d4: 10,166 build jobs, with fresh pool artifacts and the shared prebuilt package cache.

Quantity	Original full pool
Elapsed wall time	83.93 min
Inherited task-clock	9.491 CPU h
User-space retired instructions	124.499 trillion
Largest individual process RSS	12.605 GiB
Sampled peak sum of anonymous memory	13.222 GiB

Configuration: LEAN_NUM_THREADS=8, affinity CPUs 0–7; inherited perf counters excluded kernel/hypervisor execution and ran without multiplexing. Anonymous memory was sampled every 0.2 s across the process group, so this is a sampled lower bound; individual-process RSS includes mapped artifacts. Other builds ran on other CPUs during the measurement, so wall time and CPU time remain sensitive to host contention.

The migrated full build is still being repaired, so this is a reference measurement, not yet a full-pool speedup claim. The completed Feige comparison above remains the measured comparison for the module/import changes so far.

[Vilin97]

Pushed another repair checkpoint, 3ba6c3d15: 140 source files that have compiled without warnings, plus the regenerated index. This includes the module port of Mathlib's legacy Archive.Sensitivity proof (original license and authors retained), SetTheory's generator phase split and explicit public generated companions, and custom simproc/tactic runtime dependencies.

The original full build measurement is recorded above. The migrated full build is still incomplete: diagnostic passes have reported 129, then 67, then 52 failing files. These are not identical test sets: repairing dependencies lets each pass reach previously skipped downstream files. Sixteen failures in the latest pass are the same private certificate-array dependency pattern, now being repaired together.

The checkpoint does not claim a successful whole-pool build, complete import minimization, or final performance figures. Existing CI cannot yet compile this large diff because its changed-file environment exceeds the OS argument-size limit (the main build-planner fix is separately proposed in #412). The proof-profile workflow has the same size-limit problem. No checks, profiling workflow, or linter settings have been weakened.

[Vilin97]

The complete module migration now builds: lake build LeanPool succeeded with 10,167 jobs, and the build traces for all current LeanPool source files contain zero warnings or errors. lake exe mk_all --check also passes. This is an incremental integration check, not the final cold-build performance result.

Pushed checkpoint fe7613741335987902ac7aa9992a1191fffe612a, including another 123 repaired files. The last repairs covered exposed data depending on private helpers, direct metaprogramming imports, public API equations for opaque Mathlib constructions, and generated theorem proofs with unused universe metavariables. The generator rejects unresolved statement metavariables and submits every generated declaration to the kernel as before.

I also rebased onto 08ef17978 to pick up the now-merged build-planner fix #412. The only upstream differences from the measured baseline are that CI fix and an attribution update; the original Lean sources and toolchain are unchanged, so the baseline comparison remains applicable.

Full-pool lake shake --fix --explain LeanPool is now running. Next are rebuilds after minimization, repository linters/axiom checks, and the fresh optimized build measured with the same counters and CPU affinity as the baseline. The proof-profile workflow still has its separate oversized-environment issue, and module syntax support in the repository quality parser still needs the previously proposed compatibility patch; no protected gate has been changed.

[Vilin97]

Full-pool lake shake --fix --explain LeanPool completed and applied 3,953 suggestions, saved in 857298e52. I checked every edited file: after removing import lines and blank lines, its contents are identical to the preceding commit. The generated project/library indexes retain their public exports.

Direct imports across LeanPool	Before full shake	After full shake
Public	22,463	15,010
Private	251	13,345
Total	22,714	28,355

The higher total is expected: broad transitive imports become explicit dependencies. These counts describe the tool output before compatibility repairs; they are not a build-time result.

The rebuild is finding cases that still require explicit public imports (notably theorem references inside exposed constructors and some attributes), along with unused namespace/section declarations whose imports shake removed. I am repairing these as their compile jobs finish.

The full declaration linter on the pre-shake module checkpoint found only naming/docstring issues: 393 newly public helper names with underscores and 527 missing docstrings, mostly generated certificate arrays. Those fixes are applied locally and included in the rebuild. The source style check, generated-index check, and unchanged Challenge/Solution build passed at that checkpoint. Full linter/axiom verification and the optimized cold-build measurements remain outstanding.

[Vilin97]

The full import-minimization repair is progressing: the first rebuild reported 127 failing modules; the next reported 61 as more downstream files became reachable. Repairs for that second set are now undergoing another full build. These results are diagnostic rebuilds, not performance measurements.

The recurring exceptions to a mechanical lake shake --fix pass are now clearer:

• Imports used by examples or quoted/generated tactic code can disappear. I am restoring those dependencies, including the imports needed when tactic quotations are created.
• Exposed definitions sometimes need instances or proof dependencies imported publicly even when shake selects a private import.
• A documented API facade must retain its main theorem as a public import so callers can continue using the facade.
• Additional direct imports can change instance selection. The matrix-action development now passes its targeted check with its established imports plus the explicit dependency needed after its dependencies were minimized.
• A few independent files contained duplicate theorem names that become visible together. The repairs reuse the existing canonical lemmas.

The source checks pass for headers, forbidden constructs, file sizes, and proof sizes; the full style checker also passes. The helper documentation and naming fixes for the declaration linter are in the working tree and are being rebuilt. The final declaration-linter run, stable-artifact axiom/option audits, and full optimized cold-build measurement are still outstanding. The successful baseline measurement above remains the comparison point; no full-pool speedup is claimed yet.

[Vilin97]

The minimized 159-project snapshot now builds successfully and passes the full declaration linter. Tested snapshot: f248e0b98.

Validation completed for that snapshot:

• Full lake build LeanPool: success (10,100 jobs after the last dependency cleanup).
• Compiler trace audit across every current Lean Pool source: zero warnings/errors.
• lake exe runLinter LeanPool: pass (the earlier run covered 100,197 declarations plus 103,748 generated declarations).
• Full style check and generated-index check: pass.
• Challenge/Solution build: pass with only the registered challenge sorry notices.

The full repository quality checker, including axiom and option audits, is still running. The fresh optimized build measurement has started in a separate checkout of f248e0b98, using the baseline's eight-CPU affinity, eight Lean threads, prebuilt dependencies, and the same measurement harness.

Two automated merges added Ehrhart volume inequality and sphere packing to this PR branch while the optimization was underway. I have integrated those merges in f8fbbad6b, retained the module index, and converted sphere packing's entry-point wrapper (the new projects' proof files already use modules and minimized imports). That expanded build is running separately. The performance comparison intentionally retains the same 159-project workload as the completed baseline; it does not compare the old pool against the larger pool. Wall times will carry the same concurrency caveat as the baseline; inherited instruction and task-clock counters cover only the measured process tree.

[Vilin97]

The full quality audit caught problems beyond what the build and declaration linter covered. Fixed in dd80c8e5c:

• Restored 259 intentional public imports across 60 import facades. Shake had removed imports from files whose purpose is to re-export an API. Added explicit public imports for the advertised results at the affected project entry points.
• Fixed Lentil's theorem generator: quoted references now carry the original theorem's universe parameters, and proof elaboration runs directly in TermElabM, retaining kernel diagnostics. The previous command-elaborator round trip hid auxiliary proof failures. The affected generated theorem now reports only propext and Quot.sound through #print axioms.
• Adjusted two newly public helper declarations so the existing source audit resolves their names (cachedLength and an explicit universe declaration for Bundle). No checks, gates, or waivers were changed.

Validation: the expanded pool builds successfully (10,149 jobs), every current source's build trace is free of compiler warnings/errors, and the style checker passes. Full declaration lint and the complete quality audit are running again on this stable snapshot.

I stopped and discarded the incomplete cold measurement of f248e0b98 after these audit findings. The replacement measures corrected commit 8c7997a54, which applies the same repairs to the original 159-project workload. This keeps the comparison against baseline 9e514186 fair; the two projects added to main during this PR are validated separately in the integration build, not included in only one side of the timing comparison.

[Vilin97]

Correction to the workload labels in earlier progress comments: the actual projects.yml registries contain 180 projects at both baseline 9e514186 and optimized 8c7997a54, and 182 projects at integration commit dd80c8e5c. The earlier 159-project label came from the stale README count. The before/after workload is still identical; this corrects the description, not the measured inputs. The two upstream additions remain excluded from both benchmark snapshots and included in the integration validation.

[Vilin97]

All local validation now passes for dd80c8e5c (182 projects):

• lake build LeanPool: success, 10,149 jobs.
• Every current source's build trace: zero compiler warnings or errors.
• lake exe runLinter LeanPool: pass.
• lake exe lint-style LeanPool: pass.
• lake exe mk_all --check: no update necessary.
• scripts/ci/build-challenges.sh: pass, only expected open-challenge notices.
• uv run python -m lean_pool.quality --repo ..: Quality checks passed, including project entry points, 74,494 parsed pool declarations, challenge/solution axiom checks, and the environment audit for generated axioms and option backdoors.

The failed Lentil auxiliary proofs and entry-point exports reported in the earlier audit are fixed in source. No gates or waivers were changed. The matched 180-project cold benchmark on corrected commit 8c7997a54 continues; I will add the final wall/task-clock, instruction, and memory comparison when it completes.

[Vilin97]

Measurement reproduction details:

The full comparison uses fresh .lake/build directories at baseline 9e51418621fcd2050d89dd5cfe593abc9a3976d4 and optimized 8c7997a54 (the same 180-project registry, toolchain, Lake manifest, and Lake configuration). Both use the shared prebuilt package cache, LEAN_NUM_THREADS=8, and CPUs 0–7. The expanded PR snapshot is validated separately.

Run the harness below from each corresponding worktree, with a different output prefix:

LEAN_NUM_THREADS=8 taskset -c 0-7 python3 measure.py /path/to/results/baseline-full lake build LeanPool

This Linux/x86-64 harness starts inherited perf counters before releasing the child process, records maximum process RSS through wait4, and samples the sum of RssAnon across the build process group every 0.2 seconds. The JSON includes counter enabled/running times and counter errors so missing or multiplexed counters are visible. It writes the full build output to the matching .log file.

RssAnon is a sampled approximation of total heap/anonymous resident memory, not an exact allocator high-water mark. Maximum process RSS includes mapped files. There is one full cold run per version; the earlier Feige experiment has three runs per variant. Other host activity can affect elapsed and CPU time, so those single-run quantities will be reported with that limitation.

Exact measurement harness

"""Measure a process tree with inherited Linux perf counters and /proc sampling."""

import ctypes
import fcntl
import json
import os
from pathlib import Path
import struct
import sys
import time


def counter(process, kind, configuration, userspace=False):
    attributes = ctypes.create_string_buffer(128)
    flags = 1 | (1 << 1)
    if userspace:
        flags |= (1 << 5) | (1 << 6)
    struct.pack_into("IIQQQQQ", attributes, 0, kind, 128, configuration, 0, 0, 3, flags)
    library = ctypes.CDLL(None, use_errno=True)
    descriptor = library.syscall(298, ctypes.byref(attributes), process, -1, -1, 0)
    if descriptor < 0:
        raise OSError(ctypes.get_errno(), os.strerror(ctypes.get_errno()))
    return descriptor


def sample(group):
    anonymous = 0
    count = 0
    for entry in Path('/proc').iterdir():
        if not entry.name.isdecimal():
            continue
        try:
            fields = (entry / 'stat').read_text().rsplit(')', 1)[1].split()
            if int(fields[2]) != group:
                continue
            count += 1
            for line in (entry / 'status').read_text().splitlines():
                if line.startswith('RssAnon:'):
                    anonymous += int(line.split()[1])
        except (FileNotFoundError, ProcessLookupError, PermissionError):
            continue
    return anonymous, count


def main():
    destination = Path(sys.argv[1])
    command = sys.argv[2:]
    reader, writer = os.pipe()
    process = os.fork()
    if process == 0:
        os.close(writer)
        os.setsid()
        os.read(reader, 1)
        os.close(reader)
        with destination.with_suffix('.log').open('wb') as log:
            os.dup2(log.fileno(), 1)
            os.dup2(log.fileno(), 2)
        os.execvpe(command[0], command, os.environ)
    os.close(reader)
    counters = {}
    errors = {}
    for name, arguments in [('task_clock_ns', (1, 1, True)), ('instructions_user', (0, 1, True))]:
        try:
            counters[name] = counter(process, *arguments)
        except OSError as error:
            errors[name] = str(error)
    start = time.monotonic()
    for descriptor in counters.values():
        fcntl.ioctl(descriptor, 0x2400, 0)
    os.write(writer, b'1')
    os.close(writer)
    peak_anonymous = 0
    peak_processes = 0
    samples = 0
    while True:
        anonymous, count = sample(process)
        peak_anonymous = max(peak_anonymous, anonymous)
        peak_processes = max(peak_processes, count)
        samples += 1
        completed, status, usage = os.wait4(process, os.WNOHANG)
        if completed:
            break
        time.sleep(0.2)
    results = {
        'command': command, 'cwd': os.getcwd(),
        'exit_code': os.waitstatus_to_exitcode(status),
        'wall_seconds': time.monotonic() - start,
        'user_seconds': usage.ru_utime, 'system_seconds': usage.ru_stime,
        'max_process_rss_kib': usage.ru_maxrss,
        'sampled_peak_tree_anonymous_kib': peak_anonymous,
        'peak_processes': peak_processes, 'samples': samples,
        'sampling_interval_seconds': 0.2,
        'affinity': sorted(os.sched_getaffinity(0)),
        'counter_errors': errors,
    }
    for name, descriptor in counters.items():
        value, enabled, running = struct.unpack('QQQ', os.read(descriptor, 24))
        results[name] = value
        results[name + '_enabled_ns'] = enabled
        results[name + '_running_ns'] = running
        os.close(descriptor)
    destination.with_suffix('.json').write_text(json.dumps(results, indent=2) + '\n')
    print(json.dumps(results, indent=2), flush=True)
    return results['exit_code']


if __name__ == '__main__':
    sys.exit(main())

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[Vilin97]

Automated review disposition: needs-maintainer

Reviewed exact head 137da92698061e611c86cd2b39b34bb5a145829b (unchanged since 2026-09-17; auto-rebase cannot touch it). All active CI was green on this head — ten shards, assembly, Build project, linters, quality checker, separation, Greptile — so the earlier shard 05 change request is resolved.

What changed underneath it: main merged the Lean/Mathlib v4.34.0 bump (#436) plus two imports (#451, #452). git merge-tree origin/main <head> now reports 756 conflicting Lean files across the pool (e.g. AharoniKorman/Counterexample.lean, AndersonConjecture/AdicKerEval.lean, Brouwer/*.lean, BollobasNikiforov/**), because the bump repaired proofs in the same files this PR converted to modules and golfed. The auto-rebase tool stops on the first non-index conflict, and no mechanical resolution exists: the migration has to be re-done on top of v4.34.0 (regenerate the module headers/lake shake step and re-apply the proof optimizations), then re-validated with a full-pool build and the whole-library linters.

That is why this is a maintainer decision rather than a change request to an author: the PR is a pool-wide architecture change (Lean module system across ~4,600 files, a root index that mixes module and legacy imports, the #416 rebase-tool prerequisite, and a quality.py parser follow-up the author says needs explicit authorization). Please decide one of:

1. Adopt the module migration. Then the reconciliation above is a multi-hour rebuild of the branch on v4.34.0, and every subsequent import must either be module-ized or keep riding the legacy-import path in the root index — say which, and it can be scheduled as its own cycle.
2. Decline. Close this PR (and fix: preserve module exports when rebasing import PRs #416 with it), keeping the per-project optimizations already landed separately (perf: optimize polynomial restricted-sum proofs and imports #441, perf: speed up InfiniteConnesRigidity proofs and imports #447).

No code in this PR is being judged deficient; the label records the reconciliation cost and the architecture question.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[Vilin97]

Update at 32d7ca9e05 (2026-09-18, end of cycle). After the note above, a later push reconciled this branch with main (9115f3a6c merge, 32d7ca9e0 "Adapt optimized proofs to stable Mathlib import and adjoin APIs"); git merge-tree against current main now reports no conflicts, so the "756 conflicting files" figure is superseded. The reconciled head does not build, however: the exact-head Lean CI fails nine of ten shards (only shard 00 still running) — e.g. shard 05: FactorizationSystems/Orthogonality.lean:35 Unknown identifier Limits.HasPullbacks (×55) plus parse errors at lines 87–95, Incompleteness/.../Formula/Functions.lean:517–518 Unknown identifier defined_identity_substitution, Odlyzko/DedekindZeta/PrimeIdealFactor.lean:26 instance synthesis; shard 01: 101 errors under QuantumParallelRepetition. The architecture decision for the maintainer is unchanged, so needs-maintainer stays; if the answer is "adopt", the reconciliation must additionally be brought to a green full-pool build before any merge.