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] No blocking defect was found in the changed proofs or module split. SummaryFactors repeated group arguments into shared lemmas and moves public foundations into two smaller modules.
Reviews (1) · Last reviewed commit: "Reduce SmallUndecidableGroups build memo..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)
This build covers the added modules and their dependency cones on top of the measurement environment; modified files are measured without rebuilding the pool. Statement changes✅ No statements changed — all 368 tracked declarations across 5 modified files kept their type; only proofs / definition bodies changed. Also: 4 declarations added, 85 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)
➖ Declarations removed (85)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 361,984 → 316,643 (-45,341, -12.5%). Commands: 119 → 123. Per-file wall sum: 67.4 s → 44.1 s (-34.5%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 2 compared — 1 cheaper, 1 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
New files — absolute profileTotal heartbeats: 34,371 maxHeartbeats units across 2 valid files (524 added LOC). Sum of Count-heartbeats wall-clock total: 6.99 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
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.SmallUndecidableGroups.GroupTheory.HNNLemmas |
6.70 s |
LeanPool.SmallUndecidableGroups.Host.YStage |
6.70 s |
LeanPool.SmallUndecidableGroups.Host.ZStage.Definitions |
2.10 s |
LeanPool.SmallUndecidableGroups.Host.YStage.Definitions |
1.80 s |
Per-file `lean --profile` output
LeanPool/SmallUndecidableGroups/Host/YStage/Definitions.lean
import took 1.4s
cumulative profiling times:
attribute application 235ms
congr simp thm 0.897ms
elaboration 176ms
fix level params 0.915ms
import 1.4s
initialization 31.2ms
instantiate metavars 0.294ms
interpretation 301ms
let-to-have transformation 0.72ms
linting 22.5ms
module linting 0.00194ms
overlappingInstancesLinter 7.42ms
parsing 16.5ms
process pre-definitions 19ms
share common exprs 3.31ms
simp 18.1ms
tactic execution 0.608ms
tacticAnalysis 34.9ms
type checking 54.5ms
typeclass inference 60ms
real 2.72
user 1.79
sys 0.97
LeanPool/SmallUndecidableGroups/Host/ZStage/Definitions.lean
import took 876ms
attribute application took 219ms
attribute application took 168ms
cumulative profiling times:
attribute application 617ms
congr simp thm 1.92ms
elaboration 177ms
fix level params 1.14ms
import 876ms
initialization 29.8ms
instantiate metavars 0.331ms
interpretation 275ms
let-to-have transformation 0.973ms
linting 22.4ms
module linting 0.00139ms
overlappingInstancesLinter 7.45ms
parsing 15.6ms
process pre-definitions 23.1ms
share common exprs 5.4ms
simp 408ms
tactic execution 26.7ms
tacticAnalysis 35.7ms
type checking 73.9ms
typeclass inference 145ms
real 2.67
user 2.68
sys 0.88
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
SmallUndecidableGroups repeatedly elaborates concrete HNN-model compositions and expands nested substitution words. This factors the common group arguments and separates independent public foundations from the model proofs. In controlled clean-project builds, median whole-build peak PSS falls 12.55% and simultaneous process-tree RSS falls 18.93%. Median wall time is 4.60% slower on the shared VM; the requested stopping target is met through RAM usage.
Selected project: SmallUndecidableGroups, originally 30,021 lines / 87 modules. Larger candidates including QuantumParallelRepetition and EhrhartVolumeInequality already had optimization PRs in progress. This project had no competing optimizer, and its baseline exposed substantial HNN elaboration costs: ZStage took 13 s, YStage 8.7 s, and Compression 6 s; the complete baseline reached about 2.1 GiB largest-child RSS.
Host/YStage/Definitions.leanandHost/ZStage/Definitions.lean. Existing modules publicly re-export them. Every original private declaration remains in its original module. The generated project Imports index includes both new files.Base:
edbe5bd56f476cc2965564676b66199f281ab714Head:
36398932203f17bcb66f682af63191ee3adf4b28Origin/main was fetched and verified unchanged immediately before committing. Uses main's existing Lean/Mathlib 4.35.0-rc3 pins, Mathlib
c55e6e786f49471c72fbddbec5415808896aec1e. The project card, root index, pinned configuration and repository gates match base.Invariant audit. Before editing, a Lean environment inspector imported all project modules with
importAll := trueand extensions disabled. It recorded exact expression DAGs for every constant's fully elaborated type and every non-theorem value, universe parameters, declaration kind, safety/partial flags, reducibility hints and inductive/constructor/recursor metadata. Only theorem proof values and expression source metadata are omitted. An independent environment-ownership walk checks complete coverage, including private and generated constants.All 5,728 original inventory names match exactly, covering all 5,726 original project-owned constants: zero removals or type/value/universe/safety differences. The inventory has 5,774 base rows because some generated constants occur in multiple module memberships; it also records two imported generated equation helpers. Head has 5,779 rows / 5,733 names and covers all 5,731 owned constants. The five additions are three general extensionality lemmas, one generated proof helper and the private conjugated-word lemma. Expected ownership annotations change for moved public foundations. Every difference was inspected; generated constructor metadata stays in its original module. The post-measurement clean head passes the same audit.
Canonical original-declaration identity projection, excluding module ownership, is byte-identical: SHA-256
d4870f337af6a1460aefe8dfe922de335e1966daf42de41fd65dacdca28d9736. Base full-manifest SHA-256:644a1d83d17d806683f27d70df950f3d6e755a88d5b34ea27a5ee9815270aeca; head:aaeb65a0394de1215e5aec8686c3e71c1774bd46fce8760de2c0c1e4d443b5b1.Controlled measurements. Six sequential builds in base/head, head/base, base/head order on the Azure VM. Each deletes only selected-project Lean/IR artifacts, compiles all 87 base or 89 head modules, retains identical cached pinned dependencies, and verifies source SHA-256 inventories before and after. No other compiler or profiler from this task overlaps a measured build.
A separate sampler follows descendants created by every parent thread and reads Linux
smaps_rollupwith a 50 ms delay between polls. It records the maximum simultaneous sum of RSS and PSS. PSS apportions shared resident pages. GNU time reports largest-child RSS separately. All memory values below are KiB.Observed median reductions: 12.55% tree PSS, 18.93% tree RSS, 6.31% largest-child RSS and 1.39% user CPU. Wall time increases 115.14 → 120.44 s. This VM is shared, with no CPU isolation or OS-cache flushing; memory peaks depend partly on parallel module overlap. These are selected-project measurements, with no whole-pool speedup claim.
Validation.
+LeanPoolroot build.scripts/ci/lint-project.leanover all 89 modules / 5,731 declarations, including slow Mathlib/Batteries linters: passed.lake exe lint-style LeanPool.SmallUndecidableGroups.Imports: passed.python -m lean_pool.quality --repo <project-scoped validation view>: passed, including allowed axioms, compiled option/soundness audits, card, reachability, headers and size checks. The view contains this project's complete sources/card and unchanged pinned configuration/root, using its built artifacts.lake exe mk_all --module --checkon that view andgit diff --check: passed.lake shake --force --keep-public LeanPool.SmallUndecidableGroups.Imports: exit 1 with byte-identical pre-existing redundant-import advisories compared with base. Existing public coverage is preserved.Hosted whole-pool CI and independent PR review remain pending. Open for review only; this cycle does not request queue entry, auto-merge or merge.