Automate NOTICE generation, Mathlib bumps, and import-PR rebasing

.claude/skills/version-bump-project/SKILL.md

@@ -0,0 +1,91 @@
+---
+name: version-bump-project
+description: Repair a SINGLE Lean Pool project's build against a new Lean/Mathlib release. Used by the mathlib-bump workflow's repair fan-out, one job per broken project. Use when asked to fix one project (not the whole pool) for a target version.
+argument-hint: <Project> <target-version> e.g. Polytopes v4.33.0-rc1
+---
+
+# Repair one project for a new Mathlib release
+
+Fix **only** `LeanPool/<Project>` so that `lake build LeanPool.<Project>`
+succeeds with **zero errors and zero warnings** under the target release. The
+project and version are the arguments; if either is missing, stop and say so.
+
+This runs headless in CI with no reviewer present. The whole-pool equivalent is
+the `version-bump` skill; this is its per-project unit of work. Pool projects
+never import each other, so your project is independent of every other repair
+running in parallel — never edit outside your project's directory.
+
+## Hard constraints (never violate)
+
+1. **No statement drops.** Every `theorem`/`lemma`/`def`/`instance`/`structure`/
+   `inductive`/`class`/`abbrev` that exists now must still exist when you finish.
+   A statement that Mathlib has since absorbed is *still* not yours to delete —
+   leave it and note it in your summary; that call belongs to the reviewer.
+2. **Change a statement only when the statement itself does not compile** under
+   the target (a renamed or removed Mathlib symbol in its type, or a name that
+   now collides with a new Mathlib declaration). Then make the *minimal*
+   meaning-preserving change — usually a rename that keeps the statement and
+   proof intact. Everything else: change proof bodies, tactics, and syntax only.
+   A `def` → `theorem` keyword change for a `Prop`-valued declaration flagged by
+   the `defProp` linter is allowed (same statement).
+3. **Never** add `sorry`, `admit`, `native_decide`, a new `axiom`, `unsafe`,
+   `partial`, a `maxHeartbeats`/`maxRecDepth` increase, `set_option linter.* false`,
+   or any nolint waiver. **Fix the code, not the check.** These are enforced by
+   `python/lean_pool/quality.py` on the assembled branch, so adding one does not
+   get the bump merged — it just wastes the run.
+4. **Never** edit `.github/`, `python/lean_pool/quality.py`, lint configs,
+   `lakefile.toml`'s `[leanOptions]`, `lean-toolchain`, or any file outside
+   `LeanPool/<Project>/` (and `LeanPool/<Project>.lean` if it exists).
+5. **Do not** commit, push, or open a PR. The workflow captures your working
+   tree as a patch and assembles it. Just leave the files fixed on disk.
+
+## Environment
+
+- The toolchain and Mathlib cache are already installed; `lake exe cache get`
+  has run. The pins are already at the target version.
+- **CLI only — the lean-lsp MCP is not available.** Use:
+  - `lake build LeanPool.<Project>` to check your work (this is the ground truth)
+  - `lake env lean <file>` to check a single file quickly
+  - `rg <pattern> .lake/packages/mathlib` to find what a symbol was renamed to
+- `diagnostics.txt` in the working directory holds the exact errors this project
+  produced during the probe build. Start there.
+
+## Recipe
+
+1. **Read `diagnostics.txt`** and bucket the errors by root cause. Most projects
+   fail for one or two reasons repeated many times, not N independent reasons.
+2. **Identify each root cause in Mathlib.** For a renamed lemma, `rg` the old
+   name in `.lake/packages/mathlib` — deprecation aliases usually carry a
+   `Use X instead` note naming the replacement. Trust the deprecation note over
+   a guess.
+3. **Apply the minimal fix** across the project. Prefer a mechanical rename over
+   a proof rewrite; prefer a proof rewrite over any signature change.
+4. **Rebuild** with `lake build LeanPool.<Project>` until there are no errors.
+5. **Clear warnings too** — CI fails on any `warning:` line. Typical sources:
+   deprecation renames (do what the warning says), unused `simp` arguments,
+   no-op or never-executed tactics, and the `defProp` `def` → `theorem` case.
+6. **Self-check before finishing:**
+   - `git diff` — is every changed file inside your project?
+   - Diff declaration *names* against the base revision. Anything present before
+     and missing now is a violation of constraint 1 unless it was a forced
+     rename you can justify.
+   - `git diff | rg 'sorry|admit|native_decide|maxHeartbeats|set_option linter'`
+     must be empty.
+
+## Report
+
+Finish with a short structured summary — it is the return value, not a message
+to a human:
+
+```
+project: <Project>
+status: clean | errors-remain | warnings-remain
+root_causes: <one line each>
+statements_modified: <qualified name + why, or "none">
+absorbed_by_mathlib: <declarations that now duplicate Mathlib, or "none">
+notes: <anything the reviewer must check by hand>
+```
+
+If you cannot get the project clean, say so plainly in `status` and report what
+remains. A partial, honest repair is useful; a green report that is not green is
+not. Never disable a check to make the build pass.

.github/BUMP_AUTOMATION.md

@@ -0,0 +1,117 @@
+# 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.
+
+## What runs, and what it costs
+
+| Stage | What it does | Cost |
+|---|---|---|
+| `detect` | Compares the pinned release against Mathlib's tags | free |
+| `probe` | Moves the pins, builds every project, buckets failures per project | free |
+| `repair` | One Claude job per broken project, in parallel | 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
+
+The `repair` input controls the fan-out:
+
+- `auto` (default) — repair final releases, report only on `-rc` tags. Mathlib
+  tags release candidates often; repairing each one would drain the token budget
+  for a version you are not adopting yet.
+- `always` — repair whatever was detected, including candidates.
+- `never` — probe only. Use this to size a bump before committing to it.
+
+## 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. 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. Re-run just
+the failed jobs from the run page, or fix that project by hand on the `bump/*`
+branch.