Repository navigation
Reduce BrillNoetherGraphs certificate replay memory - #695
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 receipt lookup or proof transfers. SummaryReplays the genus-five receipt trees through size-tagged blocks, then transfers the results to the existing checker statements.
Reviews (1) · Last reviewed commit: "Reduce BrillNoetherGraphs certificate re..." · Reviewed by Greptile |
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 2,314 tracked declarations across 9 modified files kept their type; only proofs / definition bodies changed. Also: 504 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 (504)
Statements are compared textually against the merge base (comments and whitespace ignored; Total heartbeats: 1,140 maxHeartbeats units across 2 valid files (7,181 added LOC). Sum of Count-heartbeats wall-clock total: 3.50 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.LowGenus.CompactCellTreeLookup |
5.20 s |
LeanPool.BrillNoetherGraphs.Utilities.Foundations.ChunkedLookup |
0.95 s |
Per-file `lean --profile` output
LeanPool/BrillNoetherGraphs/LowGenus/CompactCellTreeLookup.lean
import took 2.9s
cumulative profiling times:
attribute application 0.0327ms
compilation (IR) 0.274ms
compilation (LCNF base) 1.83ms
compilation (LCNF impure) 1.34ms
compilation (LCNF mono) 1.6ms
congr simp thm 0.459ms
elaboration 9.33ms
fix level params 0.0509ms
import 2.9s
initialization 27.7ms
instantiate metavars 0.0699ms
interpretation 163ms
let-to-have transformation 0.0453ms
linting 3ms
module linting 0.00171ms
overlappingInstancesLinter 1.37ms
parsing 2.19ms
process pre-definitions 2.12ms
share common exprs 0.239ms
simp 9.12ms
tactic execution 21ms
tacticAnalysis 6.01ms
type checking 1.91ms
typeclass inference 0.309ms
real 3.73
user 1.16
sys 1.03
LeanPool/BrillNoetherGraphs/Utilities/Foundations/ChunkedLookup.lean
import took 288ms
cumulative profiling times:
attribute application 0.0224ms
compilation (IR) 0.128ms
compilation (LCNF base) 1.08ms
compilation (LCNF impure) 0.573ms
compilation (LCNF mono) 0.737ms
congr simp thm 0.537ms
elaboration 6.28ms
fix level params 0.112ms
import 288ms
initialization 29.2ms
instantiate metavars 0.152ms
interpretation 47ms
let-to-have transformation 0.0316ms
linting 2.22ms
module linting 0.00145ms
overlappingInstancesLinter 1.06ms
parsing 1.58ms
process pre-definitions 2.06ms
share common exprs 0.224ms
simp 6.52ms
tactic execution 14.9ms
tacticAnalysis 4.85ms
type checking 2.29ms
typeclass inference 1.12ms
real 0.95
user 0.47
sys 0.54
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": "Independent Source review at 4f49add against parent 15542c1, covering all 11 changed files and all 785 complete patch hunks. Size-checked block lookup is proved equal to the original concatenated-table lookup for every index, including fallback cases; the alternate decoder reuses the original checker. All 488 replay proofs transfer back to their existing statements, all 935 old written theorem headers and 875 non-theorem values are preserved, and every new private replay lemma has a transfer consumer. The reported memory/timing measurements and compiled-environment manifest were not independently replayed. This is Source acceptance; configured review, exact-head hosted CI, current-main validation and normal protected queue checks remain separate.",
"assessment": {
"scope": "Refactor of the already accepted BrillNoetherGraphs project; receipt data, tree data, old theorem contracts and existing public imports are retained.",
"introduces_tech_debt": false,
"maintainability": "unchanged",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "The small reusable lookup/equivalence layer changes certificate evaluation without duplicating the checker or weakening the old contracts; the generated compatibility wrappers have explicit consumers and a uniform proof pattern."
},
"verdict": "approve",
"findings": []
}
|
/review Exact head: |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | certificate replay optimization |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ➖ unchanged |
| Risk | ✅ low |
The optimization isolates lookup costs behind small, explicit correctness proofs without sacrificing the existing replay structure; no actionable maintenance regression was found.
Tokens: 1,528,998 in / 13,623 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.3203 (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.
CI was not green for this commit at review time; this review does not replace CI.
1 participant
The generated genus-five cover proofs in
BrillNoetherGraphsrepeatedly traverse concatenated Farkas receipt tables. This change replays their compact trees with a size-checked block lookup, then transfers each result to the original checker statement. The existing receipt data, definitions, public imports, and theorem statements are preserved.as_aux_lemma. The additional private statements keep this strict declaration contract; they account for most of the source growth.Imports.lean;LeanPool.lean, the project card, other projects, and repository checks are unchanged.Invariant audit: the exact base is
15542c175fbeeb83666dc46fc20c4f18f0783e12. Before editing, Lean environment inspection explicitly imported every project source withimportAll := trueand extensions disabled. The manifest serializes expression DAGs for fully elaborated types and all non-theorem values, together with public/private names, universe parameters, declaration kind, safety, reducibility hints, and inductive/constructor/recursor metadata. All 30,066 baseline manifest entries are byte-identical after the change: 30,014 unique declarations, with 52 identical equation-lemma reexports audited separately. There are no missing declarations, type changes, non-theorem value changes, or binder normalizations. The head adds 1,045 supporting declarations. Kernel replay and axiom/backdoor audits validate the changed proof bodies. Fresh exports from both clean builds reproduce the pre-edit base manifest exactly and preserve every baseline entry in the optimized environment.Measurements:
Two-run medians: wall 2191.37 → 2029.19 s (7.40% lower); peak RSS 4,655,522 → 3,655,296 KiB (21.48% lower). This meets the requested 10% RAM criterion. CPU time also falls 7.43%.
Both revisions use current main's unchanged Lean/Mathlib
v4.35.0-rc3pins. The prompt's older 4.34 version is no longer the live repository pin. Each run removes only the project's build artifacts, retains prebuilt dependencies, and runsLEAN_NUM_THREADS=4 /usr/bin/time -v taskset -c 12,13,14,15 lake --wfail build LeanPool.BrillNoetherGraphs.Imports. GNU time's RSS is the largest child process peak, not aggregate VM memory. The four runs alternate baseline–optimized–optimized–baseline; source digests are checked before and after each run. The VM is shared, so timing noise remains possible.The timed optimized checkpoint is
62df0e7e7f8f26bc238c927d9d28fea435fff6c9. Final head4f49adde86affc87ab31a4e0b5c61aa814f94620removes one terminal blank line afterend List; all executable tokens are unchanged. The project was rebuilt afterward, style/index/whitespace checks passed, and all 31,111 optimized declaration records remained byte-identical.Validation:
lake --wfail build LeanPool.BrillNoetherGraphs.Importslake exe runLinter --no-build LeanPool.BrillNoetherGraphs.Importslake exe lint-style LeanPool.BrillNoetherGraphs.Importscd python && uv run python -m lean_pool.quality --repo .. --static-only, plus the unchanged quality checker's_audit_axioms,_run_option_audit(all 567 modules), and_check_project_declarationson the selected projectlake exe mk_all --module --checklake shake --force --keep-public LeanPool.BrillNoetherGraphs.Utilities.Foundations.ChunkedLookupgit diff --checkOpened for review; no merge or auto-merge requested.