Repository navigation
perf(Vlasov): reduce peak compiler RSS by 11.39% - #688
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 actionable merge blocker was found in the reviewed changes. SummaryThe PR splits the Vlasov development into seven compilation units and shares Picard-series and convolution estimates.
Reviews (2) · Last reviewed commit: "Remove unused aliases to generated Vlaso..." · 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 108 tracked declarations across 5 modified files kept their type; only proofs / definition bodies changed. Also: 0 declarations added, 138 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another. ➖ Declarations removed (138)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 1 → 1 (+0, +0.0%). Commands: 3 → 3. Per-file wall sum: 6.7 s → 6.7 s (+0.3%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 1 compared — 0 cheaper, 0 costlier, 1 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: 4,827,849 maxHeartbeats units across 7 valid files (10,457 added LOC). Sum of Count-heartbeats wall-clock total: 395.58 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.Vlasov.OT.TestApproximation |
32.00 s |
LeanPool.Vlasov.OT.FlowDifferentiability |
24.00 s |
LeanPool.Vlasov.OT.Continuation |
22.00 s |
LeanPool.Vlasov.OT.CharacteristicConstruction |
18.00 s |
LeanPool.Vlasov.OT.CharacteristicFlow |
15.00 s |
LeanPool.Vlasov.OT.FrozenField |
13.00 s |
LeanPool.Vlasov.ForMathlib.VariationalEquation |
12.00 s |
LeanPool.Vlasov.OT.LocalWellPosedness |
9.70 s |
Per-file `lean --profile` output
LeanPool/Vlasov/ForMathlib/VariationalEquation.lean
import took 2.75s
tactic execution of Lean.Parser.Tactic.refine took 111ms
tactic execution of Lean.Parser.Tactic.refine took 109ms
tactic execution of Lean.Parser.Tactic.refine took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Set___elabRules_Mathlib_Tactic_setTactic_1._boxed took 109ms
tactic execution of Lean.Parser.Tactic.refine took 1.58s
cumulative profiling times:
aesop 31ms
attribute application 2.29ms
blocked (unaccounted) 2.27s
compilation (IR) 0.0974ms
compilation (LCNF base) 0.731ms
compilation (LCNF impure) 0.301ms
compilation (LCNF mono) 0.515ms
congr simp thm 11.6ms
dsimp 25.1ms
elaboration 281ms
fix level params 9.05ms
import 2.75s
initialization 30.4ms
instantiate metavars 11.9ms
interpretation 1.61s
let-to-have transformation 0.854ms
linting 115ms
module linting 0.00196ms
norm_num 32.1ms
overlappingInstancesLinter 21.5ms
parsing 69.4ms
process pre-definitions 55.5ms
ring 82.5ms
share common exprs 43ms
simp 178ms
tactic execution 3.49s
tacticAnalysis 213ms
type checking 338ms
typeclass inference 3.99s
real 6.74
user 11.57
sys 1.23
LeanPool/Vlasov/OT/CharacteristicConstruction.lean
import took 1.26s
tactic execution of Mathlib.Tactic.nlinarith took 460ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 136ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 266ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 331ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 312ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 434ms
tactic execution of Lean.Parser.Tactic.refine took 112ms
tactic execution of Lean.Parser.Tactic.refine took 118ms
tactic execution of Lean.Parser.Tactic.refine took 100ms
type checking took 117ms
tactic execution of Lean.Parser.Tactic.refine took 115ms
tactic execution of Lean.Parser.Tactic.refine took 102ms
cumulative profiling times:
attribute application 0.423ms
congr simp thm 28.4ms
dsimp 7.67ms
elaboration 718ms
fix level params 14.7ms
import 1.26s
initialization 29.5ms
instantiate metavars 44.2ms
interpretation 7.66s
let-to-have transformation 2.32ms
linting 421ms
module linting 0.00149ms
norm_num 1.41s
overlappingInstancesLinter 46.6ms
parsing 225ms
process pre-definitions 185ms
ring 644ms
share common exprs 215ms
simp 746ms
tactic execution 6.21s
tacticAnalysis 733ms
type checking 1.21s
typeclass inference 8.16s
real 10.02
user 29.38
sys 1.20
LeanPool/Vlasov/OT/Continuation.lean
import took 1.23s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 253ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 265ms
tactic execution of Lean.Parser.Tactic.exact took 158ms
tactic execution of Lean.Parser.Tactic.exact took 225ms
tactic execution of Lean.Parser.Tactic.exact took 151ms
tactic execution of Lean.Parser.Tactic.exact took 217ms
tactic execution of Lean.Parser.Tactic.exact took 150ms
tactic execution of Lean.Parser.Tactic.exact took 154ms
tactic execution of Mathlib.Tactic.nlinarith took 686ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 548ms
cumulative profiling times:
attribute application 0.48ms
blocked (unaccounted) 0.555ms
congr simp thm 30.7ms
elaboration 757ms
fix level params 13.6ms
import 1.23s
initialization 30.8ms
instantiate metavars 49ms
interpretation 4.62s
let-to-have transformation 2.65ms
linting 390ms
module linting 0.0016ms
norm_num 243ms
overlappingInstancesLinter 40.3ms
parsing 244ms
process pre-definitions 233ms
ring 399ms
share common exprs 146ms
simp 597ms
tactic execution 7.26s
tacticAnalysis 697ms
type checking 1.12s
typeclass inference 7.41s
real 8.53
user 25.11
sys 1.12
LeanPool/Vlasov/OT/FlowDifferentiability.lean
import took 1.26s
simp took 178ms
simp took 172ms
simp took 161ms
simp took 170ms
tactic execution of Lean.Parser.Tactic.exact took 154ms
type checking took 359ms
simp took 174ms
simp took 170ms
simp took 160ms
simp took 168ms
tactic execution of Lean.Parser.Tactic.exact took 153ms
tactic execution of Lean.Parser.Tactic.exact took 149ms
type checking took 477ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.23s
tactic execution of Lean.Parser.Tactic.refine took 108ms
tactic execution of Lean.Parser.Tactic.exact took 149ms
tactic execution of Lean.Parser.Tactic.refine took 117ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2.33s
type checking took 168ms
tactic execution of Lean.Parser.Tactic.obtain took 134ms
tactic execution of Lean.Parser.Tactic.exact took 151ms
tactic execution of Lean.Parser.Tactic.exact took 114ms
type checking took 103ms
tactic execution of Lean.Parser.Tactic.obtain took 119ms
tactic execution of Lean.Parser.Tactic.refine took 132ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.17s
tactic execution of Lean.Parser.Tactic.obtain took 121ms
tactic execution of Lean.Parser.Tactic.exact took 148ms
tactic execution of Lean.Parser.Tactic.clearValue took 247ms
tactic execution of Lean.Parser.Tactic.exact took 1.42s
type checking took 129ms
tactic execution of Lean.Parser.Tactic.refine took 109ms
tactic execution of Lean.Parser.Tactic.refine took 182ms
tactic execution of Lean.Parser.Tactic.refine took 126ms
tactic execution of Lean.Parser.Tactic.refine took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 2.22s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Set___elabRules_Mathlib_Tactic_setTactic_1._boxed took 156ms
tactic execution of Lean.Parser.Tactic.refine took 119ms
type checking took 113ms
tactic execution of Lean.Parser.Tactic.refine took 139ms
tactic execution of Lean.Parser.Tactic.refine took 132ms
cumulative profiling times:
attribute application 0.303ms
congr simp thm 13.7ms
dsimp 8.52ms
elaboration 649ms
fix level params 10.5ms
import 1.26s
initialization 29.4ms
instantiate metavars 31.1ms
interpretation 5.7s
let-to-have transformation 2.38ms
linting 218ms
module linting 0.00193ms
norm_num 35.3ms
overlappingInstancesLinter 29.9ms
parsing 143ms
process pre-definitions 141ms
ring 96.3ms
share common exprs 78.2ms
simp 1.6s
tactic execution 14.5s
tacticAnalysis 440ms
type checking 2.03s
typeclass inference 12.5s
real 12.99
user 38.97
sys 1.23
LeanPool/Vlasov/OT/FrozenField.lean
import took 1.25s
tactic execution of Lean.Parser.Tactic.exact took 154ms
tactic execution of Lean.Parser.Tactic.exact took 231ms
tactic execution of Lean.Parser.Tactic.exact took 153ms
tactic execution of Lean.Parser.Tactic.exact took 212ms
type checking took 110ms
typeclass inference of MeasureTheory.Measure.IsNegInvariant took 119ms
tactic execution of Lean.Parser.Tactic.refine took 107ms
tactic execution of Lean.Parser.Tactic.refine took 110ms
type checking took 196ms
cumulative profiling times:
attribute application 0.151ms
congr simp thm 7.97ms
elaboration 272ms
fix level params 2.85ms
import 1.25s
initialization 30.7ms
instantiate metavars 7.68ms
interpretation 731ms
let-to-have transformation 0.955ms
linting 77.5ms
module linting 0.00167ms
norm_num 23.2ms
overlappingInstancesLinter 12.3ms
parsing 40.5ms
process pre-definitions 47ms
ring 12.2ms
share common exprs 23.7ms
simp 458ms
tactic execution 2.86s
tacticAnalysis 144ms
type checking 763ms
typeclass inference 5.53s
real 5.89
user 11.90
sys 1.10
LeanPool/Vlasov/OT/LocalWellPosedness.lean
import took 1.21s
cumulative profiling times:
attribute application 0.211ms
congr simp thm 3.85ms
dsimp 4.1ms
elaboration 410ms
fix level params 5.05ms
import 1.21s
initialization 30.1ms
instantiate metavars 13.4ms
interpretation 1.06s
let-to-have transformation 1.41ms
linting 140ms
module linting 0.00148ms
norm_num 11.3ms
overlappingInstancesLinter 18.7ms
parsing 104ms
process pre-definitions 57.6ms
ring 72.2ms
share common exprs 39.5ms
simp 65.7ms
tactic execution 1.42s
tacticAnalysis 293ms
type checking 375ms
typeclass inference 1.62s
real 3.67
user 6.65
sys 1.02
LeanPool/Vlasov/OT/TestApproximation.lean
import took 1.23s
tactic execution of Lean.Parser.Tactic.refine took 129ms
tactic execution of Lean.Parser.Tactic.refine took 134ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 513ms
tactic execution of Lean.Parser.Tactic.exact took 118ms
type checking took 158ms
typeclass inference of AddMonoidHomClass took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 113ms
tactic execution of Lean.Parser.Tactic.exact took 151ms
tactic execution of Lean.Parser.Tactic.exact took 160ms
tactic execution of Lean.Parser.Tactic.exact took 145ms
tactic execution of Lean.Parser.Tactic.exact took 147ms
typeclass inference of ZeroHomClass took 118ms
typeclass inference of ZeroHomClass took 121ms
interpretation of Mathlib.Meta.Positivity.evalAdd._lam_0._boxed took 164ms
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 178ms
tactic execution of Lean.Parser.Tactic.clearValue took 202ms
interpretation of Mathlib.Meta.Positivity.evalAdd._lam_0._boxed took 155ms
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 227ms
interpretation of Mathlib.Meta.Positivity.evalAdd._lam_0._boxed took 246ms
tactic execution of Mathlib.Tactic.nlinarith took 499ms
cumulative profiling times:
attribute application 0.247ms
congr simp thm 9ms
dsimp 8.71ms
elaboration 396ms
fix level params 5.12ms
import 1.23s
initialization 30.3ms
instantiate metavars 14.9ms
interpretation 2.16s
let-to-have transformation 1.32ms
linting 103ms
module linting 0.00145ms
norm_num 13.6ms
overlappingInstancesLinter 14.6ms
parsing 70.7ms
process pre-definitions 73.9ms
ring 44.6ms
share common exprs 42ms
simp 198ms
tactic execution 5.45s
tacticAnalysis 191ms
type checking 890ms
typeclass inference 9.69s
real 11.12
user 20.25
sys 1.11
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "This refactor splits the Vlasov flow, differentiability, weak-solution and well-posedness arguments into focused modules and shares their repeated Picard and convolution estimates. The inspected proofs retain explicit integrability, moment and time-window hypotheses, while public re-exports and documented compatibility aliases preserve the existing module interfaces. The shared IVP specification keeps the explicit Dyson-series witness. These changes improve maintainability without hiding the analytic argument behind broad automation. The reported 11.39% reduction in per-process peak RSS is arithmetically consistent but remains an author measurement; the small, variable wall-time difference does not establish a reliable speedup. The compiled declaration audit was also author-run. Hosted CI and the matching configured review remain separate requirements.",
"assessment": {
"scope": "module split and shared analytic estimates",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The module boundaries and shared estimates make the existing proofs easier to maintain, with no actionable regression found in the source review."
},
"verdict": "approve",
"findings": []
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | module split and shared proof estimates |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ➖ unchanged |
| Risk | ✅ low |
The module boundaries and shared lemmas reduce duplication without obscuring the arguments or broadening proof automation.
Tokens: 1,213,194 in / 11,431 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.0242 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Address configured review2217 by removing42 unused private aliases to tactic-generated simp/abel constants. Preserve37 named aliases, non-alias mathematical statements/proofs, imports and gates. Old compiled-count/benchmark evidence remains historical; fresh current-head validation is required.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "The configured review identified generated-helper coupling I missed in the initial source review. This child removes 42 unused private aliases to generated simp/abel constants, retaining all 37 named private compatibility aliases, non-alias mathematical statements and proofs, and original public import paths.",
"assessment": {
"scope": "Generated-private compatibility alias cleanup following the Vlasov module split",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Removing unused dependencies on tactic-generated names preserves the useful module split and named compatibility interfaces."
},
"verdict": "approve",
"findings": [],
"verification_scope": "The prior twelve-file source review is retained through the inspected three-file deletion. All twenty project bodies were authenticated and searched; removed names have no written clients beyond their alias declaration and target. This is static source evidence, not fresh compiled-environment equivalence.",
"historical_validation": "The 514-declaration preservation audit, 596 compiled count, measurements and successful authored CI belong to 9d6758f. This child intentionally drops 42 generated-private identities; those old counts, full private-environment preservation and new performance results are not claimed.",
"gate_status": "Source accepted only at this child. Matching configured 2217 request_changes remains historical at its original head. Fresh current-head authored CI, configured review and normal native queue checks remain required. No queue or automatic merge is enabled.",
"reviewed_commit": "b7d5c2a7641359be28d0e98f2cda00495aee1103"
}
|
/review Please run the configured review for exact head |
1 participant
Vlasov's long weak solution and well-posedness files retain substantial elaboration state and repeat Picard-series and convolution estimates. This change shares those arguments and separates the analysis, flow construction, frozen field, flow differentiability, test approximation, local existence, continuation and stability layers while retaining the intended named mathematical API and all original public import paths.
5199f6df453142c54782d7d7812c9ffa3c6b98e0. Measured head:9d6758f066dd89b3690fa20ea59436da8d9f449c. Current repair head:b7d5c2a7641359be28d0e98f2cda00495aee1103.4.35.0-rc3; Mathlibc55e6e786f49471c72fbddbec5415808896aec1e. Pins, configuration and gates are unchanged.WeakToLagrangian(31.22 s) and repeated Picard continuity/integral arguments (roughly 2.75–3.18 s each) as useful targets; these profile figures were selection evidence, separate from the controlled measurements below.Concrete changes:
WeakEvolutionEqOnretains its original module.lake shake, including unused broad trigonometry and covering imports. Regenerate only this project's import index; keepLeanPool.leanfixed.Historical invariant audit at measured head
9d6758f: before editing, Lean environment inspection recorded every compiled project declaration, including private/generated auxiliaries. The comparison retains full elaborated types, universe parameters, safety and otherConstantInfometadata, export status, and complete non-theorem values. Only theorem bodies are omitted; inaccessible macro scopes on bound variable names are alpha-normalized. Constant names, named binder bases/order, universes and value structure are not normalized. At measured head9d6758f, all 514 existing declarations matched; none were missing or modified. There are 82 additions and 125 intended moves between source modules. Private compatibility aliases deliberately preserve old compiled helper identities. All 13 original module import paths also preserve their exported project declarations.Reviewer repair at
b7d5c2a7641359be28d0e98f2cda00495aee1103. Configured review 2217 identified 42 unnecessary private aliases to tactic-generated_simp/_abelconstants. The repair removes those aliases and retains the 37 named private aliases, all non-alias mathematical declarations/proofs and all original public import paths. It intentionally stops preserving the removed generated-private identities. The old 514-declaration invariant and 596-declaration validation count are not asserted for this child, and the measurements below remain historical at9d6758f. Fresh current-head hosted CI and matching configured review are required; no new benchmark or compilation result is claimed here.Controlled measurement: remove only the isolated worktree's Vlasov library/IR outputs before each build; keep dependencies warm; alternate three base/head pairs, sequentially under the cooperative machine build lock. Run
/usr/bin/time -f '%e %U %S %M' taskset -c 8-11 lake build LeanPool.Vlasov.Imports. Record source fingerprints and require the shared Mathlib checkout to be clean and pinned before and after every build. Earlier source variants are excluded from these medians.Observed median wall reduction: 1.65%. Observed median peak compiler child process RSS reduction: 11.39%. Median user CPU time is 221.87 → 218.42 seconds; median system CPU time is 8.30 → 11.70 seconds. The VM is shared, so wall-time variation limits causal inference. RSS measures the largest individual process, not the sum of concurrent compiler processes.
Historical validation passed on measured source
9d6758f(not fresh validation of the repair child):lake build --wfail LeanPool.Vlasov.Imports.lake exe lint-style LeanPool.Vlasov.Imports.lake exe mk_all --module --checkover the repository; selected-project static quality/card checks using byte-identical sources and unchanged configuration.lake shake --force --keep-public LeanPool.Vlasov.Imports, andgit diff --check.Full-pool validation and protected PR checks remain CI work. This PR does not request merging or auto-merge. Daily documentation publishing is asynchronous; the required Documentation preflight and all other protected checks remain applicable.