version-bump

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)

1. No statement drops. Every theorem/lemma/def/instance/structure/inductive/class/abbrev that exists now must still exist when done.
2. 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).
3. Keep RAM under 24 GB the whole time.
4. Work in a new git worktree (e.g. ~/Github/lean-pool-v<ver>), not the main checkout.
5. Open a non-draft PR once finished. Aim for all CI gates green before declaring done.
6. 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.