Repository navigation
Reduce GapCVP proof elaboration cost - #808
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 identified in the latest changes or the full-PR rules check. SummaryThe PR reduces proof elaboration work in
Reviews (3) · Last reviewed commit: "Document restricted GapCVP step tactics" · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 7,077 tracked declarations across 39 modified files kept their type; only proofs / definition bodies changed. Also: 2 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 (2)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 3,421,470 → 3,429,159 (+7,689, +0.2%). Commands: 7,143 → 7,160. Per-file wall sum: 389.8 s → 690.8 s (+77.2%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 21 compared — 3 cheaper, 2 costlier, 16 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: — maxHeartbeats units across 0 valid files (846 added LOC). Sum of Count-heartbeats wall-clock total: 0.00 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 |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof elaboration optimization and tactic rewrite |
| Introduces tech debt | 🛑 yes |
| Maintainability | 🛑 regressed |
| Brittleness | ✅ more_robust |
| Risk | 🟡 medium |
Keep the targeted proof rewrites, but restore a single maintenance point for each machine's tactic configuration before merging.
Findings (1)
- duplicated-tactic-configuration —
LeanPool/GapCVP/Part03E.lean:356
The same 28-entry definition list is now repeated at 22 call sites, replacing the shared delimitedCompareStepTac invocation. This pattern extends across 266 calls; Part06B.lean:866 repeats another 23-entry list 20 times. Helper changes and dependency repairs can now require editing many copies instead of one machine tactic. Factor each machine's list into a wrapper around machineStackEquality; add new wrappers alongside the existing exported tactics if their definitions must remain unchanged.
Tokens: 2,210,241 in / 10,335 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $8.9960 (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.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.
Keep existing tactics intact and centralize the identical ordered simplification inputs used by 227 machine proof calls.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Reviewed 08da721 against main d1019ce. The explicit lattice, algebra and matrix proof rewrites are sound on the inspected provider/caller readset. Nineteen shared restricted wrappers now replace 227 repeated lists, preserving their ordered inputs, all existing declaration headers/data definitions and legacy tactics. This addresses the configured review's maintenance finding. Fresh Lean compilation and protected CI at this repaired head remain pending. The public profile covers only 21 of 39 changed files, so I do not infer an overall speedup from it or adopt the author's separate benchmark as independent evidence.",
"assessment": {
"scope": "Existing GapCVP proof implementations and two supporting lemmas",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "Shared restricted wrappers preserve the explicit proof strategy and remove the repeated configuration identified by the configured review."
},
"verdict": "approve",
"findings": []
}
Add the tactic docstrings required by docBlame and tacticDocs for the nineteen new restricted wrappers. No proof or gate changes.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Reviewed dc52824 against main d1019ce. This revision adds the documentation required for the nineteen restricted step tactics. Removing exactly those comments restores the preceding 08da source byte for byte. The shared-wrapper repair still removes 227 repeated lists while retaining their ordered inputs and the existing declarations, data programs and legacy tactics. The preceding head compiled all 39 changed files within 20 seconds, then failed docBlame/tacticDocs for these nineteen undocumented tactics; style and quality did not run. This repaired head requires its own complete protected validation, and receives no prior-head CI credit. No overall speedup is claimed.",
"assessment": {
"scope": "Existing GapCVP proof implementations and two supporting lemmas",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The shared restricted wrappers address the repeated configuration, and the documentation-only follow-up directly addresses the observed lint diagnostics."
},
"verdict": "approve",
"findings": []
}
GapCVP repeatedly elaborates concrete machine transitions and field/parity-matrix expressions. This reduces that work while retaining every existing declaration and the project's public API. GapCVP was selected for its 71 modules, approximately 137,000 source lines, broad initial imports, and repeated transition-proof infrastructure.
The changes:
Invariant audit. Before editing, save the private-level compiled project environment and a declaration manifest from base
d1019ceec2f68c6ff2eaa59a413bc20b3fceac0b. Import base and optimized environments separately and structurally compare every original project-owned declaration, including private and compiler-generated declarations. For theorems, compare the completeConstantVal(name, universes and elaborated type) and mutual-declaration metadata, excluding only the proof body. For every other declaration, compare the completeConstantInfo, including values, safety and constructor/recursor data. Hash manifests are supplemental; this audit compares the actual expressions.Result: 15,835 original declarations, zero forbidden differences. There are 298 changed existing theorem bodies and 272 new Lean constants: 266 generated simplification auxiliaries, two tactic parsers with their implementations, and two supporting lemmas. No existing statement, definition, instance, notation, public import/export path, or namespace API is changed.
Measurements. Paired measurements are at commit
0fa993866eb7146554183f1a92542bf1defa94d8. Each run deletes only GapCVP's compiled and IR artifacts and executes:External dependency and compiler-plugin caches stay warm. Base and optimized sources alternate in the same isolated Azure VM worktree. GNU time records elapsed/user/system seconds and peak process RSS; no profiler or other validation runs alongside a timed build.
Mean wall time: 416.25 → 377.405 seconds (9.33% lower). Mean user CPU time is 7.00% lower; peak process RSS is essentially unchanged. The 10% target was not reached within the six-hour optimization budget. These are shared-VM observations, not a prediction for hosted CI. Representative first-pair Lake module times were Part09 34→25 s and Part13 24→16 s.
Final head
537eaeece59b02c29ad950435012f2b5005fc23fadds one unused-private-import removal and reflows the transition argument lists. A second structural comparison against the measured commit found zero differences across all 16,107 constants, including theorem proof values. The final head also passed an unpaired clean verification build: 444.03 s wall, 490.82 s user CPU, 46.74 s system CPU, peak process RSS 1,942,948 KiB. This unpaired validation run is not included in the paired performance estimate above.Validation. Final-head validation covers a clean warning-free build of all 71 project modules, Mathlib/Batteries slow declaration linters, style, project-scoped repository quality/card/size checks, axiom and option/backdoor audits, the generated project aggregate,
lake shake --force --keep-public LeanPool.GapCVP.Imports, changed-file build-time limits, andgit diff --check. No sources were added or moved, so the generated indexes and fixed LeanPool.lean remain unchanged. Toolchain pins remain Lean 4.35.0 and Mathlib v4.35.0.Only GapCVP Lean source changes. Some definition lists are repeated at restricted-tactic call sites to retain the original tactic definitions unchanged. Full-pool and hosted validation remain the PR's responsibility; no merge or auto-merge is enabled.