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 issue remains in the reviewed changes. SummaryThe PR narrows private tactic imports and splits large certificate checks into reusable private proofs. The latest update removes 27 unused private projection theorems.
Reviews (2) · Last reviewed commit: "Remove unused private ConwaySoifer proje..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Vilin97
changed the title
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "At 0e26afd, this refactor narrows 101 private tactic imports and stages 24 certificate checks through explicit tail lemmas. The original public imports, written contracts, certificate data and soundness interface are retained. The 27 unused private projection wrappers have been removed; the shared conjunction proofs and every live consumer remain. I accept the documented memory/time trade-off: the single-run 11.72% process-RSS reduction and 12.39% wall-time increase belong to the original 68c6b5c measurement, and the updated description makes no new measurement claim for this cleanup. This is source approval; current-head configured review and all applicable hosted/protected checks remain pending.",
"assessment": {
"scope": "tactic import narrowing and staged certificate proofs",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "medium",
"assessment_one_sentence": "The narrower imports and explicit, reused certificate checks are maintainable after removing the unused private wrappers; the documented performance trade-off is acceptable for this memory-focused refactor."
},
"verdict": "approve",
"findings": []
}
|
/review |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | import narrowing and certificate-check staging |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ➖ unchanged |
| Risk | ✅ low |
The staged checks make failures easier to isolate and reuse checked results without introducing actionable maintenance debt.
Tokens: 1,295,147 in / 8,439 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $5.3072 (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.
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 2,011 tracked declarations across 105 modified files kept their type; only proofs / definition bodies changed. Also: 45 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 (45)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 12,948,136 → 13,571,678 (+623,542, +4.8%). Commands: 3,372 → 3,417. Per-file wall sum: 2394.3 s → 2788.3 s (+16.5%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 105 compared — 44 cheaper, 4 costlier, 57 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
Per-project compile cost (top 2 of 2 projects by |Δ heartbeats|):
Advisory only — never blocks merge. Full log uploaded as the |
|
Current-head cost assessment for I accept this cost trade-off for the memory-focused refactor: the named tail checks retain explicit dependencies and debugging boundaries, and all 27 unused projection wrappers are removed. The 11.72% process-RSS reduction remains an attributed measurement of the original The configured review approves this same head. Source acceptance stands; applicable hosted/protected checks and normal native queue validation remain required. |
This branch has not been deployed
1 participant
Current source head:
0e26afd86c06e76007959fc163ed52749d0bf7b5. Review cleanup removes 27 newly introduced, unused private projection wrappers (162 lines in three certificate modules). The shared tail proofs, conjunction bundles, certificate data, public statements and live proof scripts are unchanged.The measurements, environment-exporter counts and local validation listed below apply to the measured commit
68c6b5cd484976c2e6f3ce8f78f87f5099bb9339. They have not been rerun on the cleanup commit; no new performance measurement or compiled-environment certificate is claimed for the current head. Current-head hosted checks and configured review remain required.ConwaySoifer's large certificate checks raise peak compiler memory. This refactor lowers the measured maximum compiler-process RSS by 11.72%, from 2,245,080 to 1,981,952 KiB, while preserving every existing declaration. Wall time increased by 12.39% in the clean comparison; this is a memory optimization with a measured time tradeoff.
ConwaySoifer was selected from local size, import and profiling evidence: 841 modules, 559,348 source lines, 101 broad private
Mathlib.Tacticimports, and expensive kernel certificate checks. The change narrows those 101 import headers to the tactic modules actually needed and restructures checks in fourAowncertificate modules. Private bundled lemmas verify fan tails sequentially and reuse their checked results through projections and explicitsimp onlylists. All original public imports are retained. Existing certificate data and mathematical statements are untouched.Base:
b634835ce57618a1331f62c3dae458c88df868d8. Validated head:68c6b5cd484976c2e6f3ce8f78f87f5099bb9339. Immediately before commit,origin/mainwas verified at14ed8c6b29fea045ba2d6fab82fd0a289d9301e2; the selected sources, relevant policies and dependency pins are unchanged from the measurement base. The branch was kept at its audited base rather than rebased to follow unrelated main changes. These use the repository's actual unchanged pin, Lean 4.35.0-rc3 / Mathlibc55e6e786f49471c72fbddbec5415808896aec1e.Before editing, a Lean environment exporter recorded all project-owned declarations, including private and generated declarations. It serializes complete elaborated expression DAGs, types, universe parameters, declaration kinds, safety/partial flags, reducibility metadata, exported visibility, definition values and inductive/recursor metadata. The comparison uses structural SHA-256 fingerprints independent of expression-node numbering and permits only theorem proof-value changes. Result: 257,912 existing declarations retained; zero type/contract changes, zero definition-value changes, zero missing declarations. 59 existing theorem proof bodies differ. All 2,697 additions are private safe theorem declarations, including generated proof auxiliaries; no existing public name is replaced. The source/configuration hashes were frozen for measurement and verified again before publication.
Both measurements removed only the isolated worktree's own
.lake/build, retained the same pinned dependency cache, and ran/usr/bin/time -v env LEAN_NUM_THREADS=4 lake build LeanPool.ConwaySoifer.Imports. All 841 project modules compiled in each run. GNU time reports the maximum descendant-process RSS, not aggregate concurrent build memory. These are single runs on a shared Azure VM; the wall-time regression is observed, but its precise attribution to source changes versus VM load is uncertain. No speedup or aggregate-memory reduction is claimed.Validation on the exact measured source:
lake shake --force --keep-public --fixon selected import candidates, followed by manual tactic-import narrowing and full recompilation.lake env lean --run scripts/ci/lint-project.leanwith all 841 project modules: all existing CI declaration linters passed.lake exe lint-style LeanPool.ConwaySoifer.Imports: passed.git diff --check, exact source-hash verification, and pre-commit base verification: passed.Only ConwaySoifer Lean sources change. Repository checks, configuration and metadata are unchanged. Full-pool and hosted protected checks and independent review remain the normal PR requirements. This PR is opened without merging, enabling auto-merge, or entering the merge queue.