Repository navigation
perf(DavisKahan): narrow proof imports and simplify operator estimates - #823
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 issue was found in this import and proof refactor. SummaryThis refactor narrows imports and replaces broad arithmetic searches with focused proofs.
All supplied changes and the omitted diff were reviewed. Builds, compiled-environment audits, and timing measurements were not rerun. External source and license evidence was not independently reverified; this PR leaves those records unchanged. Vilin97 explicitly identifies the removal of external Mathlib reexports as intentional. No separate loss of owned declarations was established. Vilin97 also acknowledges the clean-run wall-time increase for Reviews (1) · Last reviewed commit: "perf(DavisKahan): narrow proof imports a..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 2,240 tracked declarations across 107 modified files kept their type; only proofs / definition bodies changed. Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 15,694,051 → 14,882,837 (-811,214, -5.2%). Commands: 5,178 → 5,178. Per-file wall sum: 2836.4 s → 1558.9 s (-45.0%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 102 compared — 31 cheaper, 0 costlier, 71 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: 680,476 maxHeartbeats units across 2 valid files (78 added LOC). Sum of Count-heartbeats wall-clock total: 58.28 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 |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Approve — source review of 6fdd2a50f060c828025ca9bedaff64b445505c61; required CI is still running.
The narrower tactic imports and explicit arithmetic hypotheses make the proof dependencies easier to follow. The operator arguments preserve their structure: coercivity still supplies injectivity and closed range, inverse estimates retain their positivity and nonzero-denominator guards, and the sharpness calculation uses equality of the two explicit Gram matrices with existing singular-value lemmas. Reusing the existing Cauchy–Schwarz helper improves maintenance without adding an abstraction layer.
- Assessment: maintainability improved; arithmetic proofs more explicit; integration risk medium because imports change across 107 existing files. No blocking source findings.
- Scope: all 107 files remain within DavisKahan. The written declaration contracts and ambient assumptions are preserved; external Mathlib reexports are intentionally narrowed. Hosted CI must still confirm elaboration and downstream integration.
- Validation: proper Lean Action CI
43662433374/a1is building the project. Author-reported private audits and timings are not validation credit for this review.
This independent refactor review supplies the source verdict. I will enqueue the accepted head through normal protections once its applicable required checks pass and current-main readiness is verified.
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | import narrowing and targeted proof rewrites |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
Explicit arithmetic dependencies and shared helper arguments make these proofs easier to repair and maintain, with no actionable regression identified.
Tokens: 1,536,090 in / 8,414 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.2706 (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.
Ready for review: reduce DavisKahan compilation costs while preserving every owned declaration.
Scope and changes
DavisKahan is a completed project with 1,082 modules and about 302,000 lines of Lean. The reference clean build took 43:31.32, with Sharpness the slowest module at 189 seconds and BeamSection9 the largest compiler process by sampled RSS. Its broad tactic imports and foundational proof dependencies made it a useful single-project target.
Mathlib.Tacticimports with explicit private tactic imports, retaining metaprogram dependencies withshake: keep.Semantic invariant
Base:
503d6a74ee9be787839d823d271a0673e1283b1d; head:6fdd2a50f060c828025ca9bedaff64b445505c61.Before editing, save the complete compiled baseline, source snapshot and a Lean environment manifest. Compare the final environment exactly, rather than up to definitional equality. A second audit reads each module's own
ModuleData.constantsand its public export records, so repeated names of Lean-generated helpers cannot mask a difference in another module.Both audits pass for all 21,500 entries: 17,385 theorem entries, 3,569 definitions, 179 inductives, 188 constructors and 179 recursors. There are zero changed types, universe lists, non-theorem values, safety/reducibility/kernel metadata, export records, removed declarations, additions or shadowed names. Only theorem proof bodies are excluded from equality; 179 informational proof hashes differ. Parsed source signatures also match exactly across all 107 changed files. No definition, instance, notation, namespace or theorem statement is edited.
The comparison encodes complete Lean expressions as DAGs, canonicalizes the JSON, and compares it exactly using lossless deterministic compression. It does not infer semantic preservation from source text or proof hashes. The pre-edit environment audit and the module-local audit both pass. The latter reconstructs the baseline from the original compiled artifacts retained before editing.
Raw module manifest SHA-256:
98abb4cb2d0cc01208498064bde2ef9462edafdc5f23e3336ff4f29c7a6942068e61fce162c545b61b8d277c82a4fe32c6a223ad29c9b6311718880528245218Measurements
Both measurements run on the same Azure VM, rebuilding all 1,082 owned modules from absent project artifacts while retaining the pinned prebuilt dependencies:
Only this isolated worktree's DavisKahan artifacts under
.lake/build/lib/lean/LeanPool/and.lake/build/ir/LeanPool/are removed. GNU time's maximum RSS is the largest process in the build, not the sum of concurrent processes. Module wall times are taken from the Lake logs.The initial reference build started at
e5baf4dfa2e55f1dc4bb25558f1432209fc41d00. Intervening main commits were checked to leave the project, pinned dependencies, Lake settings and compiler plugin byte-identical. Lean remains 4.35.0, with Mathlib56a005855ea17e0b0958f73ec801ae140b0a1679; no version or gate changes are included.Validation
lake build LeanPool.DavisKahan.Imports, with the repository watchdog and compiler plugin.scripts/ci/lint-project.lean, supplied all 1,082 owned modules: 21,403 unique environment declarations pass.lake exe lint-style LeanPool.DavisKahan.Imports.lake exe mk_all --module --checkandgit diff --check. No generated index changes are required.python3 python/lean_pool/build_time_limits.py check --log head-cold.log --base 503d6a74ee9be787839d823d271a0673e1283b1d: all 107 changed modules covered, maximum 205 s, zero 600-second violations.Limits
This is a controlled artifact-clean comparison on a busy shared VM. CPU scheduling and the OS page cache are not isolated or reset. Exploratory replays used a separate CPU during the baseline, and the VM hosts unrelated work. Aggregate CPU time is essentially unchanged; wall-time gains are observations rather than a guaranteed speedup on other machines. The baseline also includes the small one-time compiler-plugin build; the optimized run reuses it. External Mathlib proof dependencies are intentionally no longer reexported through every intermediate module; consumers now import their providers explicitly. Owned declarations and owned reexports are preserved by the audits above.
All 3,249 checked
.olean/private/server artifact files and associated hashes are byte-identical between the validated build and the fresh measured build. All 107 final source hashes also match.Sharpness had clean-run wall times of 189 →205 s. To investigate that result, replay the saved base and final sources/dependencies in base/head/head/base order, one compiler at a time, with the same affinity, six threads, plugin/options, and normal
.olean/.ilean/C output. All four replays pass. Median CPU time falls 145.315 →138.735 s (4.53%), with median RSS 1,914,656 →1,848,962 KiB (3.43%). This supports the inference that the isolated file-wall regression reflects scheduling variation.The one-second sampler saw a sum of compiler RSS of 10,069,244 →9,800,964 KiB (2.66% lower). This proxy counts shared mapped pages repeatedly; the baseline sampler also began after early modules. It is not a measurement of total physical VM memory.
Daily documentation publication is asynchronous and is not used as a merge gate. This PR is left open for the applicable validation workflows and independent review; it is not merged automatically.