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 identified in the checker or proof replacements. SummaryAdds
Reviews (1) · Last reviewed commit: "Optimize Brill–Noether closed-cover cert..." · Reviewed by Greptile |
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. A base→head comparison was attempted but its measurements are unavailable (see the run log); modified files are omitted from the tables below. Statement changes✅ No statements changed — all 3,667 tracked declarations across 12 modified files kept their type; only proofs / definition bodies changed. Also: 925 declarations added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another. ➕ Declarations added (925)
Statements are compared textually against the merge base (comments and whitespace ignored; Total heartbeats: 1,997 maxHeartbeats units across 1 valid file (10,783 added LOC). Sum of Count-heartbeats wall-clock total: 2.69 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.BrillNoetherGraphs.Utilities.Subdivision.IndexedClosedCheck |
5.20 s |
Per-file `lean --profile` output
LeanPool/BrillNoetherGraphs/Utilities/Subdivision/IndexedClosedCheck.lean
import took 3.19s
cumulative profiling times:
attribute application 0.0609ms
compilation (IR) 0.801ms
compilation (LCNF base) 11.4ms
compilation (LCNF impure) 4.11ms
compilation (LCNF mono) 8.68ms
congr simp thm 0.903ms
elaboration 37.5ms
fix level params 0.247ms
import 3.19s
initialization 34.6ms
instantiate metavars 0.465ms
interpretation 284ms
let-to-have transformation 0.083ms
linting 10.4ms
module linting 0.00157ms
overlappingInstancesLinter 2.27ms
parsing 7.76ms
process pre-definitions 2.98ms
share common exprs 1.61ms
simp 8.27ms
tactic execution 23.3ms
tacticAnalysis 22.4ms
type checking 6.4ms
typeclass inference 18.5ms
real 4.25
user 1.65
sys 1.35
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closed-cover cell proofs repeatedly check the same witness geometry and search cone lists during kernel reduction. This refactor shares the geometry checks and supplies checked cone-row hints, reducing the complete Brill–Noether project’s observed cold build wall time by 12.7% while preserving every existing declaration.
BrillNoetherGraphs was selected because its 566 source files include expensive independent certificate replays: the baseline row-03 module alone took 447 seconds, and 917 cell checks repeat the same finite calculations. The final change:
checkClosedRows_soundto recover the originalcheckClosedresult, including all slope and endpoint conditions.as_aux_lemmawrappers retain the original private kernel auxiliaries.LeanPool.leanremain unchanged. All 13 changed files belong to this existing project.Measured base:
edbe5bd56f476cc2965564676b66199f281ab714. Head:62b4f290a1283e87a7195abc9e14e1fd26af223e. Both use the existing Lean/Mathlib 4.35.0-rc3 pins and unchanged Lake options. Before each full build, every project-owned Lean/IR artifact and the top-level entry artifacts were removed; the same pinned dependency cache was retained. All ten dependency checkouts match their pins and are clean./usr/bin/time -v)Wall time fell by 166.53 seconds; RSS is essentially unchanged. The row-03 replay fell from 447 to 401 seconds. These are one baseline and one final cold-project measurement on a shared Azure VM, with warm dependency artifacts; they are observations rather than a CI timing guarantee.
The invariant audit imports the complete project at Lean’s private environment level with extensions disabled and serializes every owned constant, including generated/private declarations. It compares SHA-256 manifests of structural types and all non-theorem values, plus names, module ownership, universe parameters, kinds and safety levels. The theorem proof bodies are the permitted exclusion. All 31,059 pre-existing records match; none are missing or changed. The 1,856 added declarations introduce no unsafe/partial definitions or axioms. Reversing the new helpers and 917 proof-body replacements also recovers the original mathematical source byte-for-byte across all 11 edited mathematical source files.
Validation passed:
--wfail, covering all 568 project modules.scripts/ci/lint-project.leanon every owned module: 32,915 declarations passed the slow declaration linters.lake exe lint-style LeanPool.BrillNoetherGraphs.Importsandlake exe mk_all --module --check.Quot.sound,Classical.choiceandpropext.git diff --check.A read-only
lake shakeaudit, after an explicit successful project freshness check, produced legacy import suggestions. Public imports are retained under the API invariant. Whole-pool CI and independent review remain pending; no repository gates, settings or waivers were changed.