| name | version-bump |
| description | Migrate the entire Lean Pool to a new Lean/Mathlib version — bump the toolchain + Mathlib + docbuild pins, repair every project's API breakage and build warnings, pass all CI gates, and open a non-draft PR. Use when the user asks to bump / migrate / upgrade the pool to a specific Lean or Mathlib version (e.g. "bump to v4.33.0-rc1", "migrate to the latest Mathlib"). |
| argument-hint | <target-version> e.g. v4.33.0-rc1 |
Lean Pool whole-pool version bump
Migrate the whole pool to the target version given as the argument (e.g. v4.33.0-rc1). If no version was given, ask for it before starting. Treat the constraints below as the directive.
Hard constraints (never violate)
- No statement drops. Every
theorem/lemma/def/instance/structure/inductive/class/abbrev that exists now must still exist when done.
- Modify a statement only when the statement itself does not compile under the target (a renamed/removed Mathlib symbol in its type, or a name that now collides with a new Mathlib decl). Then make the minimal meaning-preserving change (usually a rename keeping statement + proof). Everything else: change only proof bodies / tactics / syntax.
def→theorem keyword changes for Prop-valued decls flagged by the defProp linter are allowed (same statement).
- Keep RAM under 24 GB the whole time.
- Work in a new git worktree (e.g.
~/Github/lean-pool-v<ver>), not the main checkout.
- Open a non-draft PR once finished. Aim for all CI gates green before declaring done.
- Never add
sorry/admit/native_decide/new axiom/unsafe/partial/maxHeartbeats increases/set_option linter.* false/nolint waivers. Fix the code, not the check. Never edit .github/workflows, quality.py, lint configs, or lakefile.toml's [leanOptions].
Recipe (learned from the v4.32.0-rc1 bump — see memory v432-bump-recipe.md)
0. Setup
- Confirm the tags exist upstream:
git ls-remote --tags for leanprover-community/mathlib4, leanprover/lean4, leanprover/doc-gen4.
git worktree add -b <branch> <dir> main.- Bump
lean-toolchain, lakefile.toml (mathlib rev), docbuild/lean-toolchain, docbuild/lakefile.toml (doc-gen4 rev).
lake update mathlib then lake exe cache get; later cd docbuild && lake update doc-gen4 (verify its manifest's mathlib rev matches the main one).
1. RAM control — CRITICAL, get this right first
- Lake 5.0 ignores
LAKE_JOBS and -j. The only working lever is export LEAN_NUM_THREADS=2 in ~/.zshenv (so agent shells inherit it) — caps lake to ~3 concurrent compiles. Remove this line at the end.
- The real RAM hog is the lean-lsp MCP: each query spawns a ~3 GB
lean --worker; under parallel agents these pile up to 30+ GB. Disable it with a persistent pkill -9 -f 'lean-lsp-mcp' loop (1 s) so its calls fast-fail and agents fall back to CLI. Do NOT reap only lean --worker — that makes an agent's in-flight MCP call hang and stalls the whole run.
- Run a watchdog Monitor on total Lean RSS; if it nears the cap, kill
v<ver> processes and lower concurrency.
2. Discover breakage
lake build LeanPool (capped). Bucket errors per project and per root cause.
3. Fix errors — parallel agent Workflow (opt-in)
- Use the Workflow tool: one agent per failing project, a custom
poolMap(items, k, …) for concurrency 2–3 (the default 10 is too much RAM), effort:'high', CLI-only (tell agents lean-lsp is disabled; use lake build LeanPool.<P>, lake env lean <file>, rg over .lake/packages/mathlib).
- Bake the hard constraints into every agent prompt. Have each return a structured summary (statementsModified, introducedForbidden).
- Recurring v4.32-era API deltas (re-derive for the new version):
coe_injective'→coe_injective (SetLike/DFunLike field), return→pure in metaprogram do-blocks, Set.diff_*→Set.sdiff_* family, Symmetric→local IsSymmetric (Mathlib's Symmetric deprecated for Std.Symm), @[expose] public collisions, defProp def→theorem.
- Transient API "rate limited" / "session limit" failures kill whole rounds — just re-run the not-green subset. Commit after each clean milestone (an agent can leave the tree broken; commit = cheap recovery).
4. Verify + guards
- Whole-pool
lake build LeanPool → 0 errors.
- Drop-guard: for each changed file, diff declaration names (
git show main:<f> vs current) — any name present on main but missing now must be an intended forced rename, not a drop.
- Forbidden scan:
git diff main added lines must contain no sorry/admit/native_decide/maxHeartbeats/linter-disable.
5. Warnings — CI fails on ANY warning: line
- Collect warnings from the build; run a second per-project Workflow to clear them (deprecation renames per the warning's "Use X instead", unused-simp-arg removal, no-op/never-executed tactic removal,
defProp def→theorem, import narrowing). Rebuild to 0 warnings.
6. CI gates
lake exe mk_all --check, lake exe runLinter LeanPool, lake exe lint-style LeanPool, and cd python && uv run python -m lean_pool.quality --repo ...
- Watch the defProp × proof-size catch-22:
def→theorem can push a Prop's large proof over quality.py's 200-line gate, and quality.py only delimits proofs at theorem/lemma (it lumps a following run of defs into the preceding theorem's count). Fix by extracting the proof's match/case sub-blocks into new private lemmas placed before the theorem, AND reordering any independent def block out of the measured region (before the first theorem). Proofs only — no signature changes.
7. PR
- The
content-pr-guard exempts bump metadata: a PR may carry content (LeanPool/**/*.lean) alongside ONLY lean-toolchain, lakefile.toml, lake-manifest.json, docbuild/{lean-toolchain,lakefile.toml,lake-manifest.json}. Anything else non-content alongside content fails the guard.
- Commit, push,
gh pr create --base main non-draft. PR body: list every statement-level change (collision renames, def→theorem) with reasons, and the verification (build 0/0, all gates pass).
- Confirm all PR checks pass on the head commit SHA (
gh pr checks, and verify the runs' head_sha == HEAD) before reporting done. Don't trust a stale CI run from an earlier failing commit.
8. Cleanup
- Remove the
LEAN_NUM_THREADS=2 line from ~/.zshenv; stop the lean-lsp reaper and watchdog monitors.
- Worktrees / disk. Each worktree carries its own ~5 GB
.lake, so reclaiming disk matters — but do it carefully. This machine runs multiple concurrent Claude sessions, and an old-campaign-named worktree (e.g. lean-pool-w2-*, compress*/…) may still be actively in use by another session. Remove ONLY: (a) the worktrees this bump created, and (b) verifiably-stale ones — where NO running process has the dir as cwd (check with lsof -a -d cwd) AND nothing was modified recently (find <wt> -newermt '-1 day' -not -path '*/.lake/*'). Use plain git worktree remove — its refusal on a dirty/active tree is the safety, so respect it. NEVER use git worktree remove --force, and never a blind loop/sweep over all worktrees. When unsure, list the candidates and ask the user. Removing a worktree keeps its branch (committed work is safe) but destroys any uncommitted changes — and yanks the cwd out from under any live process there.
