diff --git a/.github/BUMP_AUTOMATION.md b/.github/BUMP_AUTOMATION.md
index 7dc10dfe30..9d852c8626 100644
--- a/.github/BUMP_AUTOMATION.md
+++ b/.github/BUMP_AUTOMATION.md
@@ -1,182 +1,13 @@
 # Automated Mathlib bumps
 
-[`mathlib-bump.yml`](workflows/mathlib-bump.yml) migrates the whole pool to a
-new Lean/Mathlib release. It runs nightly and needs a human only at the end, to
-review the draft PR it opens.
+Version bumps run nightly on the Lean VM through the privately operated
+`lean-pool-automation` repository. That repository owns the controller, tests,
+repair prompts, account selection and deployment configuration.
 
-## What runs, and what it costs
+The controller preserves a full-history bump checkout, uses Codex subscription
+accounts through `cx`, validates the existing build and quality gates, and opens
+a draft content PR for review. Execution logs, credentials and operator
+instructions are maintained privately with the automation.
 
-| Stage | What it does | Cost |
-|---|---|---|
-| `detect` | Compares the pinned release against Mathlib's tags | free |
-| `auth` | One-minute check that the Claude token still works | negligible |
-| `pin` | Moves the four pins, refreshes manifests, pushes `bump/<version>` | free |
-| `probe` | Builds every project across 10 parallel shards | free |
-| `triage` | Buckets the shard logs into a per-project breakage map | free |
-| `repair` | One Claude job per broken project, in parallel (Opus 5) | subscription quota |
-| `assemble` | Applies patches, rebuilds the pool, runs all four gates, opens a draft PR | free |
-
-"Free" means GitHub-hosted runner minutes, which are unmetered for public
-repositories. Only `repair` spends anything, and only when something broke.
-
-The `probe` stage is worth having on its own: it runs whether or not a repair
-follows, so the morning after a release you already know whether the bump costs
-three projects or thirty.
-
-### Repair modes
-
-Bumps target the **newest available release, release candidates included** —
-mid-cycle that is what "latest Lean and Mathlib" means. `stable_only: true`
-narrows detection to final releases.
-
-The `repair` input controls the fan-out:
-
-- `always` (default) — repair every broken project.
-- `never` — probe only. Use this to size a bump without spending anything; the
-  per-project breakage report is produced either way.
-
-`auth` gates only `repair`, and runs in parallel with `pin`/`probe`, so an
-expired token still leaves you with the free breakage report. It exercises the
-same model the fan-out uses, so it cannot pass while that model is unavailable.
-
-Repairs run on **Opus 5**, pinned explicitly rather than left to the action's
-default. A bump repair is the hardest work in this repository -- Mathlib API
-archaeology plus proof surgery under a no-statement-drops constraint -- and a
-weaker model spends the same runner hours to produce patches that do not
-apply.
-
-## One-time setup
-
-### 1. Claude subscription token
-
-`repair` authenticates with a Claude subscription rather than API credits:
-
-```bash
-claude setup-token
-```
-
-Store the result as a repository secret named `CLAUDE_CODE_OAUTH_TOKEN`
-(Settings → Secrets and variables → Actions). Usage bills against the
-subscription's quota, shared with terminal and web sessions.
-
-**These tokens expire.** When one does, `repair` fails with an authentication
-error while `detect` and `probe` keep succeeding — so the nightly canary looks
-healthy and only the repair half is dead. Two ways to handle it:
-
-- *Simplest:* re-run `claude setup-token` and update the secret when a repair
-  job fails to authenticate. The failure is loud and the fix takes a minute.
-- *Unattended:* store a fine-grained PAT with `secrets: write` on this
-  repository and have the action refresh the stored token automatically. This
-  trades a long-lived PAT for never having to think about expiry.
-
-### 2. `BUMP_TOKEN` (optional) — CI on the bump PR
-
-A pull request opened by a bot has its workflow runs held in `action_required`
-until someone approves them. The run exists and is attached to the right
-commit, but no checks are created, so the PR shows **no checks at all** — worse
-than a red one, because it reads as unverified rather than broken.
-
-`assemble` handles this itself: it finds its own gated run and approves it, so
-the draft PR arrives with CI already going. That only ever approves a run on a
-`bump/*` branch this workflow created, and does not relax the approval gate for
-contributor pull requests.
-
-Setting `BUMP_TOKEN` to a PAT with `repo` scope (or a GitHub App installation
-token) avoids the gate entirely, since the PR is then authored by a real
-account. It is optional; without it the approval step covers the same ground.
-
-`assemble` also re-runs the whole-pool build and all four gates itself and puts
-the results in the PR body, so the information exists either way — but a
-reviewer should be able to see it on the PR.
-
-### 3. Pushing to branches (and to fork PRs)
-
-This workflow only ever pushes to `bump/*` branches in this repository, which
-the default `GITHUB_TOKEN` can do.
-
-Any automation that needs to push to a **contributor's fork branch** — the
-auto-rebase job for import PRs, for instance — cannot use `GITHUB_TOKEN`: it has
-no write access to forks even when the PR has *Allow edits by maintainers*
-checked. The fix is to authenticate as an app or a user instead:
-
-```yaml
-- uses: actions/create-github-app-token@<sha>
-  id: app-token
-  with:
-    app-id: ${{ secrets.APP_ID }}
-    private-key: ${{ secrets.APP_PRIVATE_KEY }}
-- uses: actions/checkout@<sha>
-  with:
-    token: ${{ steps.app-token.outputs.token }}
-```
-
-A GitHub App is preferable to a personal access token: its permissions are
-scoped to this repository, it can be revoked without touching your account, and
-its pushes re-trigger `pull_request` CI, which `GITHUB_TOKEN` pushes do not.
-
-## Triggering a bump by hand
-
-Actions → Mathlib Bump → Run workflow. Leave `version` blank to bump to the
-newest release, or name one explicitly:
-
-```bash
-gh workflow run mathlib-bump.yml -f version=v4.33.0-rc1 -f repair=always
-```
-
-To size a bump without spending anything:
-
-```bash
-gh workflow run mathlib-bump.yml -f repair=never
-```
-
-The probe report (per-project errors and warnings) is attached to the run as the
-`bump-report` artifact and summarised on the run page.
-
-## What the automation will not do
-
-- **Merge.** The PR is opened as a draft and stays that way until you review it.
-- **Weaken a gate.** Repair agents are instructed never to add `sorry`,
-  `native_decide`, an axiom, or a linter waiver, and `assemble` re-runs
-  `quality.py`, which fails on those regardless of what an agent was told.
-- **Drop a statement.** Agents are told that a lemma now absorbed by Mathlib is
-  still not theirs to delete; they report it instead, and the reviewer decides.
-  This is deliberately not a hard gate — losing a declaration to Mathlib is a
-  legitimate outcome of a bump, so it needs a human judgement, not a check.
-
-## When a repair job fails
-
-Failures are isolated: `fail-fast` is off, so one project failing does not stop
-the others, and `assemble` still opens a PR with whatever succeeded. The PR body
-lists how many repairs applied and which patches would not apply.
-
-Repair agents run with **no turn limit and no job timeout**. A repair is
-finished when the project builds, not after some number of turns or minutes,
-and an agent cut off mid-edit leaves behind a half-applied change that is worse
-than either outcome.
-
-One ceiling remains and cannot be removed here: GitHub-hosted runners kill any
-job at **six hours**. That is the longest a single project's repair can run.
-Raising it would mean moving the repair jobs to a self-hosted runner, where the
-limit is five days — worth doing only if projects ever start hitting six hours,
-which is far from the observed maximum of 20 minutes.
-
-Whatever an agent has done is exported as a patch even when its job fails, so
-partial progress on a hard project is never thrown away. The whole-pool build
-in `assemble` remains what decides whether the result is actually correct.
-
-**Runs accumulate.** `pin` resumes an existing `bump/<version>` branch rather
-than recreating it from main, so each run starts from every repair earlier runs
-landed. The probe then only finds the projects that are *still* broken, and the
-repair fan-out shrinks each round — that is what lets a large bump converge
-instead of re-repairing the same projects forever. If main has moved
-underneath, the branch merges it, resolving the generated index and the
-registry with the same mechanical resolver `auto-rebase.yml` uses.
-
-Re-running a bump is therefore the normal way to finish one. Dispatch it again
-and it picks up where the last run stopped.
-
-Measured on the first real run (v4.32.0-rc1 → v4.33.0-rc1, 99 projects broken,
-with a 60-turn cap still in place): 40 repaired cleanly, 59 hit the cap. Those
-59 had a *lower* median runtime (5 min) than the successes (9 min) — they were
-burning turns in tight edit/build/fail loops, so the cap was stopping them
-early rather than after sustained work. That is what removing it addresses.
+GitHub-hosted runners no longer perform migrations. Normal required PR checks
+continue to run on the resulting content changes.
diff --git a/.github/workflows/claude-auth-check.yml b/.github/workflows/claude-auth-check.yml
deleted file mode 100644
index 9ca47d5a1b..0000000000
--- a/.github/workflows/claude-auth-check.yml
+++ /dev/null
@@ -1,53 +0,0 @@
-name: Claude auth check
-
-# Verifies that CLAUDE_CODE_OAUTH_TOKEN still works, in about a minute.
-#
-# The token generated by `claude setup-token` expires. When it does, the only
-# thing that breaks is the repair fan-out in mathlib-bump.yml -- `detect`,
-# `pin`, `probe` and `triage` all keep passing, so the nightly bump looks
-# healthy while its expensive half is silently dead. This canary makes that
-# failure loud and cheap to diagnose: without it, the same answer costs a full
-# probe build (~40 minutes) before the first repair job even starts.
-#
-# `show_full_output` is safe here and nowhere else in this repository: the
-# prompt is trivial, no tools are allowed, and the job touches no secrets
-# beyond the token itself, which the action masks. Never set it on a job that
-# runs Bash -- these logs are public.
-
-on:
-  schedule:
-    # Weekly, off-peak and off the hour.
-    - cron: '41 6 * * 1'
-  workflow_dispatch:
-
-permissions:
-  contents: read
-  # The action exchanges an OIDC token unless `github_token` is supplied.
-  id-token: write
-
-jobs:
-  check:
-    runs-on: ubuntu-latest
-    name: Verify the Claude subscription token
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          persist-credentials: false
-
-      - name: Ping Claude
-        uses: anthropics/claude-code-action@be7b93b1907a4abad570368f3c74b6fe3807510b
-        with:
-          claude_code_oauth_token: ${{ secrets.CLAUDE_CODE_OAUTH_TOKEN }}
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-          show_full_output: true
-          prompt: "Reply with exactly: AUTH_OK"
-          claude_args: >-
-            --max-turns 1
-            --model claude-opus-5
-
-      - name: Report
-        if: always()
-        run: |
-          echo "If the step above failed, regenerate the token with" \
-            "\`claude setup-token\` and update the" \
-            "CLAUDE_CODE_OAUTH_TOKEN repository secret." >> "$GITHUB_STEP_SUMMARY"
diff --git a/.github/workflows/mathlib-bump.yml b/.github/workflows/mathlib-bump.yml
deleted file mode 100644
index 4357342fb2..0000000000
--- a/.github/workflows/mathlib-bump.yml
+++ /dev/null
@@ -1,692 +0,0 @@
-name: Mathlib Bump
-
-# Automated whole-pool migration to a new Lean/Mathlib release, in stages where
-# only the last one needs a human:
-#
-#   detect    Is there a newer release than the pinned one? (free, no LLM)
-#   pin       Move the four version pins, refresh the manifests, push a
-#             bump/<version> branch, and plan the build shards. (free)
-#   probe     Build every project across parallel shards, one project at a
-#             time so each diagnostic is attributable. (free)
-#   triage    Merge the shard logs into a per-project breakage map, which
-#             becomes the repair fan-out's job matrix. (free)
-#   repair    One Claude job per broken project, in parallel. Pool projects
-#             never import each other, so a bump decomposes into independent
-#             per-project repairs. (subscription quota)
-#   assemble  Apply every patch, rebuild the WHOLE pool, run all four gates,
-#             open a DRAFT pull request. (free)
-#
-# Agents propose, deterministic gates dispose: nothing here can merge itself,
-# and `assemble` re-runs the same checks CI would. Repair jobs upload patches
-# as artifacts rather than pushing, so parallel jobs cannot race the branch.
-#
-# Auth: `CLAUDE_CODE_OAUTH_TOKEN` is a Claude subscription token generated
-# locally with `claude setup-token`; usage bills against the subscription
-# rather than API credits. See .github/BUMP_AUTOMATION.md for setup and costs.
-
-on:
-  schedule:
-    # Off-peak, and off the :00 mark where every scheduled workflow piles up.
-    - cron: '23 5 * * *'
-  workflow_dispatch:
-    inputs:
-      version:
-        description: "Target release (e.g. v4.33.0-rc1); blank = auto-detect"
-        required: false
-        type: string
-      stable_only:
-        description: "Ignore -rc tags (default: bump to the newest release of any kind)"
-        required: false
-        default: false
-        type: boolean
-      repair:
-        description: "Run the Claude repair fan-out"
-        required: false
-        default: 'always'
-        type: choice
-        options: ['always', 'never']
-
-concurrency:
-  # One bump at a time: two concurrent bumps would fight over the branch.
-  group: mathlib-bump
-  cancel-in-progress: false
-
-permissions:
-  contents: read
-
-jobs:
-  detect:
-    runs-on: ubuntu-latest
-    name: Detect new release
-    outputs:
-      found: ${{ steps.detect.outputs.found }}
-      target: ${{ steps.detect.outputs.target }}
-      branch: ${{ steps.detect.outputs.branch }}
-      repair: ${{ steps.detect.outputs.repair }}
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          persist-credentials: false
-
-      - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
-      - name: Install Python tooling
-        run: cd python && uv sync --locked
-
-      - name: Resolve target version
-        id: detect
-        env:
-          REQUESTED: ${{ inputs.version }}
-          STABLE_ONLY: ${{ inputs.stable_only }}
-          REPAIR_MODE: ${{ inputs.repair || 'always' }}
-        run: |
-          set -euo pipefail
-          if [ -n "$REQUESTED" ]; then
-            target="$REQUESTED"
-            found=true
-          else
-            flags=""
-            if [ "$STABLE_ONLY" = "true" ]; then
-              flags="--stable-only"
-            fi
-            # Release candidates count: the pool tracks the newest Lean and
-            # Mathlib, which mid-cycle means the latest rc.
-            # shellcheck disable=SC2086
-            result="$(cd python && uv run python -m lean_pool.bump detect --repo .. $flags)"
-            echo "$result"
-            target="$(echo "$result" | python3 -c 'import json,sys; print(json.load(sys.stdin)["target"])')"
-            found="$(echo "$result" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["found"]).lower())')"
-          fi
-
-          repair=true
-          if [ "$REPAIR_MODE" = "never" ]; then
-            repair=false
-          fi
-
-          {
-            echo "found=$found"
-            echo "target=$target"
-            echo "branch=bump/$target"
-            echo "repair=$repair"
-          } >> "$GITHUB_OUTPUT"
-
-      - name: Summary
-        env:
-          FOUND: ${{ steps.detect.outputs.found }}
-          TARGET: ${{ steps.detect.outputs.target }}
-          REPAIR: ${{ steps.detect.outputs.repair }}
-        run: |
-          if [ "$FOUND" != "true" ]; then
-            echo "Pool is up to date; nothing to bump." >> "$GITHUB_STEP_SUMMARY"
-          else
-            echo "Target: **$TARGET** (repair fan-out: $REPAIR)" >> "$GITHUB_STEP_SUMMARY"
-          fi
-
-  auth:
-    needs: detect
-    # Only gates the paid stage; the free probe runs regardless of the token.
-    if: needs.detect.outputs.found == 'true' && needs.detect.outputs.repair == 'true'
-    runs-on: ubuntu-latest
-    name: Preflight Claude auth
-    permissions:
-      contents: read
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          persist-credentials: false
-
-      # A trivial round-trip. Without it an invalid or expired token is only
-      # discovered after the ~40-minute probe, by 99 repair jobs failing
-      # identically -- which is exactly how the first three runs were spent.
-      - uses: anthropics/claude-code-action@be7b93b1907a4abad570368f3c74b6fe3807510b
-        with:
-          claude_code_oauth_token: ${{ secrets.CLAUDE_CODE_OAUTH_TOKEN }}
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-          prompt: "Reply with exactly: AUTH_OK"
-          claude_args: >-
-            --max-turns 1
-            --model claude-opus-5
-
-      - name: Explain a failure
-        if: failure()
-        run: |
-          echo "::error::CLAUDE_CODE_OAUTH_TOKEN is invalid or expired." \
-            "Regenerate it with \`claude setup-token\` and update the secret," \
-            "then verify with the Claude auth check workflow."
-
-  pin:
-    needs: detect
-    if: needs.detect.outputs.found == 'true'
-    runs-on: ubuntu-latest
-    name: Move pins and plan shards
-    permissions:
-      contents: write
-    outputs:
-      matrix: ${{ steps.plan.outputs.matrix }}
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          # GitHub suppresses workflow triggers for anything pushed with
-          # GITHUB_TOKEN, so a branch pushed with it yields a PR that never
-          # runs CI. BUMP_TOKEN (a PAT or GitHub App token) restores that;
-          # without it `assemble` dispatches Lean Action CI explicitly.
-          token: ${{ secrets.BUMP_TOKEN || secrets.GITHUB_TOKEN }}
-
-      - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
-      - name: Install Python tooling
-        run: cd python && uv sync --locked
-
-      - name: Resume the bump branch if one exists
-        env:
-          BRANCH: ${{ needs.detect.outputs.branch }}
-        run: |
-          set -euo pipefail
-          git config user.name "github-actions[bot]"
-          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-          if ! git ls-remote --exit-code --heads origin "$BRANCH" >/dev/null 2>&1; then
-            echo "No existing $BRANCH; starting from main."
-            git checkout -B "$BRANCH"
-            exit 0
-          fi
-          # Build on the repairs earlier runs already landed. Recreating the
-          # branch from main would discard them, so every run would re-repair
-          # the same projects from scratch and the bump could never converge.
-          echo "Resuming $BRANCH."
-          git fetch origin "$BRANCH"
-          git checkout -B "$BRANCH" "origin/$BRANCH"
-          if git merge --no-edit origin/main; then
-            exit 0
-          fi
-          # main moving under the branch conflicts only in the generated index
-          # and the registry, both of which resolve mechanically.
-          git diff --name-only --diff-filter=U > conflicts.txt
-          cat conflicts.txt
-          (cd python && uv run python -m lean_pool.rebase resolvable \
-            --conflicts ../conflicts.txt)
-          merge_base="$(git merge-base "origin/$BRANCH" origin/main)"
-          if grep -qx 'LeanPool/projects.yml' conflicts.txt; then
-            git show "$merge_base:LeanPool/projects.yml" > /tmp/base.yml
-            git show origin/main:LeanPool/projects.yml > /tmp/ours.yml
-            git show "origin/$BRANCH:LeanPool/projects.yml" > /tmp/theirs.yml
-            (cd python && uv run python -m lean_pool.rebase registry --repo .. \
-              --base /tmp/base.yml --ours /tmp/ours.yml --theirs /tmp/theirs.yml)
-            git add LeanPool/projects.yml
-          fi
-          if grep -qx 'LeanPool.lean' conflicts.txt; then
-            (cd python && uv run python -m lean_pool.rebase index --repo ..)
-            git add LeanPool.lean
-          fi
-          git commit --no-edit
-
-      - name: Move the version pins
-        env:
-          TARGET: ${{ needs.detect.outputs.target }}
-        run: cd python && uv run python -m lean_pool.bump pin --repo .. --version "$TARGET"
-
-      - name: Install Lean toolchain
-        run: |
-          set -euo pipefail
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-            -o elan-init.sh
-          sh elan-init.sh -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-
-      - name: Refresh dependency manifests
-        run: |
-          set -euo pipefail
-          lake update mathlib
-          (cd docbuild && lake update doc-gen4)
-
-      - name: Push the bump branch
-        env:
-          BRANCH: ${{ needs.detect.outputs.branch }}
-          TARGET: ${{ needs.detect.outputs.target }}
-        run: |
-          set -euo pipefail
-          # Already on $BRANCH, resumed or freshly created above.
-          git add lean-toolchain lakefile.toml lake-manifest.json \
-            docbuild/lean-toolchain docbuild/lakefile.toml docbuild/lake-manifest.json
-          # A re-run against an already-pinned version has nothing to commit.
-          if git diff --cached --quiet; then
-            echo "Pins already at $TARGET."
-          else
-            git commit -m "chore: pin Lean and Mathlib to $TARGET"
-          fi
-          # --force-with-lease, never --force: the branch carries accumulated
-          # repairs, and a blind force would discard anything landed since this
-          # job checked it out.
-          git push --force-with-lease origin "$BRANCH"
-
-      - name: Plan the build shards
-        id: plan
-        env:
-          FORCE_FULL: 'true'
-        run: |
-          set -euo pipefail
-          plan="$(python3 scripts/ci/plan-build-shards.py)"
-          echo "$plan"
-          matrix="$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')"
-          echo "matrix=$matrix" >> "$GITHUB_OUTPUT"
-
-  probe:
-    needs: [detect, pin]
-    runs-on: ubuntu-latest
-    name: Probe shard ${{ matrix.shard }}
-    strategy:
-      # A shard whose projects fail to build is the expected case, and one
-      # shard dying must never hide the breakage the others found.
-      fail-fast: false
-      matrix: ${{ fromJSON(needs.pin.outputs.matrix) }}
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          ref: ${{ needs.detect.outputs.branch }}
-          persist-credentials: false
-
-      - name: Install Lean toolchain
-        run: |
-          set -euo pipefail
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-            -o elan-init.sh
-          sh elan-init.sh -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-
-      - name: Fetch Mathlib build cache
-        run: lake exe cache get
-
-      - name: Build this shard's projects
-        env:
-          PROJECTS: ${{ matrix.projects }}
-          SHARD: ${{ matrix.shard }}
-          # Lake 5.0 ignores LAKE_JOBS and -j; this is the only working lever,
-          # and a 16 GB runner needs it (~3.5 GB per concurrent elaboration).
-          LEAN_NUM_THREADS: 2
-        run: |
-          set -uo pipefail
-          # One project at a time, so a failure never masks the rest and each
-          # diagnostic is attributable to the project that produced it.
-          for project in $PROJECTS; do
-            echo "::group::LeanPool.$project"
-            lake build "LeanPool.$project" 2>&1 | tee -a "shard-$SHARD.log" || true
-            echo "::endgroup::"
-          done
-
-      - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        with:
-          name: probe-log-${{ matrix.shard }}
-          path: shard-${{ matrix.shard }}.log
-          if-no-files-found: ignore
-
-  triage:
-    needs: [detect, probe]
-    if: always() && needs.probe.result != 'skipped'
-    runs-on: ubuntu-latest
-    name: Triage breakage
-    outputs:
-      broken: ${{ steps.report.outputs.broken }}
-      has_breakage: ${{ steps.report.outputs.has_breakage }}
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          persist-credentials: false
-
-      - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
-      - name: Install Python tooling
-        run: cd python && uv sync --locked
-
-      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
-        with:
-          pattern: probe-log-*
-          path: logs
-          merge-multiple: true
-
-      - name: Triage the build logs
-        id: report
-        run: |
-          set -euo pipefail
-          cat logs/*.log > build.log 2>/dev/null || : > build.log
-          (cd python && uv run python -m lean_pool.bump report \
-            --log ../build.log --output ../bump-report.json > /dev/null)
-          broken="$(python3 -c 'import json; print(json.dumps(json.load(open("bump-report.json"))["broken_projects"]))')"
-          echo "broken=$broken" >> "$GITHUB_OUTPUT"
-          if [ "$broken" = "[]" ]; then
-            echo "has_breakage=false" >> "$GITHUB_OUTPUT"
-          else
-            echo "has_breakage=true" >> "$GITHUB_OUTPUT"
-          fi
-          python3 scripts/ci/bump-summary.py bump-report.json >> "$GITHUB_STEP_SUMMARY"
-
-      - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        with:
-          name: bump-report
-          path: |
-            bump-report.json
-            build.log
-
-  repair:
-    needs: [detect, auth, triage]
-    if: needs.detect.outputs.repair == 'true' && needs.triage.outputs.has_breakage == 'true'
-    runs-on: ubuntu-latest
-    name: Repair ${{ matrix.project }}
-    # No turn limit and no explicit timeout: a repair is done when the project
-    # builds, and any cap only ever stops an agent mid-edit, leaving a
-    # half-applied change behind. GitHub-hosted runners still enforce their own
-    # six-hour ceiling, which is the longest a job can run here; raising that
-    # would require a self-hosted runner.
-    permissions:
-      contents: read
-      # claude-code-action exchanges a GitHub OIDC token for its credentials;
-      # without this it fails every attempt with "Unable to get
-      # ACTIONS_ID_TOKEN_REQUEST_URL".
-      id-token: write
-    strategy:
-      fail-fast: false
-      # The free plan allows 20 concurrent jobs across the account; leave
-      # headroom so a bump never starves ordinary PR CI.
-      max-parallel: 12
-      matrix:
-        project: ${{ fromJSON(needs.triage.outputs.broken) }}
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          ref: ${{ needs.detect.outputs.branch }}
-          persist-credentials: false
-
-      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
-        with:
-          name: bump-report
-
-      - name: Install Lean toolchain
-        run: |
-          set -euo pipefail
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-            -o elan-init.sh
-          sh elan-init.sh -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-
-      - name: Fetch Mathlib build cache
-        run: lake exe cache get
-
-      - name: Extract this project's diagnostics
-        env:
-          PROJECT: ${{ matrix.project }}
-        run: |
-          set -euo pipefail
-          python3 scripts/ci/bump-summary.py bump-report.json --project "$PROJECT" \
-            > diagnostics.txt
-          cat diagnostics.txt
-
-      - name: Repair with Claude
-        uses: anthropics/claude-code-action@be7b93b1907a4abad570368f3c74b6fe3807510b
-        with:
-          claude_code_oauth_token: ${{ secrets.CLAUDE_CODE_OAUTH_TOKEN }}
-          # Supplying a token short-circuits the action's OIDC-to-app-token
-          # exchange (OVERRIDE_GITHUB_TOKEN in its token.ts), which otherwise
-          # 401s with "Claude Code is not installed on this repository". These
-          # jobs only read the repo and write a patch artifact, so the default
-          # job token is sufficient and no GitHub App install is needed.
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-          prompt: "/version-bump-project ${{ matrix.project }} ${{ needs.detect.outputs.target }}"
-          claude_args: >-
-            --model claude-opus-5
-            --allowedTools "Bash,Read,Edit,Write,Grep,Glob"
-
-      - name: Verify the repair
-        id: verify
-        # Runs even when the Claude step failed. The common failure is
-        # `error_max_turns`, and an agent that ran out of turns has usually
-        # made real progress -- skipping these steps threw all of it away and
-        # made the project start from scratch on the next run.
-        if: always()
-        env:
-          PROJECT: ${{ matrix.project }}
-          LEAN_NUM_THREADS: 2
-        run: |
-          # `set +e`, not just `set -uo pipefail`: the runner's shell is
-          # `bash -e`, which would abort this step on a failing build before
-          # PIPESTATUS could be read. A project that still fails must be
-          # recorded, not silently lost.
-          set +e
-          set -uo pipefail
-          lake build "LeanPool.$PROJECT" 2>&1 | tee verify.log
-          status=${PIPESTATUS[0]}
-          if [ "$status" -ne 0 ]; then
-            echo "::warning::LeanPool.$PROJECT still fails to build"
-            echo "clean=false" >> "$GITHUB_OUTPUT"
-          elif grep -qE '(^|: )warning:' verify.log; then
-            echo "::warning::LeanPool.$PROJECT builds but emits warnings"
-            echo "clean=warnings" >> "$GITHUB_OUTPUT"
-          else
-            echo "clean=true" >> "$GITHUB_OUTPUT"
-          fi
-
-      - name: Export the repair as a patch
-        if: always()
-        env:
-          PROJECT: ${{ matrix.project }}
-          CLEAN: ${{ steps.verify.outputs.clean }}
-        run: |
-          set -euo pipefail
-          # Patches, not pushes: parallel jobs writing the same branch would
-          # race. `assemble` applies them in a defined order instead.
-          git add -- LeanPool
-          git diff --cached --binary > "repair-$PROJECT.patch"
-          changed="$(git diff --cached --name-only | wc -l | tr -d ' ')"
-          printf '{"project": "%s", "clean": "%s", "changed": %s}\n' \
-            "$PROJECT" "$CLEAN" "$changed" > "repair-$PROJECT.json"
-          cat "repair-$PROJECT.json"
-
-      - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        if: always()
-        with:
-          name: repair-${{ matrix.project }}
-          path: |
-            repair-${{ matrix.project }}.patch
-            repair-${{ matrix.project }}.json
-
-  assemble:
-    needs: [detect, pin, triage, repair]
-    # Runs even when some repairs failed: a partial bump PR with an honest
-    # summary beats no PR. Skipped only if triage never produced a report.
-    if: always() && needs.triage.result == 'success'
-    runs-on: ubuntu-latest
-    name: Assemble and open PR
-    permissions:
-      contents: write
-      pull-requests: write
-      # To release the PR's own CI run from the approval gate; see the last step.
-      actions: write
-    steps:
-      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
-        with:
-          ref: ${{ needs.detect.outputs.branch }}
-          fetch-depth: 0
-          token: ${{ secrets.BUMP_TOKEN || secrets.GITHUB_TOKEN }}
-
-      - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
-      - name: Install Python tooling
-        run: cd python && uv sync --locked
-
-      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
-        with:
-          path: artifacts
-          merge-multiple: true
-
-      - name: Apply repair patches
-        id: apply
-        env:
-          TARGET: ${{ needs.detect.outputs.target }}
-        run: |
-          set -euo pipefail
-          applied=0
-          skipped=""
-          for patch in artifacts/repair-*.patch; do
-            [ -s "$patch" ] || continue
-            if git apply --index "$patch"; then
-              applied=$((applied + 1))
-            else
-              skipped="$skipped $(basename "$patch" .patch)"
-            fi
-          done
-          {
-            echo "applied=$applied"
-            echo "skipped=$skipped"
-          } >> "$GITHUB_OUTPUT"
-          if [ "$applied" -gt 0 ]; then
-            git config user.name "github-actions[bot]"
-            git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-            git commit -m "Repair $applied project(s) for $TARGET"
-          fi
-
-      - name: Install Lean toolchain
-        run: |
-          set -euo pipefail
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-            -o elan-init.sh
-          sh elan-init.sh -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-
-      - name: Build the whole pool
-        id: build
-        env:
-          LEAN_NUM_THREADS: 2
-        run: |
-          # See the repair job's verify step: the runner's `bash -e` would
-          # abort here on a failing build, skipping the PR that reports it.
-          set +e
-          set -uo pipefail
-          lake exe cache get
-          # Whole-pool, not per-project: this is the pass that catches the
-          # cross-project effects per-project repair cannot see (a transitive
-          # instance changing simp behaviour in an unrelated project).
-          lake build LeanPool 2>&1 | tee assemble.log
-          status=${PIPESTATUS[0]}
-          errors=$(grep -cE '(^|: )error:' assemble.log || true)
-          warnings=$(grep -cE '(^|: )warning:' assemble.log || true)
-          {
-            echo "errors=$errors"
-            echo "warnings=$warnings"
-            echo "status=$status"
-          } >> "$GITHUB_OUTPUT"
-
-      - name: Run the quality gates
-        id: gates
-        if: steps.build.outputs.status == '0'
-        run: |
-          # Each gate's result is recorded rather than aborting the job, so the
-          # PR body can report which ones failed.
-          set +e
-          set -uo pipefail
-          results=""
-          lake exe mk_all --check      && results="$results mk_all:pass" || results="$results mk_all:FAIL"
-          lake exe runLinter LeanPool  && results="$results linter:pass" || results="$results linter:FAIL"
-          lake exe lint-style LeanPool && results="$results style:pass"  || results="$results style:FAIL"
-          (cd python && uv run python -m lean_pool.quality --repo ..) \
-            && results="$results quality:pass" || results="$results quality:FAIL"
-          echo "results=$results" >> "$GITHUB_OUTPUT"
-          echo "Gates:$results" >> "$GITHUB_STEP_SUMMARY"
-
-      - name: Push and open a draft PR
-        env:
-          GH_TOKEN: ${{ secrets.BUMP_TOKEN || secrets.GITHUB_TOKEN }}
-          BRANCH: ${{ needs.detect.outputs.branch }}
-          TARGET: ${{ needs.detect.outputs.target }}
-          APPLIED: ${{ steps.apply.outputs.applied }}
-          SKIPPED: ${{ steps.apply.outputs.skipped }}
-          ERRORS: ${{ steps.build.outputs.errors }}
-          WARNINGS: ${{ steps.build.outputs.warnings }}
-          GATES: ${{ steps.gates.outputs.results }}
-        run: |
-          set -euo pipefail
-          # The branch may have moved while the whole-pool build ran (a
-          # parallel session pushing to the same bump branch, or auto-rebase).
-          # A rejected push here threw away round 2's repairs after two hours
-          # of build. Rebase the repair commits onto the new tip and retry;
-          # repairs touch only LeanPool project files, so a clean rebase is
-          # the overwhelmingly common case. A genuine conflict still fails.
-          pushed=false
-          for _ in 1 2 3; do
-            if git push origin "$BRANCH"; then
-              pushed=true
-              break
-            fi
-            git fetch origin "$BRANCH"
-            git rebase "origin/$BRANCH" || { git rebase --abort; break; }
-          done
-          if [ "$pushed" != "true" ]; then
-            echo "::error::Could not push $BRANCH: it moved during assemble" \
-              "and the repairs do not rebase cleanly. Re-run the workflow."
-            exit 1
-          fi
-          {
-            echo "Automated migration of the pool to \`$TARGET\`."
-            echo
-            echo "| | |"
-            echo "|---|---|"
-            echo "| Repairs applied | $APPLIED |"
-            echo "| Whole-pool errors | $ERRORS |"
-            echo "| Whole-pool warnings | $WARNINGS |"
-            echo "| Gates | ${GATES:-not run (build failed)} |"
-            if [ -n "$SKIPPED" ]; then
-              echo "| Patches that would not apply |$SKIPPED |"
-            fi
-            echo
-            echo "Opened as a **draft**: review the statement-level changes before"
-            echo "marking ready. CI must be green on the head SHA, and a declaration"
-            echo "that disappeared should be one Mathlib absorbed, not one lost."
-            echo
-            echo "Generated by \`.github/workflows/mathlib-bump.yml\`."
-          } > body.md
-          if gh pr view "$BRANCH" --json number >/dev/null 2>&1; then
-            gh pr edit "$BRANCH" --body-file body.md
-          else
-            gh pr create --draft --base main --head "$BRANCH" \
-              --title "chore: bump Lean and Mathlib to $TARGET" \
-              --body-file body.md
-          fi
-
-      - name: Release the PR's CI run from the approval gate
-        env:
-          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          BRANCH: ${{ needs.detect.outputs.branch }}
-          REPO: ${{ github.repository }}
-        run: |
-          set -euo pipefail
-          # A PR opened by a bot has its workflow runs held in
-          # `action_required` until someone approves them, so the bump PR
-          # shows no checks at all -- worse than a red one, because it reads
-          # as unverified rather than broken. Approve the run here so the
-          # draft PR arrives with CI already going.
-          #
-          # This only ever approves a run on this workflow's own bump/* branch,
-          # whose contents are main plus patches this run produced. It does not
-          # relax the gate for contributor pull requests.
-          for _ in $(seq 1 10); do
-            run_id="$(gh run list --repo "$REPO" --workflow lean_action_ci.yml \
-              --branch "$BRANCH" --limit 1 --json databaseId,status \
-              --jq '.[] | select(.status == "action_required") | .databaseId')"
-            if [ -n "$run_id" ]; then
-              gh api -X POST "repos/$REPO/actions/runs/$run_id/approve"
-              echo "Approved Lean Action CI run $run_id on $BRANCH." \
-                >> "$GITHUB_STEP_SUMMARY"
-              exit 0
-            fi
-            sleep 10
-          done
-          # Nothing to approve is the normal case with BUMP_TOKEN set, since a
-          # PAT-authored PR is not gated. Fall back to an explicit dispatch so
-          # the branch is never left unverified.
-          gh workflow run lean_action_ci.yml --repo "$REPO" --ref "$BRANCH" || true
-          echo "No gated run found; dispatched Lean Action CI on $BRANCH." \
-            >> "$GITHUB_STEP_SUMMARY"
diff --git a/python/lean_pool/bump.py b/python/lean_pool/bump.py
deleted file mode 100644
index fc04531e80..0000000000
--- a/python/lean_pool/bump.py
+++ /dev/null
@@ -1,319 +0,0 @@
-"""Version-detection, pin-rewriting, and build-log triage for Mathlib bumps.
-
-Backs ``.github/workflows/mathlib-bump.yml``. The workflow keeps only
-orchestration; every decision that benefits from being testable lives here:
-
-* ``detect``  -- is there a newer Mathlib release than the one pinned?
-* ``pin``     -- rewrite the four version pins to a target release.
-* ``report``  -- turn a ``lake build`` log into a per-project breakage map,
-  which becomes the repair fan-out's job matrix.
-
-Pool projects never import each other, so a bump decomposes into one
-independent repair per broken project. ``report`` is what makes that
-decomposition explicit.
-
-Usage::
-
-    python -m lean_pool.bump detect --repo .. [--allow-prerelease]
-    python -m lean_pool.bump pin --repo .. --version v4.33.0-rc1
-    python -m lean_pool.bump report --repo .. --log build.log
-"""
-
-from __future__ import annotations
-
-import argparse
-import json
-import logging
-import re
-import subprocess
-import sys
-from dataclasses import dataclass, field
-from pathlib import Path
-
-logger = logging.getLogger(__name__)
-
-MATHLIB_REMOTE = "https://github.com/leanprover-community/mathlib4"
-
-# Release tags shared by Lean, Mathlib, and doc-gen4: v4.33.0, v4.33.0-rc1.
-VERSION_RE = re.compile(r"^v(\d+)\.(\d+)\.(\d+)(?:-rc(\d+))?$")
-# Diagnostics are `error: <path>:<line>:<col>: <message>`; lake may prefix the
-# path with `./`. Progress lines instead name the module: `Building LeanPool.X`.
-DIAGNOSTIC_RE = re.compile(r"^(?:.*?\s)?(error|warning):\s*(.*)$")
-PATH_PROJECT_RE = re.compile(r"LeanPool/(\w+)")
-MODULE_PROJECT_RE = re.compile(r"LeanPool\.(\w+)")
-BUILDING_RE = re.compile(r"Building\s+(LeanPool\.\S+)")
-
-# How many diagnostic lines to carry into the repair prompt per project.
-MAX_EXCERPT_LINES = 40
-
-
-def version_key(tag: str) -> tuple[int, int, int, int, int]:
-    """Sort key for a release tag; a final release outranks its candidates."""
-    match = VERSION_RE.match(tag)
-    if match is None:
-        raise ValueError(f"not a release tag: {tag}")
-    major, minor, patch, candidate = match.groups()
-    # `is_final` = 1 sorts v4.33.0 above v4.33.0-rc9.
-    is_final = 0 if candidate else 1
-    return (int(major), int(minor), int(patch), is_final, int(candidate or 0))
-
-
-def is_prerelease(tag: str) -> bool:
-    """Whether ``tag`` names a release candidate rather than a final release."""
-    match = VERSION_RE.match(tag)
-    return bool(match and match.group(4))
-
-
-def current_version(root: Path) -> str:
-    """Read the Mathlib release currently pinned in ``lakefile.toml``."""
-    text = (root / "lakefile.toml").read_text(encoding="utf-8")
-    # The manifest lists several packages; only Mathlib's rev is a release tag.
-    for match in re.finditer(r'rev\s*=\s*"([^"]+)"', text):
-        if VERSION_RE.match(match.group(1)):
-            return match.group(1)
-    raise SystemExit("no Mathlib release tag found in lakefile.toml")
-
-
-def remote_tags(remote: str = MATHLIB_REMOTE) -> list[str]:
-    """List release tags published by the Mathlib repository."""
-    result = subprocess.run(
-        ["git", "ls-remote", "--tags", "--refs", remote],
-        capture_output=True,
-        text=True,
-        check=True,
-    )
-    tags = []
-    for line in result.stdout.splitlines():
-        _, _, ref = line.partition("refs/tags/")
-        if ref and VERSION_RE.match(ref.strip()):
-            tags.append(ref.strip())
-    return tags
-
-
-def newer_versions(
-    current: str, tags: list[str], *, stable_only: bool = False
-) -> list[str]:
-    """Return tags strictly newer than ``current``, oldest first.
-
-    Release candidates count by default: the pool tracks the newest Lean and
-    Mathlib available, and an rc is what "newest" usually means during a
-    release cycle. ``stable_only`` narrows this to final releases.
-    """
-    threshold = version_key(current)
-    candidates = [
-        tag
-        for tag in tags
-        if version_key(tag) > threshold and not (stable_only and is_prerelease(tag))
-    ]
-    return sorted(set(candidates), key=version_key)
-
-
-def pin_files(root: Path, version: str) -> list[Path]:
-    """Rewrite the toolchain and dependency pins to ``version``.
-
-    Returns the files that changed. ``lake update`` still has to regenerate
-    the manifests afterwards; this only moves the declared pins.
-    """
-    if not VERSION_RE.match(version):
-        raise SystemExit(f"not a release tag: {version}")
-    changed: list[Path] = []
-    edits: list[tuple[Path, re.Pattern[str], str]] = [
-        (
-            root / "lean-toolchain",
-            re.compile(r"^leanprover/lean4:.*$", re.M),
-            f"leanprover/lean4:{version}",
-        ),
-        (
-            root / "docbuild" / "lean-toolchain",
-            re.compile(r"^leanprover/lean4:.*$", re.M),
-            f"leanprover/lean4:{version}",
-        ),
-        # Only the release-tag rev is rewritten; branch pins (main, master)
-        # in the same file are left alone.
-        (
-            root / "lakefile.toml",
-            re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"'),
-            f'rev = "{version}"',
-        ),
-        (
-            root / "docbuild" / "lakefile.toml",
-            re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"'),
-            f'rev = "{version}"',
-        ),
-    ]
-    for path, pattern, replacement in edits:
-        if not path.is_file():
-            raise SystemExit(f"missing pin file: {path}")
-        before = path.read_text(encoding="utf-8")
-        after = pattern.sub(replacement, before)
-        if after != before:
-            path.write_text(after, encoding="utf-8")
-            changed.append(path)
-    return changed
-
-
-@dataclass
-class ProjectDiagnostics:
-    """Errors and warnings attributed to a single pool project."""
-
-    project: str
-    errors: list[str] = field(default_factory=list)
-    warnings: list[str] = field(default_factory=list)
-
-    def as_dict(self) -> dict[str, object]:
-        """Serialise for the workflow's job matrix and report artifact."""
-        return {
-            "project": self.project,
-            "errors": self.errors[:MAX_EXCERPT_LINES],
-            "warnings": self.warnings[:MAX_EXCERPT_LINES],
-            "error_count": len(self.errors),
-            "warning_count": len(self.warnings),
-        }
-
-
-def _attribute(text: str, fallback: str | None) -> str | None:
-    """Find which project a diagnostic line belongs to."""
-    match = PATH_PROJECT_RE.search(text) or MODULE_PROJECT_RE.search(text)
-    return match.group(1) if match else fallback
-
-
-def parse_build_log(log: str) -> dict[str, ProjectDiagnostics]:
-    """Bucket a ``lake build`` log's diagnostics by pool project.
-
-    Diagnostics name their file, so most lines attribute themselves. A
-    message that does not (a bare continuation line, or an error lake prints
-    against a module rather than a file) is attributed to the module of the
-    most recent ``Building`` line.
-    """
-    buckets: dict[str, ProjectDiagnostics] = {}
-    current: str | None = None
-    active: tuple[str, str] | None = None  # (project, severity) for continuations
-
-    for line in log.splitlines():
-        building = BUILDING_RE.search(line)
-        if building:
-            module = MODULE_PROJECT_RE.search(building.group(1))
-            current = module.group(1) if module else None
-
-        diagnostic = DIAGNOSTIC_RE.match(line)
-        if diagnostic:
-            severity, message = diagnostic.groups()
-            project = _attribute(message, current)
-            if project is None:
-                active = None
-                continue
-            bucket = buckets.setdefault(project, ProjectDiagnostics(project))
-            target = bucket.errors if severity == "error" else bucket.warnings
-            target.append(line.rstrip())
-            active = (project, severity)
-            continue
-
-        # Indented continuation of the previous diagnostic (goal state, etc.).
-        if active and line.startswith(" ") and line.strip():
-            project, severity = active
-            bucket = buckets[project]
-            target = bucket.errors if severity == "error" else bucket.warnings
-            if len(target) < MAX_EXCERPT_LINES:
-                target.append(line.rstrip())
-        elif not line.strip():
-            active = None
-
-    return buckets
-
-
-def build_report(log: str) -> dict[str, object]:
-    """Summarise a build log into the report the workflow consumes."""
-    buckets = parse_build_log(log)
-    broken = sorted((b for b in buckets.values() if b.errors), key=lambda b: b.project)
-    warned = sorted(
-        (b for b in buckets.values() if b.warnings and not b.errors),
-        key=lambda b: b.project,
-    )
-    return {
-        "broken": [b.as_dict() for b in broken],
-        "warned": [b.as_dict() for b in warned],
-        "broken_projects": [b.project for b in broken],
-        "warned_projects": [b.project for b in warned],
-        "clean": not broken and not warned,
-    }
-
-
-def _command_detect(args: argparse.Namespace) -> int:
-    """Print the newest Mathlib release to bump to, if any."""
-    root = args.repo.resolve()
-    current = current_version(root)
-    tags = remote_tags(args.remote)
-    newer = newer_versions(current, tags, stable_only=args.stable_only)
-    # The newest available release, candidates included: the pool tracks the
-    # latest Lean and Mathlib, not the latest final release.
-    target = newer[-1] if newer else ""
-    payload = {
-        "current": current,
-        "target": target,
-        "available": newer,
-        "found": bool(target),
-    }
-    print(json.dumps(payload))
-    return 0
-
-
-def _command_pin(args: argparse.Namespace) -> int:
-    """Rewrite the version pins and report which files moved."""
-    changed = pin_files(args.repo.resolve(), args.version)
-    for path in changed:
-        logger.info("pinned %s", path)
-    if not changed:
-        logger.info("pins already at %s", args.version)
-    return 0
-
-
-def _command_report(args: argparse.Namespace) -> int:
-    """Turn a build log into the per-project breakage report."""
-    log = args.log.read_text(encoding="utf-8", errors="replace")
-    report = build_report(log)
-    output = json.dumps(report, indent=2)
-    if args.output:
-        args.output.write_text(output + "\n", encoding="utf-8")
-    print(output)
-    return 0
-
-
-def _parse_args(argv: list[str] | None) -> argparse.Namespace:
-    """Parse command-line arguments."""
-    parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    subparsers = parser.add_subparsers(dest="command", required=True)
-
-    # `--repo` sits on each subcommand rather than the parent so it can be
-    # passed after the subcommand, which is how it reads in a workflow step.
-    detect = subparsers.add_parser("detect", help="find a newer Mathlib release")
-    detect.add_argument("--repo", type=Path, default=Path("."), help="repository root")
-    detect.add_argument("--remote", default=MATHLIB_REMOTE)
-    detect.add_argument(
-        "--stable-only",
-        action="store_true",
-        help="ignore -rc tags (default: bump to the newest release of any kind)",
-    )
-    detect.set_defaults(func=_command_detect)
-
-    pin = subparsers.add_parser("pin", help="rewrite the version pins")
-    pin.add_argument("--repo", type=Path, default=Path("."), help="repository root")
-    pin.add_argument("--version", required=True)
-    pin.set_defaults(func=_command_pin)
-
-    report = subparsers.add_parser("report", help="triage a build log by project")
-    report.add_argument("--log", type=Path, required=True)
-    report.add_argument("--output", type=Path)
-    report.set_defaults(func=_command_report)
-
-    return parser.parse_args(argv)
-
-
-def main(argv: list[str] | None = None) -> int:
-    """Dispatch a subcommand; return a process exit code."""
-    logging.basicConfig(level=logging.INFO, format="%(message)s")
-    args = _parse_args(argv)
-    return int(args.func(args))
-
-
-if __name__ == "__main__":
-    sys.exit(main())
diff --git a/python/tests/test_bump.py b/python/tests/test_bump.py
deleted file mode 100644
index 82e627bc29..0000000000
--- a/python/tests/test_bump.py
+++ /dev/null
@@ -1,239 +0,0 @@
-"""Tests for Mathlib bump detection, pin rewriting, and build-log triage."""
-
-from __future__ import annotations
-
-from pathlib import Path
-
-import pytest
-
-from lean_pool.bump import (
-    build_report,
-    current_version,
-    is_prerelease,
-    main,
-    newer_versions,
-    parse_build_log,
-    pin_files,
-    version_key,
-)
-
-LAKEFILE = """name = "lean-pool"
-
-[leanOptions]
-relaxedAutoImplicit = false
-
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-rev = "v4.32.0-rc1"
-
-[[lean_lib]]
-name = "LeanPool"
-"""
-
-DOCBUILD_LAKEFILE = """name = "docbuild"
-
-[[require]]
-name = "lean-pool"
-path = "../"
-
-[[require]]
-scope = "leanprover"
-name = "doc-gen4"
-rev = "v4.32.0-rc1"
-"""
-
-
-def _write_repo(root: Path) -> None:
-    """Create a repository with the four version pins a bump rewrites."""
-    (root / "lean-toolchain").write_text("leanprover/lean4:v4.32.0-rc1\n")
-    (root / "lakefile.toml").write_text(LAKEFILE)
-    docbuild = root / "docbuild"
-    docbuild.mkdir()
-    (docbuild / "lean-toolchain").write_text("leanprover/lean4:v4.32.0-rc1\n")
-    (docbuild / "lakefile.toml").write_text(DOCBUILD_LAKEFILE)
-
-
-# --------------------------------------------------------------------------- #
-# Version ordering
-# --------------------------------------------------------------------------- #
-def test_final_release_outranks_its_candidates() -> None:
-    """v4.33.0 is newer than every v4.33.0-rcN."""
-    assert version_key("v4.33.0") > version_key("v4.33.0-rc9")
-    assert version_key("v4.33.0-rc2") > version_key("v4.33.0-rc1")
-    assert version_key("v4.33.0-rc1") > version_key("v4.32.0")
-
-
-def test_version_key_rejects_non_releases() -> None:
-    """A branch name is not a release tag."""
-    with pytest.raises(ValueError, match="not a release tag"):
-        version_key("main")
-
-
-def test_is_prerelease() -> None:
-    """Release candidates are distinguishable from final releases."""
-    assert is_prerelease("v4.33.0-rc1")
-    assert not is_prerelease("v4.33.0")
-
-
-def test_prereleases_count_by_default() -> None:
-    """The pool tracks the newest release, which mid-cycle is an rc."""
-    tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1"]
-    assert newer_versions("v4.32.0-rc1", tags) == ["v4.32.0", "v4.33.0-rc1"]
-    assert newer_versions("v4.32.0-rc1", tags)[-1] == "v4.33.0-rc1"
-
-
-def test_stable_only_narrows_to_final_releases() -> None:
-    """``stable_only`` opts out of release candidates."""
-    tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1"]
-    assert newer_versions("v4.32.0-rc1", tags, stable_only=True) == ["v4.32.0"]
-
-
-def test_newer_versions_empty_when_current_is_latest() -> None:
-    """An up-to-date pin yields no bump target."""
-    assert newer_versions("v4.33.0", ["v4.32.0", "v4.33.0"], stable_only=False) == []
-
-
-def test_newer_versions_ignores_unparseable_tags() -> None:
-    """Only well-formed release tags are considered."""
-    tags = ["v4.33.0", "nightly-2026-07-01"]
-    assert newer_versions(
-        "v4.32.0",
-        [t for t in tags if t != "nightly-2026-07-01"],
-        stable_only=True,
-    ) == ["v4.33.0"]
-
-
-# --------------------------------------------------------------------------- #
-# Pins
-# --------------------------------------------------------------------------- #
-def test_current_version_reads_the_mathlib_pin(tmp_path: Path) -> None:
-    """The pinned Mathlib release comes from lakefile.toml."""
-    _write_repo(tmp_path)
-    assert current_version(tmp_path) == "v4.32.0-rc1"
-
-
-def test_pin_files_rewrites_all_four_pins(tmp_path: Path) -> None:
-    """A bump moves both toolchains and both dependency revs."""
-    _write_repo(tmp_path)
-    changed = pin_files(tmp_path, "v4.33.0-rc1")
-    assert len(changed) == 4
-    assert (tmp_path / "lean-toolchain").read_text() == "leanprover/lean4:v4.33.0-rc1\n"
-    assert 'rev = "v4.33.0-rc1"' in (tmp_path / "lakefile.toml").read_text()
-    assert (
-        tmp_path / "docbuild" / "lean-toolchain"
-    ).read_text() == "leanprover/lean4:v4.33.0-rc1\n"
-    assert (
-        'rev = "v4.33.0-rc1"' in (tmp_path / "docbuild" / "lakefile.toml").read_text()
-    )
-
-
-def test_pin_files_preserves_lean_options(tmp_path: Path) -> None:
-    """Rewriting pins must not disturb the gate-bearing [leanOptions]."""
-    _write_repo(tmp_path)
-    pin_files(tmp_path, "v4.33.0-rc1")
-    assert "relaxedAutoImplicit = false" in (tmp_path / "lakefile.toml").read_text()
-
-
-def test_pin_files_is_idempotent(tmp_path: Path) -> None:
-    """Re-pinning to the same version changes nothing."""
-    _write_repo(tmp_path)
-    pin_files(tmp_path, "v4.33.0-rc1")
-    assert pin_files(tmp_path, "v4.33.0-rc1") == []
-
-
-def test_pin_files_rejects_a_bad_version(tmp_path: Path) -> None:
-    """A non-release version string fails before touching any file."""
-    _write_repo(tmp_path)
-    with pytest.raises(SystemExit, match="not a release tag"):
-        pin_files(tmp_path, "main")
-    assert "v4.32.0-rc1" in (tmp_path / "lean-toolchain").read_text()
-
-
-def test_pin_files_reports_a_missing_pin(tmp_path: Path) -> None:
-    """A missing pin file is an error, not a silent skip."""
-    _write_repo(tmp_path)
-    (tmp_path / "docbuild" / "lean-toolchain").unlink()
-    with pytest.raises(SystemExit, match="missing pin file"):
-        pin_files(tmp_path, "v4.33.0-rc1")
-
-
-# --------------------------------------------------------------------------- #
-# Build-log triage
-# --------------------------------------------------------------------------- #
-BUILD_LOG = """\
-info: [1/900] Building LeanPool.Alpha.Core
-error: ./LeanPool/Alpha/Core.lean:12:2: unknown identifier 'Set.diff_eq'
-  the goal was
-    ⊢ s \\ t = s ∩ tᶜ
-info: [2/900] Building LeanPool.Beta.Main
-warning: ./LeanPool/Beta/Main.lean:3:0: `Symmetric` is deprecated
-info: [3/900] Building LeanPool.Gamma.Basic
-info: build completed
-"""
-
-
-def test_parse_build_log_buckets_by_project() -> None:
-    """Each diagnostic lands on the project whose file it names."""
-    buckets = parse_build_log(BUILD_LOG)
-    assert set(buckets) == {"Alpha", "Beta"}
-    assert len(buckets["Alpha"].errors) == 3  # message plus two goal lines
-    assert buckets["Beta"].warnings and not buckets["Beta"].errors
-
-
-def test_parse_build_log_attaches_continuation_lines() -> None:
-    """Indented goal-state lines stay with the error they explain."""
-    errors = parse_build_log(BUILD_LOG)["Alpha"].errors
-    assert "unknown identifier" in errors[0]
-    assert any("⊢" in line for line in errors)
-
-
-def test_build_report_separates_broken_from_warned() -> None:
-    """Only projects with errors become repair jobs."""
-    report = build_report(BUILD_LOG)
-    assert report["broken_projects"] == ["Alpha"]
-    assert report["warned_projects"] == ["Beta"]
-    assert report["clean"] is False
-
-
-def test_build_report_on_a_clean_build() -> None:
-    """A build with no diagnostics reports clean and schedules no repairs."""
-    report = build_report("info: [1/1] Building LeanPool.Alpha\ninfo: done\n")
-    assert report["clean"] is True
-    assert report["broken_projects"] == []
-
-
-def test_project_with_errors_is_not_also_listed_as_warned() -> None:
-    """A project that fails outright is a repair job, not a warning job."""
-    log = (
-        "info: [1/2] Building LeanPool.Alpha.Core\n"
-        "warning: ./LeanPool/Alpha/Core.lean:1:0: unused variable\n"
-        "error: ./LeanPool/Alpha/Core.lean:9:0: type mismatch\n"
-    )
-    report = build_report(log)
-    assert report["broken_projects"] == ["Alpha"]
-    assert report["warned_projects"] == []
-
-
-def test_diagnostic_without_a_path_uses_the_building_context() -> None:
-    """A message lake prints against a module still finds its project."""
-    log = "info: [1/2] Building LeanPool.Delta.Core\nerror: no such file or directory\n"
-    assert build_report(log)["broken_projects"] == ["Delta"]
-
-
-def test_excerpts_are_capped() -> None:
-    """A project that fails everywhere cannot flood the repair prompt."""
-    lines = ["info: [1/1] Building LeanPool.Alpha.Core"]
-    lines += [f"error: ./LeanPool/Alpha/Core.lean:{i}:0: boom" for i in range(200)]
-    entry = build_report("\n".join(lines))["broken"][0]
-    assert entry["error_count"] == 200
-    assert len(entry["errors"]) == 40
-
-
-def test_report_command_writes_json(tmp_path: Path) -> None:
-    """The report subcommand persists the artifact the workflow uploads."""
-    log = tmp_path / "build.log"
-    log.write_text(BUILD_LOG)
-    output = tmp_path / "report.json"
-    assert main(["report", "--log", str(log), "--output", str(output)]) == 0
-    assert '"broken_projects"' in output.read_text()
diff --git a/scripts/ci/bump-summary.py b/scripts/ci/bump-summary.py
deleted file mode 100644
index 2c2928df18..0000000000
--- a/scripts/ci/bump-summary.py
+++ /dev/null
@@ -1,77 +0,0 @@
-"""Render a bump report for humans, or one project's diagnostics for an agent.
-
-Used twice by `.github/workflows/mathlib-bump.yml`:
-
-    python3 scripts/ci/bump-summary.py bump-report.json
-        Markdown breakage table for the run's step summary.
-
-    python3 scripts/ci/bump-summary.py bump-report.json --project Polytopes
-        That project's build errors, written to `diagnostics.txt` for the
-        repair agent to start from.
-
-Only stdlib is used: this runs from a bare checkout, before any Python
-dependency install.
-"""
-
-import argparse
-import json
-import sys
-
-
-def render_summary(report: dict) -> str:
-    """Render the whole-run breakage table."""
-    broken = report.get("broken", [])
-    warned = report.get("warned", [])
-    lines = [
-        f"### Probe: {len(broken)} project(s) failing, "
-        f"{len(warned)} with warnings",
-        "",
-    ]
-    if not broken and not warned:
-        lines.append("The pool builds clean against this release.")
-        return "\n".join(lines) + "\n"
-    if broken:
-        lines += ["| Project | Errors |", "|---|---|"]
-        lines += [
-            f"| **{entry['project']}** | {entry['error_count']} |" for entry in broken
-        ]
-        lines.append("")
-    if warned:
-        lines += ["| Project (warnings only) | Warnings |", "|---|---|"]
-        lines += [
-            f"| {entry['project']} | {entry['warning_count']} |" for entry in warned
-        ]
-    return "\n".join(lines) + "\n"
-
-
-def render_project(report: dict, project: str) -> str:
-    """Render one project's diagnostics for its repair agent."""
-    for entry in report.get("broken", []):
-        if entry["project"] == project:
-            shown, total = len(entry["errors"]), entry["error_count"]
-            header = f"{total} error(s) building LeanPool.{project}"
-            if shown < total:
-                header += f" (first {shown} lines shown)"
-            return header + ":\n\n" + "\n".join(entry["errors"]) + "\n"
-    return f"No recorded errors for LeanPool.{project}.\n"
-
-
-def main(argv: list[str] | None = None) -> int:
-    """Print the requested rendering of a bump report."""
-    parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    parser.add_argument("report", help="path to bump-report.json")
-    parser.add_argument("--project", help="render only this project's errors")
-    args = parser.parse_args(argv)
-
-    with open(args.report, encoding="utf-8") as handle:
-        report = json.load(handle)
-
-    if args.project:
-        sys.stdout.write(render_project(report, args.project))
-    else:
-        sys.stdout.write(render_summary(report))
-    return 0
-
-
-if __name__ == "__main__":
-    sys.exit(main())