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 found in the reviewed changes; external provenance and reported measurements remain independently unverified. SummarySeparates elementary periodicity from the Ramanujan development, shares Bernoulli evaluations, and shortens several proofs without changing their stated results.
Reviews (1) · Last reviewed commit: "Optimize Chudnovsky proof elaboration an..." · 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 745 tracked declarations across 16 modified files kept their type; only proofs / definition bodies changed. Also: 5 declarations added, 1 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another. ➕ Declarations added (5)
➖ Declarations removed (1)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 1,939,195 → 1,868,079 (-71,116, -3.7%). Commands: 787 → 796. Per-file wall sum: 286.3 s → 313.1 s (+9.4%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 8 compared — 3 cheaper, 1 costlier, 4 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: 6,982 maxHeartbeats units across 2 valid files (97 added LOC). Sum of Count-heartbeats wall-clock total: 3.53 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.Chudnovsky.BernoulliValues |
3.20 s |
LeanPool.Chudnovsky.Periodicity |
3.10 s |
Per-file `lean --profile` output
LeanPool/Chudnovsky/BernoulliValues.lean
import took 2.1s
cumulative profiling times:
attribute application 0.0181ms
congr simp thm 0.249ms
elaboration 2.9ms
fix level params 0.134ms
import 2.1s
initialization 23.8ms
instantiate metavars 0.0786ms
interpretation 143ms
let-to-have transformation 0.0261ms
linting 1.34ms
module linting 0.00147ms
norm_num 20.4ms
overlappingInstancesLinter 1.15ms
parsing 1.06ms
process pre-definitions 1.14ms
share common exprs 0.999ms
tactic execution 8.97ms
tacticAnalysis 5.05ms
type checking 8.51ms
typeclass inference 11.8ms
real 2.85
user 0.84
sys 0.85
LeanPool/Chudnovsky/Periodicity.lean
import took 894ms
cumulative profiling times:
attribute application 0.0129ms
congr simp thm 0.324ms
elaboration 3.02ms
fix level params 0.0295ms
import 894ms
initialization 28.7ms
instantiate metavars 0.0805ms
interpretation 125ms
let-to-have transformation 0.0176ms
linting 1.6ms
module linting 0.00156ms
overlappingInstancesLinter 1.05ms
parsing 1.05ms
process pre-definitions 0.465ms
share common exprs 0.251ms
simp 8.18ms
tactic execution 5.11ms
tacticAnalysis 4.17ms
type checking 0.979ms
typeclass inference 6.5ms
real 1.62
user 0.82
sys 0.75
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Reviewed the complete 18-file refactor at f22c348 against main ededf2d. Moving the unchanged periodicity lemma behind Ramanujan's public re-export removes an unnecessary derivative dependency; shared Bernoulli values, the general Clausen formula, explicit cubic witnesses and the named FTC/Fubini argument make the proofs easier to maintain. The rational rounding changes local enclosures while preserving the original hypotheses and one-half conclusions. The public profile covers eight modified-file comparisons and has eight measurement errors; it does not establish the claimed whole-project timing, memory or compiled-declaration invariant. The complete six-parent authored CI has been independently qualified. The requested configured review and native integration validation remain separate pending gates.",
"assessment": {
"scope": "proof and dependency refactor",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The complete source refactor is acceptable, with explicit mathematical structure and existing public entry points preserved; the configured verdict and protected native integration remain pending."
},
"verdict": "approve",
"findings": []
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | module split and proof rewrites |
| Introduces tech debt | 🛑 yes |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
The main rewrites improve clarity and robustness, but remove the newly orphaned private integral helpers before merging.
Findings (1)
- dead-leftover —
LeanPool/Chudnovsky/Liouville.lean:951
The rewrite removes the only consumers ofdouble_integral_diff_apply,double_integral_conj_apply,integrableOn_diff_apply, andintervalIntegral_conj_comp. Those four lemmas and theirintervalIntegral_conjhelper now form an unused private block at lines 840–927. This retains roughly 90 lines of analytic proof code that still require elaboration and maintenance on Mathlib upgrades. Remove the obsolete helper block alongside this rewrite.
Tokens: 1,630,227 in / 9,231 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.6594 (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.
|
Maintainer disposition for The finding in configured review 2301 is factually correct: I accept this bounded retention as a source-quality tradeoff for this PR. The configured verdict remains recorded as The complete 18-file source review and proper six-parent authored CI (18 jobs, 72 steps, own canonical check) are qualified at this head. The public profile has eight valid modified-file comparisons and eight failed measurements; it does not establish whole-project timing, memory, or compiled-manifest claims. Source acceptance therefore stands. Any native queue admission still requires fresh exact-head, current-main, owner, check, and protection guards; the actual cumulative merge-group must pass normal validation. The owner’s NOAUTO instruction remains in force. |
Chudnovsky's modular-function chain waited for the full Ramanujan derivative development to obtain one elementary periodicity lemma. Several proofs also repeated kernel computations or long analytic arguments. This separates that dependency and simplifies the proofs while preserving every original declaration.
The final three-pair series reduced median clean-build wall time 11.33% and median whole-build peak memory 12.17%.
Changes
Periodicity.lean; publicly re-export it from Ramanujan and replace four unnecessary derivative-module dependencies.BernoulliValues.lean, reuse the general Clausen theorem for its special case, and use a direct monic cubic witness and determinant identity.1/2tolerances. Remove 29 broad private import edges and add narrow dependencies; retain the namespace/instance imports needed to preserve the elaborated environment.LeanPool.lean, project metadata, toolchain pins, CI and gates are unchanged.Declaration invariant
Base:
ededf2dc890654488765f9f22dac63af8c047dab.Head:
f22c3485e96799d37643ffc19953442d0ba9c970.Before editing, Lean environment inspection recorded both private and exported declarations. The audit loads with trust level 0 and extensions disabled, serializes expression DAGs for every type and every non-theorem value, and records universe parameters, declaration kinds, safety, reducibility and generated declaration metadata. The final comparison preserves all 2,306 original declarations, including 959 exported declarations, with identical types and non-theorem values. Nine supporting declarations are added; none is removed.
The one investigated metadata difference is the physical module of
periodic_comp_ofComplex_of_vadd. Its source statement and proof are byte-identical and Ramanujan re-exports the same name. All other inspected fields are identical. A separate textual audit preserves all 1,173 original source signatures. Original private support declarations and generated auxiliaries are deliberately retained.A transitive trust audit covers all 2,315 current declarations and 72,769 dependencies: the only axioms are
Classical.choice,propext, andQuot.sound.Controlled measurements
Separate base and candidate worktrees; delete only their own
.lake/buildbefore each run; reuse the same warm pinned dependency artifacts. Each native build usesLEAN_NUM_THREADS=4, CPU affinity 0–3, and/usr/bin/time. Whole-build memory is the transient cgroup's kernelmemory.peak, captured while the cgroup is still alive. Three alternating base/candidate pairs were specified before observing results.Median CPU time: 279.03 → 270.55 s (3.04% lower). Median maximum single-compiler RSS: 1,962,496 → 1,954,708 KiB (0.40% lower). The memory target is met by the whole build's measured peak.
The VM is shared: the third pair is nearly flat on wall time and increases peak memory. These are observed medians, not a claim of a uniform speedup. The only post-measurement source change corrects the new Bernoulli file's attribution; normalized Lean code is identical.
Validation
lake --wfail build LeanPool.Chudnovsky.Importslake env lean --run scripts/ci/lint-project.leanwith all 34 selected-project moduleslake exe lint-style LeanPool.Chudnovskylake exe mk_all --module --checklake shake --force --keep-public LeanPool.Chudnovsky.ImportsAll pass, with warning-free native builds. This uses current main's checked-in Lean/Mathlib v4.35.0-rc3 pins unchanged. Full-pool validation remains for CI; shake's
--forceavoids its unrelated whole-pool artifact sanity check. Audit scripts, manifests, source checkpoints and every timing sample are retained on the VM in/data/codex/scratch/researcher/optimization-20261103T1115/evidence.This PR is open for protected CI and review. Auto-merge is disabled.