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 concrete blocker was found in the reviewed changes. SummaryThis refactor narrows arithmetic tactics to the facts they need and moves three Moore certificates into a graph-independent module.
Performance conclusions rely on the supplied measurements. No build or timing run was performed during this review. The removed Mathlib imports and external source/license evidence were not independently rechecked. Reviews (1) · Last reviewed commit: "perf(ACMax): isolate scalar proofs and t..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)
This build covers the added modules and their dependency cones on top of the measurement environment; modified files are measured without rebuilding the pool. Statement changes✅ No statements changed — all 669 tracked declarations across 49 modified files kept their type; only proofs / definition bodies changed. Also: 3 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 (3)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 6,414,755 → 5,668,482 (-746,273, -11.6%). Commands: 3,808 → 3,810. Per-file wall sum: 460.2 s → 373.8 s (-18.8%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 43 compared — 6 cheaper, 0 costlier, 37 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: 979,595 maxHeartbeats units across 4 valid files (164 added LOC). Sum of Count-heartbeats wall-clock total: 62.93 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.ACMax.Counting.Arithmetic |
3.40 s |
Per-file `lean --profile` output
LeanPool/ACMax/Counting/Arithmetic.lean
import took 1.19s
cumulative profiling times:
attribute application 0.0415ms
elaboration 45.8ms
fix level params 2.95ms
import 1.19s
initialization 32.5ms
instantiate metavars 6.29ms
interpretation 586ms
let-to-have transformation 0.0865ms
linting 47.6ms
module linting 0.00145ms
norm_num 23.8ms
overlappingInstancesLinter 2.07ms
parsing 6.29ms
process pre-definitions 30.8ms
ring 168ms
share common exprs 53.8ms
tactic execution 125ms
tacticAnalysis 19.4ms
type checking 136ms
typeclass inference 251ms
real 2.79
user 2.23
sys 0.93
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.
Independent Source APPROVE at 9928dba2860d790af0eb42962244c89cac397ce8; no findings.
The complete 50-file delta and all 26 changed/new proof commands were reviewed, including the full new 109-line arithmetic module. The explicit polynomial identities, sign bounds, product monotonicity and focused tactic inputs discharge the original graph/counting/spectral obligations. Existing theorem contracts and the three public V9 wrappers remain intact; the new scalar helpers remove large graph contexts from arithmetic proofs.
All 154 removed public imports have actual current public runtime re-export paths to the same modules, checked against the complete project and pinned Mathlib sources. The complete native patches round-trip in both directions; existing written declaration prefixes and all 71 non-theorem commands are preserved. The facade, card, other projects and noncontent inputs remain unchanged. These are source and module-exposure checks, without a claim of compiled environment equality.
Author-reported benchmarks are attributed rather than treated as independently reproduced measurements. Current own authored CI is still pending. Configured review, the current-main infrastructure hold and normal protected native-queue checks remain separate.
{
"summary": "This refactor removes redundant public imports, extracts the graph-free integer inequalities into a shared Arithmetic module while retaining the old public wrappers, and replaces broad arithmetic automation with explicit products, sign bounds and focused tactic inputs. The changed counting and spectral arguments retain their mathematical witnesses and case structure. Actual public reexport paths preserve every removed import at its original module path; no actionable maintainability regression was found.",
"assessment": {
"scope": "import pruning, shared arithmetic extraction and targeted proof elaboration",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The explicit arithmetic interfaces and focused proof steps improve maintainability while preserving the old written contracts and public module exposure."
},
"verdict": "approve",
"findings": []
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | arithmetic tactic rewrite and module extraction |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
Explicit arithmetic dependencies and isolated scalar lemmas make these proofs easier to debug and maintain without losing reusable entry points.
Tokens: 1,215,347 in / 7,361 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $4.9718 (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.
ACMax's arithmetic tactics repeatedly inspect large graph proof contexts. This change limits those tactics to the scalar facts they need and replaces several searches with explicit order and polynomial certificates. It also removes 154 transitively redundant public import statements using
lake shake --keep-public. Only the existing ACMax project and its generated module index change.Base:
edbe5bd56f476cc2965564676b66199f281ab714.Head:
9928dba2860d790af0eb42962244c89cac397ce8.The repository's pins remain Lean 4.35.0-rc3 and Mathlib
c55e6e786f49471c72fbddbec5415808896aec1e.The project was selected from the existing source profile: approximately 33,000 lines across 66 files, with 121.3 seconds of instrumented source time. The cubic certificate and girth transport proof accounted for 7.88 s and 7.69 s of that historical source profile. Those historical numbers guided selection; the measurements below use clean project builds.
Concrete changes:
Counting.Arithmeticmodule. The original theorem names and signatures remain as wrappers.Declaration audit: before editing, import
LeanPool.ACMax.Importswith private visibility, extensions disabled and trust level zero. Serialize every project declaration's owner, name, kind, universes, safety, raw type expression, and complete non-theorem value and metadata. Retain and compare those raw records after the change. All 2,831 original declarations remain: 2,823 records are byte-identical, and eight private generated proof types differ only in bound variable labels. A second Lean traversal renames bound labels only and verifies those eight types are identical in every other expression node and metadata field. Its base raw records are also checked against the original pre-edit manifest. There are zero missing declarations or semantic differences; all 85 original definition values remain byte-identical. Nine declarations are added: six supporting theorems and three generated proofs. No original statement, definition, universe parameter, safety level or public name changes.Observed clean-build results (chronological order):
Mean wall time falls from 302.77 s to 271.085 s (10.47%). Mean user CPU falls from 398.34 s to 362.575 s (8.98%). Peak process RSS does not improve. These are observations from four runs on a shared VM; the remaining wall-time variability limits any claim about other runs or hardware.
A follow-up profile of
StarMoatSharpfound its previously expensive nonlinear arithmetic call at 3.64 s on the base and below the 100 ms reporting threshold on the head. This check did not show the suspected per-module regression.Measurement method: remove every ACMax root/subtree Lean and IR build artifact before each run; retain the same warm, private external dependency cache. Run committed, clean source trees in base/head/head/base order with
LEAN_NUM_THREADS=4 /usr/bin/time -v taskset -c 4-7 lake --wfail build LeanPool.ACMax.Imports. Record each source fingerprint, wall time, user/system CPU and maximum process RSS. CPU affinity is identical on both revisions; the VM remains shared.Validation passed:
lake exe mk_all --module --check.lake exe runLinter --no-build LeanPool.ACMax.Imports(all imported LeanPool declarations).lake exe lint-style LeanPool.ACMax.Imports(selected source import closure).python -m lean_pool.quality --repo .. --static-only.Quot.sound,Classical.choiceandpropext.lake shake --force --keep-public LeanPool.ACMax.Imports: zero remaining suggestions.git diff --check.The full compiled pool and protected review remain for CI. No gates, linter configuration, waivers or toolchain pins change. This PR does not request queue entry or auto-merge.