From 478eb338fb609d76fe8ff55fa2b1903e2c24ba30 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 15 Oct 2026 21:55:14 -0700 Subject: [PATCH 1/3] Run resumable version bumps on the Lean VM with cx account failover --- .github/BUMP_AUTOMATION.md | 204 +----- .github/workflows/claude-auth-check.yml | 53 -- .github/workflows/mathlib-bump.yml | 692 ------------------ python/lean_pool/bump_vm.py | 485 ++++++++++++ python/tests/test_bump_vm.py | 234 ++++++ scripts/version-bump/README.md | 101 +++ .../lean-pool-version-bump.service | 25 + .../version-bump/lean-pool-version-bump.timer | 11 + 8 files changed, 880 insertions(+), 925 deletions(-) delete mode 100644 .github/workflows/claude-auth-check.yml delete mode 100644 .github/workflows/mathlib-bump.yml create mode 100644 python/lean_pool/bump_vm.py create mode 100644 python/tests/test_bump_vm.py create mode 100644 scripts/version-bump/README.md create mode 100644 scripts/version-bump/lean-pool-version-bump.service create mode 100644 scripts/version-bump/lean-pool-version-bump.timer diff --git a/.github/BUMP_AUTOMATION.md b/.github/BUMP_AUTOMATION.md index 7dc10dfe30..e0f527f76f 100644 --- a/.github/BUMP_AUTOMATION.md +++ b/.github/BUMP_AUTOMATION.md @@ -1,182 +1,26 @@ # 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 | -| `auth` | One-minute check that the Claude token still works | negligible | -| `pin` | Moves the four pins, refreshes manifests, pushes `bump/` | 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@ - id: app-token - with: - app-id: ${{ secrets.APP_ID }} - private-key: ${{ secrets.APP_PRIVATE_KEY }} -- uses: actions/checkout@ - 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/` 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. +Version bumps run on the **Lean VM**, using its `cx` Codex accounts. GitHub-hosted +runners no longer perform migrations. The nightly check remains at 05:23 UTC. + +See [VM deployment and operations](../scripts/version-bump/README.md) for installation, +manual activation, recovery and validation. The implementation is +[`lean_pool.bump_vm`](../python/lean_pool/bump_vm.py). + +The controller uses a full-history checkout, preserving existing `bump/` +repairs while merging current main. This fixes the shallow checkout that made +resumed GitHub runs fail with `refusing to merge unrelated histories`. + +Each repair starts with the authenticated `cx` account with the most remaining +quota. Availability is measured using the highest used percentage across the +reported quota windows. After a failure or an unsuccessful repair, quotas are +probed again and the next eligible, untried account continues from the saved +edits. Unknown quota, identity failures, and accounts with 98% or more usage are +ineligible. Account occupancy does not affect eligibility. There is no Claude or +API fallback. Exhausted attempts keep a checkpoint and retry after an hour. + +The controller builds each project's public `Imports` module, checks warnings, +then runs the whole-pool build, index check, Mathlib linters, style checker and +quality checker independently of the agent. It opens or updates a **draft** PR; +reviewers assess statement changes and normal required CI before merging. +Execution transcripts, account identities and credentials remain private on the VM. 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/ 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_vm.py b/python/lean_pool/bump_vm.py new file mode 100644 index 0000000000..2bf346c59d --- /dev/null +++ b/python/lean_pool/bump_vm.py @@ -0,0 +1,485 @@ +"""Run resumable Lean/Mathlib migrations on the Lean VM's cx account pool.""" + +from __future__ import annotations + +import argparse +import fcntl +import json +import logging +import math +import os +import re +import shutil +import subprocess +from datetime import UTC, datetime +from pathlib import Path + +from lean_pool.bump import current_version, newer_versions, pin_files, remote_tags + +LOGGER = logging.getLogger(__name__) +REPOSITORY = "LeanPool/lean-pool" +REMOTE = f"https://github.com/{REPOSITORY}.git" +PINS = ( + "lean-toolchain", + "lakefile.toml", + "lake-manifest.json", + "docbuild/lean-toolchain", + "docbuild/lakefile.toml", + "docbuild/lake-manifest.json", +) +GATES = { + "indexes": ["lake", "exe", "mk_all", "--check"], + "linter": ["lake", "exe", "runLinter", "LeanPool"], + "style": ["lake", "exe", "lint-style", "LeanPool"], + "quality": [ + "uv", + "run", + "--directory", + "python", + "--locked", + "python", + "-m", + "lean_pool.quality", + "--repo", + "..", + ], +} +WARNING = re.compile(r"(^|: )warning:", re.M) + + +def rank_accounts(statuses: list[dict]) -> list[str]: + """Prefer most remaining quota in the most constrained reported window.""" + eligible = [] + for status in statuses: + used = status.get("usedPercent") + if ( + status.get("provider") not in (None, "openai") + or status.get("name") == "claude" + or not all( + status.get(key) + for key in ("ready", "authenticated", "identityOk", "available") + ) + or not isinstance(used, (int, float)) + or not math.isfinite(used) + or not 0 <= used < 98 + or not re.fullmatch(r"[a-z0-9][a-z0-9_-]*", status.get("name", "")) + ): + continue + eligible.append((used, status["name"])) + return [name for _, name in sorted(eligible)] + + +def save(path: Path, value: dict) -> None: + """Replace a private checkpoint atomically.""" + temporary = path.with_suffix(".tmp") + temporary.write_text(json.dumps(value, indent=2) + "\n") + temporary.replace(path) + + +class Runner: + """Own one persistent checkout, checkpoint, and set of private logs.""" + + def __init__(self, root: Path) -> None: + """Keep mutable run data outside the installed controller.""" + self.root = root + self.repository = root / "repository" + self.state_path = root / "pending.json" + self.state = ( + json.loads(self.state_path.read_text()) if self.state_path.exists() else {} + ) + self.environment = os.environ.copy() + for key in list(self.environment): + if key.startswith(("OPENAI_", "AZURE_OPENAI_", "ANTHROPIC_")): + self.environment.pop(key) + self.environment["LEAN_NUM_THREADS"] = "2" + + def command(self, *arguments: str, directory: Path | None = None) -> str: + """Run a controller command and retain ordinary error diagnostics.""" + result = subprocess.run( + arguments, + cwd=directory or self.repository, + env=self.environment, + text=True, + stdout=subprocess.PIPE, + check=True, + ) + return result.stdout.strip() + + def logged(self, arguments: list[str], name: str, prompt: str | None = None) -> int: + """Keep compiler and agent transcripts private, outside the checkout.""" + path = self.root / "logs" / name + LOGGER.info("Running %s; log: %s", arguments[0], path) + with path.open("w") as output: + return subprocess.run( + arguments, + cwd=self.repository, + env=self.environment, + input=prompt, + text=True, + stdout=output, + stderr=subprocess.STDOUT, + ).returncode + + def checkpoint(self, **values: object) -> None: + """Record progress before each interruptible operation.""" + self.state.update(values) + save(self.state_path, self.state) + + def changed_paths(self) -> list[str]: + """Include untracked agent edits when enforcing the write scope.""" + tracked = self.command("git", "diff", "--name-only", "-z", "HEAD") + untracked = self.command( + "git", "ls-files", "--others", "--exclude-standard", "-z" + ) + return [path for path in (tracked + "\0" + untracked).split("\0") if path] + + def commit_repairs(self, project: str) -> None: + """Preserve partial progress, refusing any edit outside this project.""" + paths = self.changed_paths() + for path in paths: + allowed = path == f"LeanPool/{project}.lean" or ( + path.startswith(f"LeanPool/{project}/") and path.endswith(".lean") + ) + if not allowed or (self.repository / path).is_symlink(): + raise RuntimeError(f"repair changed an unexpected path: {path}") + if paths: + self.command("git", "add", "--", *paths) + self.command( + "git", "commit", "-m", f"Repair {project} for {self.state['target']}" + ) + + def update_pins(self) -> None: + """Finish pin updates before a restart can merge more upstream work.""" + target = self.state["target"] + if self.command("git", "branch", "--show-current") != f"bump/{target}": + raise RuntimeError("interrupted pin checkout changed branches") + if set(self.changed_paths()) - set(PINS): + raise RuntimeError("unexpected edits during dependency update") + self.checkpoint(phase="pins") + pin_files(self.repository, target) + self.command("lake", "update", "mathlib") + self.command( + "lake", "update", "doc-gen4", directory=self.repository / "docbuild" + ) + self.command("git", "add", "--", *PINS) + if self.command("git", "diff", "--cached", "--name-only"): + self.command( + "git", "commit", "-m", f"chore: pin Lean and Mathlib to {target}" + ) + self.checkpoint(phase="cache") + + def checkout(self) -> None: + """Fetch complete ancestry so resuming a branch can merge current main.""" + if not self.repository.exists(): + self.command( + "git", "clone", REMOTE, str(self.repository), directory=self.root + ) + if self.command("git", "remote", "get-url", "origin") != REMOTE: + raise RuntimeError("the bump checkout has an unexpected origin") + if self.command("git", "rev-parse", "--is-shallow-repository") == "true": + self.command("git", "fetch", "--unshallow", "origin") + self.command("git", "config", "user.name", "Lean Pool version bump") + self.command( + "git", + "config", + "user.email", + "41898282+github-actions[bot]@users.noreply.github.com", + ) + if self.state.get("phase") == "pins": + self.update_pins() + if self.state.get("project"): + expected = f"bump/{self.state['target']}" + if self.command("git", "branch", "--show-current") != expected: + raise RuntimeError("interrupted repair checkout changed branches") + self.commit_repairs(self.state["project"]) + self.checkpoint(project=None) + if self.changed_paths(): + raise RuntimeError( + "preserving unexpected uncommitted changes in the bump checkout" + ) + self.command( + "git", + "fetch", + "--prune", + "origin", + "+refs/heads/*:refs/remotes/origin/*", + ) + + def select_target(self, requested: str | None, stable_only: bool) -> str | None: + """Resume pending work before detecting another upstream release.""" + if self.state.get("target"): + if requested and requested != self.state["target"]: + raise RuntimeError( + "finish the pending target before selecting another release" + ) + return self.state["target"] + self.command("git", "checkout", "--detach", "origin/main") + available = newer_versions( + current_version(self.repository), remote_tags(), stable_only=stable_only + ) + if requested and requested not in available: + raise RuntimeError( + "requested target must be a published newer Mathlib release" + ) + target = requested or (available[-1] if available else None) + if target: + self.checkpoint(target=target) + return target + + def prepare_branch(self, target: str) -> None: + """Keep local and remote repairs without resetting or force-pushing.""" + branch = f"bump/{target}" + branches = self.command( + "git", "for-each-ref", "--format=%(refname)" + ).splitlines() + if f"refs/heads/{branch}" in branches: + self.command("git", "checkout", branch) + elif f"refs/remotes/origin/{branch}" in branches: + self.command("git", "checkout", "-b", branch, f"origin/{branch}") + else: + self.command("git", "checkout", "-b", branch, "origin/main") + if f"refs/remotes/origin/{branch}" in branches: + self.command("git", "merge", "--no-edit", f"origin/{branch}") + self.command("git", "merge", "--no-edit", "origin/main") + self.update_pins() + self.command("git", "push", "origin", branch) + self.command("lake", "exe", "cache", "get") + + def build_project(self, project: str) -> bool: + """Build every source through its public Imports module, including warnings.""" + entry = self.repository / "LeanPool" / project / "Imports.lean" + module = f"LeanPool.{project}" + (".Imports" if entry.exists() else "") + name = f"build-{project}.log" + status = self.logged(["lake", "build", module], name) + return status == 0 and not WARNING.search( + (self.root / "logs" / name).read_text() + ) + + def repair(self, project: str) -> None: + """Try each eligible cx account once, retaining edits across failures.""" + tried: set[str] = set() + self.checkpoint(project=project) + while True: + statuses = json.loads(self.command("cx", "limits", "--json")) + candidates = [name for name in rank_accounts(statuses) if name not in tried] + if not candidates: + raise RuntimeError( + "cx waterfall exhausted; checkpoint retained for retry" + ) + account = candidates[0] + tried.add(account) + LOGGER.info("Repairing %s using cx %s", project, account) + before = self.command("git", "rev-parse", "HEAD") + status = self.logged( + self.agent_arguments(account), + f"repair-{project}-{account}.log", + self.prompt(project), + ) + if self.command("git", "rev-parse", "HEAD") != before: + raise RuntimeError("repair agent unexpectedly changed Git history") + self.commit_repairs(project) + if self.build_project(project): + self.checkpoint(project=None) + return + LOGGER.warning( + "cx %s exited %s; %s still needs repair", account, status, project + ) + + def agent_arguments(self, account: str) -> list[str]: + """Use cx credentials while keeping the repair agent inside its workspace.""" + return [ + "cx", + account, + "exec", + "--ignore-user-config", + "--sandbox", + "workspace-write", + "-c", + 'approval_policy="never"', + "-c", + "sandbox_workspace_write.network_access=true", + "--add-dir", + "/data/.elan", + "--add-dir", + "/data/codex/cache/shared", + "--model", + os.environ.get("LEAN_POOL_BUMP_MODEL", "gpt-6.1-sol"), + "-c", + 'model_reasoning_effort="xhigh"', + "--cd", + str(self.repository), + "-", + ] + + def prompt(self, project: str) -> str: + """Reconcile a previous attempt using the same files and fresh diagnostics.""" + diagnostics = (self.root / "logs" / f"build-{project}.log").read_text() + return f"""Repair LeanPool.{project} for {self.state["target"]}. +Earlier attempts may have left partial repairs. Inspect the files and Git history +and continue their work. Read .claude/skills/version-bump-project/SKILL.md and follow +its proof, statement-preservation and no-waiver constraints. Edit only +LeanPool/{project}/**/*.lean and LeanPool/{project}.lean if it exists. +Use CLI Lake/Lean and rg; do not delegate to other agents. Do not commit, push, +open a PR, change branches, or modify any other files. Do not weaken statements, +drop declarations, change checks or increase resource limits. The controller handles +checkpoints, commits, whole-pool validation and the draft PR. +Build LeanPool.{project}.Imports if that module exists, otherwise LeanPool.{project}. +Finish when that build has zero errors and warnings; report unresolved issues honestly. +Diagnostics are supplied below instead of diagnostics.txt. +Current build diagnostics (excerpt): +{diagnostics[-24000:]} +""" + + def validate(self) -> dict[str, bool]: + """Run the full build and every existing gate independently of the agent.""" + self.checkpoint(phase="validation") + status = self.logged(["lake", "build", "LeanPool"], "whole-pool.log") + results = { + "build": status == 0 + and not WARNING.search((self.root / "logs" / "whole-pool.log").read_text()) + } + for name, arguments in GATES.items(): + results[name] = ( + self.logged(arguments, f"gate-{name}.log") == 0 + if results["build"] + else False + ) + return results + + def pull_request_body( + self, revision: str, results: dict[str, bool], incomplete: bool + ) -> Path: + """Report measured validation at the precise commit being published.""" + rows = "\n".join( + f"| {name} | {'pass' if passed else 'FAIL / not run'} |" + for name, passed in results.items() + ) + body = self.root / "pull-request.md" + body.write_text( + f"Automated migration to `{self.state['target']}`, run on the Lean VM.\n\n" + f"Validation at `{revision}`:\n\n| Check | Result |\n|---|---|\n{rows}\n\n" + + ( + "Repair is incomplete; saved progress will be retried.\n\n" + if incomplete + else "" + ) + + "Review statement changes before marking ready. " + "Required CI must pass on the current head. " + "Execution logs and cx account data remain private on the VM.\n" + ) + return body + + def publish(self, results: dict[str, bool], incomplete: bool = False) -> None: + """Publish a draft with measured results; a racing push fails safely.""" + branch = f"bump/{self.state['target']}" + self.command("git", "push", "origin", branch) + revision = self.command("git", "rev-parse", "HEAD") + body = self.pull_request_body(revision, results, incomplete) + pulls = json.loads( + self.command( + "gh", + "pr", + "list", + "--repo", + REPOSITORY, + "--head", + branch, + "--state", + "open", + "--json", + "number", + ) + ) + if pulls: + self.command( + "gh", + "pr", + "edit", + str(pulls[0]["number"]), + "--repo", + REPOSITORY, + "--body-file", + str(body), + ) + else: + self.command( + "gh", + "pr", + "create", + "--repo", + REPOSITORY, + "--draft", + "--base", + "main", + "--head", + branch, + "--title", + f"chore: bump Lean and Mathlib to {self.state['target']}", + "--body-file", + str(body), + ) + + def run(self, requested: str | None, stable_only: bool, probe_only: bool) -> None: + """Keep the migration pending until every gate passes.""" + self.checkout() + target = self.select_target(requested, stable_only) + if not target: + LOGGER.info("Pool already tracks the newest Mathlib release") + return + self.prepare_branch(target) + self.checkpoint(phase="probe") + projects = sorted( + { + path.parent.name + for path in (self.repository / "LeanPool").glob("*/Imports.lean") + } + ) + if not projects: + raise RuntimeError("no project Imports modules found") + for project in projects: + if not self.build_project(project) and not probe_only: + try: + self.repair(project) + except RuntimeError: + self.publish({"build": False}, incomplete=True) + raise + self.command("git", "push", "origin", f"bump/{target}") + results = self.validate() + self.publish(results) + if not all(results.values()): + raise RuntimeError("migration has failing gates; checkpoint retained") + self.state["phase"] = "complete" + save(self.root / "completed.json", self.state) + self.state_path.unlink() + LOGGER.info("Migration validated and draft PR published") + + +def main() -> None: + """Serialize timer/manual activations and keep all runtime files private.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=Path("/data/lean-pool-bump")) + parser.add_argument("--version") + parser.add_argument("--stable-only", action="store_true") + parser.add_argument("--probe-only", action="store_true") + arguments = parser.parse_args() + os.umask(0o077) + root = arguments.root.resolve() + root.mkdir(parents=True, exist_ok=True, mode=0o700) + (root / "logs").mkdir(exist_ok=True) + logging.basicConfig( + level=logging.INFO, format="%(asctime)s %(levelname)s %(message)s" + ) + with (root / "run.lock").open("w") as lock: + try: + fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB) + except BlockingIOError: + LOGGER.info("A version bump is already running") + return + if shutil.disk_usage(root).free < 30 * 1024**3: + raise RuntimeError("version bump needs at least 30 GiB free") + LOGGER.info("Starting activation at %s", datetime.now(UTC).isoformat()) + Runner(root).run(arguments.version, arguments.stable_only, arguments.probe_only) + + +if __name__ == "__main__": + main() diff --git a/python/tests/test_bump_vm.py b/python/tests/test_bump_vm.py new file mode 100644 index 0000000000..5a2173939e --- /dev/null +++ b/python/tests/test_bump_vm.py @@ -0,0 +1,234 @@ +"""Exercise VM checkout recovery, quota waterfalls and independent validation.""" + +from __future__ import annotations + +import json +import subprocess +from pathlib import Path +from unittest.mock import Mock + +import pytest + +from lean_pool import bump_vm +from lean_pool.bump_vm import Runner, rank_accounts + + +def account(name: str, used: float | None, **overrides: object) -> dict: + """Describe an authenticated account without reading any credentials.""" + return { + "name": name, + "usedPercent": used, + "ready": True, + "authenticated": True, + "identityOk": True, + "available": True, + **overrides, + } + + +def test_quota_order_prefers_remaining_usage_over_reset_time() -> None: + """Sooner resets do not outrank more available quota.""" + statuses = [ + account("soon", 80, resetsAt=1), + account("most", 5, resetsAt=999999), + account("middle", 30), + ] + assert rank_accounts(statuses) == ["most", "middle", "soon"] + + +def test_unknown_exhausted_or_other_provider_accounts_are_excluded() -> None: + """Incomplete probes, identity failures, and Claude never enter the waterfall.""" + statuses = [ + account("good", 0), + account("unknown", None), + account("nonfinite", float("nan")), + account("exhausted", 98), + account("logged-out", 1, authenticated=False), + account("wrong-user", 1, identityOk=False), + account("blocked", 1, available=False), + account("claude", 0), + account("other", 0, provider="anthropic"), + ] + assert rank_accounts(statuses) == ["good"] + + +@pytest.fixture +def runner(tmp_path: Path) -> Runner: + """Construct an isolated controller with a pending test release.""" + (tmp_path / "logs").mkdir() + result = Runner(tmp_path) + result.checkpoint(target="v4.35.0") + return result + + +def test_waterfall_reprobes_and_keeps_edits_after_failure( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """A failing or falsely successful agent cannot stop project verification.""" + statuses = [account("first", 0), account("second", 5), account("third", 20)] + probes = iter([statuses, [account("second", 90), account("third", 10)]]) + attempts = [] + monkeypatch.setattr( + runner, + "command", + lambda *args: json.dumps(next(probes)) if args[0] == "cx" else "revision", + ) + monkeypatch.setattr(runner, "prompt", lambda project: "continue partial edits") + commits = Mock() + monkeypatch.setattr(runner, "commit_repairs", commits) + builds = Mock(side_effect=[False, True]) + monkeypatch.setattr(runner, "build_project", builds) + + def attempt(arguments: list[str], name: str, prompt: str) -> int: + attempts.append(arguments[:3]) + assert "--ignore-user-config" in arguments + assert prompt == "continue partial edits" + return 1 if len(attempts) == 1 else 0 + + monkeypatch.setattr(runner, "logged", attempt) + runner.repair("Example") + assert attempts == [["cx", "first", "exec"], ["cx", "third", "exec"]] + assert commits.call_count == 2 + assert runner.state["project"] is None + + +def test_all_accounts_failing_retains_checkpoint( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """Exhaustion waits for service retry instead of looping on the same account.""" + statuses = json.dumps([account("only", 0)]) + monkeypatch.setattr( + runner, "command", lambda *args: statuses if args[0] == "cx" else "head" + ) + monkeypatch.setattr(runner, "prompt", lambda project: "repair") + monkeypatch.setattr(runner, "logged", Mock(return_value=0)) + monkeypatch.setattr(runner, "commit_repairs", Mock()) + monkeypatch.setattr(runner, "build_project", Mock(return_value=False)) + with pytest.raises(RuntimeError, match="waterfall exhausted"): + runner.repair("Example") + assert runner.logged.call_count == 1 + assert json.loads(runner.state_path.read_text())["project"] == "Example" + + +def git(root: Path, *arguments: str) -> str: + """Run real local Git commands for ancestry and dirty-tree regressions.""" + return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip() + + +def test_shallow_checkout_resumes_real_branch_with_common_ancestor( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """Reproduce the old unrelated-histories failure and merge both lines of work.""" + source = tmp_path / "source" + source.mkdir() + git(source, "init", "-b", "main") + git(source, "config", "user.name", "Test") + git(source, "config", "user.email", "test@example.com") + (source / "base").write_text("base") + git(source, "add", ".") + git(source, "commit", "-m", "base") + git(source, "checkout", "-b", "bump/v4.35.0") + (source / "repair").write_text("existing repair") + git(source, "add", ".") + git(source, "commit", "-m", "existing repair") + repair = git(source, "rev-parse", "HEAD") + git(source, "checkout", "main") + (source / "upstream").write_text("new main work") + git(source, "add", ".") + git(source, "commit", "-m", "main moved") + upstream = git(source, "rev-parse", "HEAD") + remote = tmp_path / "remote.git" + git(tmp_path, "clone", "--bare", str(source), str(remote)) + monkeypatch.setattr(bump_vm, "REMOTE", remote.as_uri()) + root = tmp_path / "runtime" + root.mkdir() + git( + root, "clone", "--depth", "1", "--branch", "main", remote.as_uri(), "repository" + ) + worker = Runner(root) + worker.checkpoint(target="v4.35.0") + assert git(worker.repository, "rev-parse", "--is-shallow-repository") == "true" + worker.checkout() + monkeypatch.setattr(worker, "update_pins", Mock()) + original = worker.command + monkeypatch.setattr( + worker, + "command", + lambda *args, **kw: "" if args[0] == "lake" else original(*args, **kw), + ) + worker.prepare_branch("v4.35.0") + assert git(worker.repository, "rev-parse", "--is-shallow-repository") == "false" + git(worker.repository, "merge-base", "--is-ancestor", repair, "HEAD") + git(worker.repository, "merge-base", "--is-ancestor", upstream, "HEAD") + + +@pytest.mark.parametrize( + "path", [".github/workflows/check.yml", "LeanPool/Other/File.lean"] +) +def test_out_of_scope_repairs_are_preserved_but_never_committed( + runner: Runner, monkeypatch: pytest.MonkeyPatch, path: str +) -> None: + """A checkpoint cannot silently include unrelated agent edits.""" + monkeypatch.setattr(runner, "changed_paths", lambda: [path]) + commands = Mock() + monkeypatch.setattr(runner, "command", commands) + with pytest.raises(RuntimeError, match="unexpected path"): + runner.commit_repairs("Example") + commands.assert_not_called() + + +def test_build_success_with_warnings_still_needs_repair( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """Warnings remain a gate even when Lake returns zero.""" + (runner.root / "logs" / "build-Example.log").write_text( + "warning: unused simp argument" + ) + monkeypatch.setattr(runner, "logged", Mock(return_value=0)) + assert not runner.build_project("Example") + + +def test_all_existing_gates_run_and_failure_is_retained( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """The agent's exit status never substitutes for build and quality gates.""" + (runner.root / "logs" / "whole-pool.log").write_text("Build completed successfully") + calls = [] + + def logged(arguments: list[str], name: str) -> int: + calls.append(name) + return int(name == "gate-quality.log") + + monkeypatch.setattr(runner, "logged", logged) + results = runner.validate() + assert results == dict( + build=True, indexes=True, linter=True, style=True, quality=False + ) + assert len(calls) == 5 + assert runner.state_path.exists() + + +def test_pin_update_is_recovered_before_checkout_fetch( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """An interruption between rewriting pins and refreshing manifests is resumable.""" + runner.checkpoint(phase="pins") + runner.repository.mkdir() + calls = [] + + def command(*arguments: str) -> str: + calls.append(arguments) + if arguments[:3] == ("git", "remote", "get-url"): + return bump_vm.REMOTE + return "false" + + def update() -> None: + calls.append(("finish-pins",)) + + monkeypatch.setattr(runner, "command", command) + monkeypatch.setattr(runner, "changed_paths", lambda: []) + monkeypatch.setattr(runner, "update_pins", update) + runner.checkout() + finish = calls.index(("finish-pins",)) + fetch = next(i for i, call in enumerate(calls) if call[:2] == ("git", "fetch")) + assert finish < fetch diff --git a/scripts/version-bump/README.md b/scripts/version-bump/README.md new file mode 100644 index 0000000000..68b0843e9a --- /dev/null +++ b/scripts/version-bump/README.md @@ -0,0 +1,101 @@ +# Version bumps on the Lean VM + +The `lean-pool-version-bump.timer` user timer checks for new Mathlib releases, +including release candidates, at **05:23 UTC daily**. It also activates five +minutes after boot to resume interrupted work. The service runs entirely on +`lean`, independently of GitHub runners. It survives logout through user lingering. + +The controller resumes the oldest pending target, keeps a full-history private +checkout, merges current main without force-pushing, updates both sets of pins +and manifests, and fetches Mathlib's build cache. It builds each project's public +`Imports` module. Failing projects and warnings are repaired sequentially through +`cx`; each attempt probes quotas and picks the eligible account with the lowest +maximum used percentage across the reported windows. Thus the account with the +most remaining usable quota starts first, rather than the account resetting soonest. +Every eligible account is tried at most once per project per activation. Failed +attempts retain partial edits and refresh diagnostics for the next account. + +Repairs use `gpt-6.1-sol` / `xhigh`, with a workspace sandbox and CLI Lake/Lean. +Account configuration and MCP servers are not loaded into the agent. Subscription +credentials are supplied by `cx`; the runner clears inherited API credentials. +There is no Claude or API fallback, purchase, or reset-credit action. + +The service limits its process tree to 24 GiB and four CPU cores, with two Lean +threads, low scheduling weight and a 30 GiB free-space startup check. It neither +switches the shared `/data/lean-pool` checkout nor changes global account policy. +The account pool remains available to other services. + +## Deploy + +Use an authenticated VM operator account with GitHub push and PR access, elan, +Lake, uv, and the VM's existing `cx` installation. Enable user lingering if needed. +Install a trusted revision's Python package separately from the migration checkout: + +```sh +# From the trusted LeanPool checkout on the VM: +install -d -m 700 /data/lean-pool-bump/engine /data/lean-pool-bump/tmp +# Record the deployed commit outside the archive. +git rev-parse HEAD > /data/lean-pool-bump/engine-revision +# Do not replace the controller while its service is running. +git archive HEAD python scripts/version-bump | tar -x -C /data/lean-pool-bump/engine +cd /data/lean-pool-bump/engine/python +uv sync --locked +uv run python -m lean_pool.bump_vm --help +install -m 644 ../scripts/version-bump/*.service ../scripts/version-bump/*.timer \ + ~/.config/systemd/user/ +systemctl --user daemon-reload +systemctl --user enable --now lean-pool-version-bump.timer +systemctl --user start --no-block lean-pool-version-bump.service +``` + +During migration from the old GitHub workflow, disable `mathlib-bump.yml` before +starting the VM service, so two controllers cannot write the same branch. This +change removes that workflow from the repository; its historical logs remain. + +## Operate + +```sh +systemctl --user status lean-pool-version-bump.service +systemctl --user list-timers lean-pool-version-bump.timer +journalctl --user -u lean-pool-version-bump.service -n 30 +cat /data/lean-pool-bump/pending.json +# Manual check/resume, through the same process lock: +systemctl --user start --no-block lean-pool-version-bump.service +# Stop and disable future scheduling: +systemctl --user disable --now lean-pool-version-bump.timer +systemctl --user stop lean-pool-version-bump.service +``` + +With the service stopped, the installed module also accepts `--version v4.35.0`, +`--stable-only`, and `--probe-only`. Explicit targets must be published Mathlib +releases newer than main; a pending target cannot be silently replaced. Probe-only +runs still validate and publish a draft, but never invoke a repair account. +`LEAN_POOL_BUMP_MODEL` can override the repair model through the private optional +`/data/lean-pool-bump/environment` file. + +`pending.json`, the private checkout, logs and PR-body staging stay under +`/data/lean-pool-bump` with a private umask. A process lock prevents timer/manual +activation overlap. Systemd retries failures after an hour, while boot activation +resumes after restarts. Partial project edits and pin updates are checkpointed +before upstream merges. Unexpected edits, merge conflicts and racing pushes stop +without discarding changes; inspect and repair those explicitly. Do not delete a +pending checkpoint to force a fresh run. + +The controller commits and pushes repairs incrementally. A failed account +waterfall publishes saved progress as a draft and leaves the checkpoint pending. +Whole-pool build, warning, index, linter, style and quality results are measured +outside the agent. Only passing every gate clears the checkpoint; even then the +PR remains a draft for statement review and normal current-head CI. + +## Tests + +```sh +cd python +uv run ruff check +uv run ruff format --check +uv run --group test pytest tests/test_bump.py tests/test_bump_vm.py +``` + +Tests reproduce resuming a shallow clone with a real diverged Git history, check +live quota ordering and reordering, preserve failed-attempt checkpoints, reject +out-of-scope edits, and enforce independent warning and quality validation. diff --git a/scripts/version-bump/lean-pool-version-bump.service b/scripts/version-bump/lean-pool-version-bump.service new file mode 100644 index 0000000000..502850bd4d --- /dev/null +++ b/scripts/version-bump/lean-pool-version-bump.service @@ -0,0 +1,25 @@ +[Unit] +Description=Resume Lean Pool version bumps on the Lean VM using cx +Wants=network-online.target +After=network-online.target +StartLimitIntervalSec=0 + +[Service] +Type=oneshot +WorkingDirectory=/data/lean-pool-bump/engine/python +Environment=PATH=/home/vasil/.local/bin:/home/vasil/.elan/bin:/usr/local/bin:/usr/bin:/bin +Environment=TMPDIR=/data/lean-pool-bump/tmp +EnvironmentFile=-/data/lean-pool-bump/environment +ExecStart=/data/lean-pool-bump/engine/python/.venv/bin/python -m lean_pool.bump_vm +UMask=0077 +TimeoutStartSec=infinity +TimeoutStopSec=30s +KillMode=control-group +Restart=on-failure +RestartSec=1h +MemoryMax=24G +CPUQuota=400% +TasksMax=4096 +Nice=10 +CPUWeight=20 +IOWeight=20 diff --git a/scripts/version-bump/lean-pool-version-bump.timer b/scripts/version-bump/lean-pool-version-bump.timer new file mode 100644 index 0000000000..6b7cadb432 --- /dev/null +++ b/scripts/version-bump/lean-pool-version-bump.timer @@ -0,0 +1,11 @@ +[Unit] +Description=Check nightly for a new Lean/Mathlib release on the Lean VM + +[Timer] +OnCalendar=*-*-* 05:23:00 UTC +OnBootSec=5min +Persistent=true +Unit=lean-pool-version-bump.service + +[Install] +WantedBy=timers.target From b9a0c4119150e6b174aafb12a9a6de45498bd959 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 15 Oct 2026 21:57:25 -0700 Subject: [PATCH 2/3] Continue other project repairs after an unfinished account waterfall --- python/lean_pool/bump_vm.py | 18 ++++++++++----- python/tests/test_bump_vm.py | 23 +++++++++++++++++++ scripts/version-bump/README.md | 4 ++-- .../lean-pool-version-bump.service | 1 + 4 files changed, 38 insertions(+), 8 deletions(-) diff --git a/python/lean_pool/bump_vm.py b/python/lean_pool/bump_vm.py index 2bf346c59d..12f898b8e8 100644 --- a/python/lean_pool/bump_vm.py +++ b/python/lean_pool/bump_vm.py @@ -47,6 +47,10 @@ WARNING = re.compile(r"(^|: )warning:", re.M) +class RepairIncompleteError(RuntimeError): + """The account waterfall could not finish a project in this activation.""" + + def rank_accounts(statuses: list[dict]) -> list[str]: """Prefer most remaining quota in the most constrained reported window.""" eligible = [] @@ -263,7 +267,7 @@ def repair(self, project: str) -> None: statuses = json.loads(self.command("cx", "limits", "--json")) candidates = [name for name in rank_accounts(statuses) if name not in tried] if not candidates: - raise RuntimeError( + raise RepairIncompleteError( "cx waterfall exhausted; checkpoint retained for retry" ) account = candidates[0] @@ -436,13 +440,15 @@ def run(self, requested: str | None, stable_only: bool, probe_only: bool) -> Non ) if not projects: raise RuntimeError("no project Imports modules found") - for project in projects: - if not self.build_project(project) and not probe_only: + broken = [project for project in projects if not self.build_project(project)] + self.checkpoint(phase="repair", broken=broken) + if not probe_only: + for project in broken: try: self.repair(project) - except RuntimeError: - self.publish({"build": False}, incomplete=True) - raise + except RepairIncompleteError: + LOGGER.warning("Account waterfall did not finish %s", project) + self.checkpoint(project=None) self.command("git", "push", "origin", f"bump/{target}") results = self.validate() self.publish(results) diff --git a/python/tests/test_bump_vm.py b/python/tests/test_bump_vm.py index 5a2173939e..df029856ce 100644 --- a/python/tests/test_bump_vm.py +++ b/python/tests/test_bump_vm.py @@ -232,3 +232,26 @@ def update() -> None: finish = calls.index(("finish-pins",)) fetch = next(i for i, call in enumerate(calls) if call[:2] == ("git", "fetch")) assert finish < fetch + + +def test_unfinished_project_does_not_skip_other_repairs( + runner: Runner, monkeypatch: pytest.MonkeyPatch +) -> None: + """A difficult proof must not starve the rest of the migration.""" + for project in ("First", "Second"): + directory = runner.repository / "LeanPool" / project + directory.mkdir(parents=True) + (directory / "Imports.lean").write_text("-- example") + monkeypatch.setattr(runner, "checkout", Mock()) + monkeypatch.setattr(runner, "select_target", Mock(return_value="v4.35.0")) + monkeypatch.setattr(runner, "prepare_branch", Mock()) + monkeypatch.setattr(runner, "build_project", Mock(return_value=False)) + repairs = Mock(side_effect=[bump_vm.RepairIncompleteError("unfinished"), None]) + monkeypatch.setattr(runner, "repair", repairs) + monkeypatch.setattr(runner, "command", Mock()) + monkeypatch.setattr(runner, "validate", Mock(return_value={"build": False})) + monkeypatch.setattr(runner, "publish", Mock()) + with pytest.raises(RuntimeError, match="failing gates"): + runner.run(None, False, False) + assert [call.args[0] for call in repairs.call_args_list] == ["First", "Second"] + assert runner.state_path.exists() diff --git a/scripts/version-bump/README.md b/scripts/version-bump/README.md index 68b0843e9a..e9bb55bd95 100644 --- a/scripts/version-bump/README.md +++ b/scripts/version-bump/README.md @@ -81,8 +81,8 @@ before upstream merges. Unexpected edits, merge conflicts and racing pushes stop without discarding changes; inspect and repair those explicitly. Do not delete a pending checkpoint to force a fresh run. -The controller commits and pushes repairs incrementally. A failed account -waterfall publishes saved progress as a draft and leaves the checkpoint pending. +The controller commits and pushes repairs incrementally. An unfinished project does not skip other project repairs. A failed account +waterfall retains saved progress for the draft and leaves the checkpoint pending. Whole-pool build, warning, index, linter, style and quality results are measured outside the agent. Only passing every gate clears the checkpoint; even then the PR remains a draft for statement review and normal current-head CI. diff --git a/scripts/version-bump/lean-pool-version-bump.service b/scripts/version-bump/lean-pool-version-bump.service index 502850bd4d..bc5307fe1d 100644 --- a/scripts/version-bump/lean-pool-version-bump.service +++ b/scripts/version-bump/lean-pool-version-bump.service @@ -1,5 +1,6 @@ [Unit] Description=Resume Lean Pool version bumps on the Lean VM using cx +ConditionPathIsMountPoint=/data Wants=network-online.target After=network-online.target StartLimitIntervalSec=0 From a2ea06c6873dc528e56ad2b525a9f8ddc6b35214 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 15 Oct 2026 22:05:05 -0700 Subject: [PATCH 3/3] Move version-bump implementation and tests to lean-pool-automation --- .github/BUMP_AUTOMATION.md | 31 +- python/lean_pool/bump.py | 319 ------------ python/lean_pool/bump_vm.py | 491 ------------------ python/tests/test_bump.py | 239 --------- python/tests/test_bump_vm.py | 257 --------- scripts/ci/bump-summary.py | 77 --- scripts/version-bump/README.md | 101 ---- .../lean-pool-version-bump.service | 26 - .../version-bump/lean-pool-version-bump.timer | 11 - 9 files changed, 9 insertions(+), 1543 deletions(-) delete mode 100644 python/lean_pool/bump.py delete mode 100644 python/lean_pool/bump_vm.py delete mode 100644 python/tests/test_bump.py delete mode 100644 python/tests/test_bump_vm.py delete mode 100644 scripts/ci/bump-summary.py delete mode 100644 scripts/version-bump/README.md delete mode 100644 scripts/version-bump/lean-pool-version-bump.service delete mode 100644 scripts/version-bump/lean-pool-version-bump.timer diff --git a/.github/BUMP_AUTOMATION.md b/.github/BUMP_AUTOMATION.md index e0f527f76f..9d852c8626 100644 --- a/.github/BUMP_AUTOMATION.md +++ b/.github/BUMP_AUTOMATION.md @@ -1,26 +1,13 @@ # Automated Mathlib bumps -Version bumps run on the **Lean VM**, using its `cx` Codex accounts. GitHub-hosted -runners no longer perform migrations. The nightly check remains at 05:23 UTC. +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. -See [VM deployment and operations](../scripts/version-bump/README.md) for installation, -manual activation, recovery and validation. The implementation is -[`lean_pool.bump_vm`](../python/lean_pool/bump_vm.py). +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. -The controller uses a full-history checkout, preserving existing `bump/` -repairs while merging current main. This fixes the shallow checkout that made -resumed GitHub runs fail with `refusing to merge unrelated histories`. - -Each repair starts with the authenticated `cx` account with the most remaining -quota. Availability is measured using the highest used percentage across the -reported quota windows. After a failure or an unsuccessful repair, quotas are -probed again and the next eligible, untried account continues from the saved -edits. Unknown quota, identity failures, and accounts with 98% or more usage are -ineligible. Account occupancy does not affect eligibility. There is no Claude or -API fallback. Exhausted attempts keep a checkpoint and retry after an hour. - -The controller builds each project's public `Imports` module, checks warnings, -then runs the whole-pool build, index check, Mathlib linters, style checker and -quality checker independently of the agent. It opens or updates a **draft** PR; -reviewers assess statement changes and normal required CI before merging. -Execution transcripts, account identities and credentials remain private on the VM. +GitHub-hosted runners no longer perform migrations. Normal required PR checks +continue to run on the resulting content changes. 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: ::: `; 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/lean_pool/bump_vm.py b/python/lean_pool/bump_vm.py deleted file mode 100644 index 12f898b8e8..0000000000 --- a/python/lean_pool/bump_vm.py +++ /dev/null @@ -1,491 +0,0 @@ -"""Run resumable Lean/Mathlib migrations on the Lean VM's cx account pool.""" - -from __future__ import annotations - -import argparse -import fcntl -import json -import logging -import math -import os -import re -import shutil -import subprocess -from datetime import UTC, datetime -from pathlib import Path - -from lean_pool.bump import current_version, newer_versions, pin_files, remote_tags - -LOGGER = logging.getLogger(__name__) -REPOSITORY = "LeanPool/lean-pool" -REMOTE = f"https://github.com/{REPOSITORY}.git" -PINS = ( - "lean-toolchain", - "lakefile.toml", - "lake-manifest.json", - "docbuild/lean-toolchain", - "docbuild/lakefile.toml", - "docbuild/lake-manifest.json", -) -GATES = { - "indexes": ["lake", "exe", "mk_all", "--check"], - "linter": ["lake", "exe", "runLinter", "LeanPool"], - "style": ["lake", "exe", "lint-style", "LeanPool"], - "quality": [ - "uv", - "run", - "--directory", - "python", - "--locked", - "python", - "-m", - "lean_pool.quality", - "--repo", - "..", - ], -} -WARNING = re.compile(r"(^|: )warning:", re.M) - - -class RepairIncompleteError(RuntimeError): - """The account waterfall could not finish a project in this activation.""" - - -def rank_accounts(statuses: list[dict]) -> list[str]: - """Prefer most remaining quota in the most constrained reported window.""" - eligible = [] - for status in statuses: - used = status.get("usedPercent") - if ( - status.get("provider") not in (None, "openai") - or status.get("name") == "claude" - or not all( - status.get(key) - for key in ("ready", "authenticated", "identityOk", "available") - ) - or not isinstance(used, (int, float)) - or not math.isfinite(used) - or not 0 <= used < 98 - or not re.fullmatch(r"[a-z0-9][a-z0-9_-]*", status.get("name", "")) - ): - continue - eligible.append((used, status["name"])) - return [name for _, name in sorted(eligible)] - - -def save(path: Path, value: dict) -> None: - """Replace a private checkpoint atomically.""" - temporary = path.with_suffix(".tmp") - temporary.write_text(json.dumps(value, indent=2) + "\n") - temporary.replace(path) - - -class Runner: - """Own one persistent checkout, checkpoint, and set of private logs.""" - - def __init__(self, root: Path) -> None: - """Keep mutable run data outside the installed controller.""" - self.root = root - self.repository = root / "repository" - self.state_path = root / "pending.json" - self.state = ( - json.loads(self.state_path.read_text()) if self.state_path.exists() else {} - ) - self.environment = os.environ.copy() - for key in list(self.environment): - if key.startswith(("OPENAI_", "AZURE_OPENAI_", "ANTHROPIC_")): - self.environment.pop(key) - self.environment["LEAN_NUM_THREADS"] = "2" - - def command(self, *arguments: str, directory: Path | None = None) -> str: - """Run a controller command and retain ordinary error diagnostics.""" - result = subprocess.run( - arguments, - cwd=directory or self.repository, - env=self.environment, - text=True, - stdout=subprocess.PIPE, - check=True, - ) - return result.stdout.strip() - - def logged(self, arguments: list[str], name: str, prompt: str | None = None) -> int: - """Keep compiler and agent transcripts private, outside the checkout.""" - path = self.root / "logs" / name - LOGGER.info("Running %s; log: %s", arguments[0], path) - with path.open("w") as output: - return subprocess.run( - arguments, - cwd=self.repository, - env=self.environment, - input=prompt, - text=True, - stdout=output, - stderr=subprocess.STDOUT, - ).returncode - - def checkpoint(self, **values: object) -> None: - """Record progress before each interruptible operation.""" - self.state.update(values) - save(self.state_path, self.state) - - def changed_paths(self) -> list[str]: - """Include untracked agent edits when enforcing the write scope.""" - tracked = self.command("git", "diff", "--name-only", "-z", "HEAD") - untracked = self.command( - "git", "ls-files", "--others", "--exclude-standard", "-z" - ) - return [path for path in (tracked + "\0" + untracked).split("\0") if path] - - def commit_repairs(self, project: str) -> None: - """Preserve partial progress, refusing any edit outside this project.""" - paths = self.changed_paths() - for path in paths: - allowed = path == f"LeanPool/{project}.lean" or ( - path.startswith(f"LeanPool/{project}/") and path.endswith(".lean") - ) - if not allowed or (self.repository / path).is_symlink(): - raise RuntimeError(f"repair changed an unexpected path: {path}") - if paths: - self.command("git", "add", "--", *paths) - self.command( - "git", "commit", "-m", f"Repair {project} for {self.state['target']}" - ) - - def update_pins(self) -> None: - """Finish pin updates before a restart can merge more upstream work.""" - target = self.state["target"] - if self.command("git", "branch", "--show-current") != f"bump/{target}": - raise RuntimeError("interrupted pin checkout changed branches") - if set(self.changed_paths()) - set(PINS): - raise RuntimeError("unexpected edits during dependency update") - self.checkpoint(phase="pins") - pin_files(self.repository, target) - self.command("lake", "update", "mathlib") - self.command( - "lake", "update", "doc-gen4", directory=self.repository / "docbuild" - ) - self.command("git", "add", "--", *PINS) - if self.command("git", "diff", "--cached", "--name-only"): - self.command( - "git", "commit", "-m", f"chore: pin Lean and Mathlib to {target}" - ) - self.checkpoint(phase="cache") - - def checkout(self) -> None: - """Fetch complete ancestry so resuming a branch can merge current main.""" - if not self.repository.exists(): - self.command( - "git", "clone", REMOTE, str(self.repository), directory=self.root - ) - if self.command("git", "remote", "get-url", "origin") != REMOTE: - raise RuntimeError("the bump checkout has an unexpected origin") - if self.command("git", "rev-parse", "--is-shallow-repository") == "true": - self.command("git", "fetch", "--unshallow", "origin") - self.command("git", "config", "user.name", "Lean Pool version bump") - self.command( - "git", - "config", - "user.email", - "41898282+github-actions[bot]@users.noreply.github.com", - ) - if self.state.get("phase") == "pins": - self.update_pins() - if self.state.get("project"): - expected = f"bump/{self.state['target']}" - if self.command("git", "branch", "--show-current") != expected: - raise RuntimeError("interrupted repair checkout changed branches") - self.commit_repairs(self.state["project"]) - self.checkpoint(project=None) - if self.changed_paths(): - raise RuntimeError( - "preserving unexpected uncommitted changes in the bump checkout" - ) - self.command( - "git", - "fetch", - "--prune", - "origin", - "+refs/heads/*:refs/remotes/origin/*", - ) - - def select_target(self, requested: str | None, stable_only: bool) -> str | None: - """Resume pending work before detecting another upstream release.""" - if self.state.get("target"): - if requested and requested != self.state["target"]: - raise RuntimeError( - "finish the pending target before selecting another release" - ) - return self.state["target"] - self.command("git", "checkout", "--detach", "origin/main") - available = newer_versions( - current_version(self.repository), remote_tags(), stable_only=stable_only - ) - if requested and requested not in available: - raise RuntimeError( - "requested target must be a published newer Mathlib release" - ) - target = requested or (available[-1] if available else None) - if target: - self.checkpoint(target=target) - return target - - def prepare_branch(self, target: str) -> None: - """Keep local and remote repairs without resetting or force-pushing.""" - branch = f"bump/{target}" - branches = self.command( - "git", "for-each-ref", "--format=%(refname)" - ).splitlines() - if f"refs/heads/{branch}" in branches: - self.command("git", "checkout", branch) - elif f"refs/remotes/origin/{branch}" in branches: - self.command("git", "checkout", "-b", branch, f"origin/{branch}") - else: - self.command("git", "checkout", "-b", branch, "origin/main") - if f"refs/remotes/origin/{branch}" in branches: - self.command("git", "merge", "--no-edit", f"origin/{branch}") - self.command("git", "merge", "--no-edit", "origin/main") - self.update_pins() - self.command("git", "push", "origin", branch) - self.command("lake", "exe", "cache", "get") - - def build_project(self, project: str) -> bool: - """Build every source through its public Imports module, including warnings.""" - entry = self.repository / "LeanPool" / project / "Imports.lean" - module = f"LeanPool.{project}" + (".Imports" if entry.exists() else "") - name = f"build-{project}.log" - status = self.logged(["lake", "build", module], name) - return status == 0 and not WARNING.search( - (self.root / "logs" / name).read_text() - ) - - def repair(self, project: str) -> None: - """Try each eligible cx account once, retaining edits across failures.""" - tried: set[str] = set() - self.checkpoint(project=project) - while True: - statuses = json.loads(self.command("cx", "limits", "--json")) - candidates = [name for name in rank_accounts(statuses) if name not in tried] - if not candidates: - raise RepairIncompleteError( - "cx waterfall exhausted; checkpoint retained for retry" - ) - account = candidates[0] - tried.add(account) - LOGGER.info("Repairing %s using cx %s", project, account) - before = self.command("git", "rev-parse", "HEAD") - status = self.logged( - self.agent_arguments(account), - f"repair-{project}-{account}.log", - self.prompt(project), - ) - if self.command("git", "rev-parse", "HEAD") != before: - raise RuntimeError("repair agent unexpectedly changed Git history") - self.commit_repairs(project) - if self.build_project(project): - self.checkpoint(project=None) - return - LOGGER.warning( - "cx %s exited %s; %s still needs repair", account, status, project - ) - - def agent_arguments(self, account: str) -> list[str]: - """Use cx credentials while keeping the repair agent inside its workspace.""" - return [ - "cx", - account, - "exec", - "--ignore-user-config", - "--sandbox", - "workspace-write", - "-c", - 'approval_policy="never"', - "-c", - "sandbox_workspace_write.network_access=true", - "--add-dir", - "/data/.elan", - "--add-dir", - "/data/codex/cache/shared", - "--model", - os.environ.get("LEAN_POOL_BUMP_MODEL", "gpt-6.1-sol"), - "-c", - 'model_reasoning_effort="xhigh"', - "--cd", - str(self.repository), - "-", - ] - - def prompt(self, project: str) -> str: - """Reconcile a previous attempt using the same files and fresh diagnostics.""" - diagnostics = (self.root / "logs" / f"build-{project}.log").read_text() - return f"""Repair LeanPool.{project} for {self.state["target"]}. -Earlier attempts may have left partial repairs. Inspect the files and Git history -and continue their work. Read .claude/skills/version-bump-project/SKILL.md and follow -its proof, statement-preservation and no-waiver constraints. Edit only -LeanPool/{project}/**/*.lean and LeanPool/{project}.lean if it exists. -Use CLI Lake/Lean and rg; do not delegate to other agents. Do not commit, push, -open a PR, change branches, or modify any other files. Do not weaken statements, -drop declarations, change checks or increase resource limits. The controller handles -checkpoints, commits, whole-pool validation and the draft PR. -Build LeanPool.{project}.Imports if that module exists, otherwise LeanPool.{project}. -Finish when that build has zero errors and warnings; report unresolved issues honestly. -Diagnostics are supplied below instead of diagnostics.txt. -Current build diagnostics (excerpt): -{diagnostics[-24000:]} -""" - - def validate(self) -> dict[str, bool]: - """Run the full build and every existing gate independently of the agent.""" - self.checkpoint(phase="validation") - status = self.logged(["lake", "build", "LeanPool"], "whole-pool.log") - results = { - "build": status == 0 - and not WARNING.search((self.root / "logs" / "whole-pool.log").read_text()) - } - for name, arguments in GATES.items(): - results[name] = ( - self.logged(arguments, f"gate-{name}.log") == 0 - if results["build"] - else False - ) - return results - - def pull_request_body( - self, revision: str, results: dict[str, bool], incomplete: bool - ) -> Path: - """Report measured validation at the precise commit being published.""" - rows = "\n".join( - f"| {name} | {'pass' if passed else 'FAIL / not run'} |" - for name, passed in results.items() - ) - body = self.root / "pull-request.md" - body.write_text( - f"Automated migration to `{self.state['target']}`, run on the Lean VM.\n\n" - f"Validation at `{revision}`:\n\n| Check | Result |\n|---|---|\n{rows}\n\n" - + ( - "Repair is incomplete; saved progress will be retried.\n\n" - if incomplete - else "" - ) - + "Review statement changes before marking ready. " - "Required CI must pass on the current head. " - "Execution logs and cx account data remain private on the VM.\n" - ) - return body - - def publish(self, results: dict[str, bool], incomplete: bool = False) -> None: - """Publish a draft with measured results; a racing push fails safely.""" - branch = f"bump/{self.state['target']}" - self.command("git", "push", "origin", branch) - revision = self.command("git", "rev-parse", "HEAD") - body = self.pull_request_body(revision, results, incomplete) - pulls = json.loads( - self.command( - "gh", - "pr", - "list", - "--repo", - REPOSITORY, - "--head", - branch, - "--state", - "open", - "--json", - "number", - ) - ) - if pulls: - self.command( - "gh", - "pr", - "edit", - str(pulls[0]["number"]), - "--repo", - REPOSITORY, - "--body-file", - str(body), - ) - else: - self.command( - "gh", - "pr", - "create", - "--repo", - REPOSITORY, - "--draft", - "--base", - "main", - "--head", - branch, - "--title", - f"chore: bump Lean and Mathlib to {self.state['target']}", - "--body-file", - str(body), - ) - - def run(self, requested: str | None, stable_only: bool, probe_only: bool) -> None: - """Keep the migration pending until every gate passes.""" - self.checkout() - target = self.select_target(requested, stable_only) - if not target: - LOGGER.info("Pool already tracks the newest Mathlib release") - return - self.prepare_branch(target) - self.checkpoint(phase="probe") - projects = sorted( - { - path.parent.name - for path in (self.repository / "LeanPool").glob("*/Imports.lean") - } - ) - if not projects: - raise RuntimeError("no project Imports modules found") - broken = [project for project in projects if not self.build_project(project)] - self.checkpoint(phase="repair", broken=broken) - if not probe_only: - for project in broken: - try: - self.repair(project) - except RepairIncompleteError: - LOGGER.warning("Account waterfall did not finish %s", project) - self.checkpoint(project=None) - self.command("git", "push", "origin", f"bump/{target}") - results = self.validate() - self.publish(results) - if not all(results.values()): - raise RuntimeError("migration has failing gates; checkpoint retained") - self.state["phase"] = "complete" - save(self.root / "completed.json", self.state) - self.state_path.unlink() - LOGGER.info("Migration validated and draft PR published") - - -def main() -> None: - """Serialize timer/manual activations and keep all runtime files private.""" - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("--root", type=Path, default=Path("/data/lean-pool-bump")) - parser.add_argument("--version") - parser.add_argument("--stable-only", action="store_true") - parser.add_argument("--probe-only", action="store_true") - arguments = parser.parse_args() - os.umask(0o077) - root = arguments.root.resolve() - root.mkdir(parents=True, exist_ok=True, mode=0o700) - (root / "logs").mkdir(exist_ok=True) - logging.basicConfig( - level=logging.INFO, format="%(asctime)s %(levelname)s %(message)s" - ) - with (root / "run.lock").open("w") as lock: - try: - fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB) - except BlockingIOError: - LOGGER.info("A version bump is already running") - return - if shutil.disk_usage(root).free < 30 * 1024**3: - raise RuntimeError("version bump needs at least 30 GiB free") - LOGGER.info("Starting activation at %s", datetime.now(UTC).isoformat()) - Runner(root).run(arguments.version, arguments.stable_only, arguments.probe_only) - - -if __name__ == "__main__": - 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/python/tests/test_bump_vm.py b/python/tests/test_bump_vm.py deleted file mode 100644 index df029856ce..0000000000 --- a/python/tests/test_bump_vm.py +++ /dev/null @@ -1,257 +0,0 @@ -"""Exercise VM checkout recovery, quota waterfalls and independent validation.""" - -from __future__ import annotations - -import json -import subprocess -from pathlib import Path -from unittest.mock import Mock - -import pytest - -from lean_pool import bump_vm -from lean_pool.bump_vm import Runner, rank_accounts - - -def account(name: str, used: float | None, **overrides: object) -> dict: - """Describe an authenticated account without reading any credentials.""" - return { - "name": name, - "usedPercent": used, - "ready": True, - "authenticated": True, - "identityOk": True, - "available": True, - **overrides, - } - - -def test_quota_order_prefers_remaining_usage_over_reset_time() -> None: - """Sooner resets do not outrank more available quota.""" - statuses = [ - account("soon", 80, resetsAt=1), - account("most", 5, resetsAt=999999), - account("middle", 30), - ] - assert rank_accounts(statuses) == ["most", "middle", "soon"] - - -def test_unknown_exhausted_or_other_provider_accounts_are_excluded() -> None: - """Incomplete probes, identity failures, and Claude never enter the waterfall.""" - statuses = [ - account("good", 0), - account("unknown", None), - account("nonfinite", float("nan")), - account("exhausted", 98), - account("logged-out", 1, authenticated=False), - account("wrong-user", 1, identityOk=False), - account("blocked", 1, available=False), - account("claude", 0), - account("other", 0, provider="anthropic"), - ] - assert rank_accounts(statuses) == ["good"] - - -@pytest.fixture -def runner(tmp_path: Path) -> Runner: - """Construct an isolated controller with a pending test release.""" - (tmp_path / "logs").mkdir() - result = Runner(tmp_path) - result.checkpoint(target="v4.35.0") - return result - - -def test_waterfall_reprobes_and_keeps_edits_after_failure( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """A failing or falsely successful agent cannot stop project verification.""" - statuses = [account("first", 0), account("second", 5), account("third", 20)] - probes = iter([statuses, [account("second", 90), account("third", 10)]]) - attempts = [] - monkeypatch.setattr( - runner, - "command", - lambda *args: json.dumps(next(probes)) if args[0] == "cx" else "revision", - ) - monkeypatch.setattr(runner, "prompt", lambda project: "continue partial edits") - commits = Mock() - monkeypatch.setattr(runner, "commit_repairs", commits) - builds = Mock(side_effect=[False, True]) - monkeypatch.setattr(runner, "build_project", builds) - - def attempt(arguments: list[str], name: str, prompt: str) -> int: - attempts.append(arguments[:3]) - assert "--ignore-user-config" in arguments - assert prompt == "continue partial edits" - return 1 if len(attempts) == 1 else 0 - - monkeypatch.setattr(runner, "logged", attempt) - runner.repair("Example") - assert attempts == [["cx", "first", "exec"], ["cx", "third", "exec"]] - assert commits.call_count == 2 - assert runner.state["project"] is None - - -def test_all_accounts_failing_retains_checkpoint( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """Exhaustion waits for service retry instead of looping on the same account.""" - statuses = json.dumps([account("only", 0)]) - monkeypatch.setattr( - runner, "command", lambda *args: statuses if args[0] == "cx" else "head" - ) - monkeypatch.setattr(runner, "prompt", lambda project: "repair") - monkeypatch.setattr(runner, "logged", Mock(return_value=0)) - monkeypatch.setattr(runner, "commit_repairs", Mock()) - monkeypatch.setattr(runner, "build_project", Mock(return_value=False)) - with pytest.raises(RuntimeError, match="waterfall exhausted"): - runner.repair("Example") - assert runner.logged.call_count == 1 - assert json.loads(runner.state_path.read_text())["project"] == "Example" - - -def git(root: Path, *arguments: str) -> str: - """Run real local Git commands for ancestry and dirty-tree regressions.""" - return subprocess.check_output(["git", *arguments], cwd=root, text=True).strip() - - -def test_shallow_checkout_resumes_real_branch_with_common_ancestor( - tmp_path: Path, monkeypatch: pytest.MonkeyPatch -) -> None: - """Reproduce the old unrelated-histories failure and merge both lines of work.""" - source = tmp_path / "source" - source.mkdir() - git(source, "init", "-b", "main") - git(source, "config", "user.name", "Test") - git(source, "config", "user.email", "test@example.com") - (source / "base").write_text("base") - git(source, "add", ".") - git(source, "commit", "-m", "base") - git(source, "checkout", "-b", "bump/v4.35.0") - (source / "repair").write_text("existing repair") - git(source, "add", ".") - git(source, "commit", "-m", "existing repair") - repair = git(source, "rev-parse", "HEAD") - git(source, "checkout", "main") - (source / "upstream").write_text("new main work") - git(source, "add", ".") - git(source, "commit", "-m", "main moved") - upstream = git(source, "rev-parse", "HEAD") - remote = tmp_path / "remote.git" - git(tmp_path, "clone", "--bare", str(source), str(remote)) - monkeypatch.setattr(bump_vm, "REMOTE", remote.as_uri()) - root = tmp_path / "runtime" - root.mkdir() - git( - root, "clone", "--depth", "1", "--branch", "main", remote.as_uri(), "repository" - ) - worker = Runner(root) - worker.checkpoint(target="v4.35.0") - assert git(worker.repository, "rev-parse", "--is-shallow-repository") == "true" - worker.checkout() - monkeypatch.setattr(worker, "update_pins", Mock()) - original = worker.command - monkeypatch.setattr( - worker, - "command", - lambda *args, **kw: "" if args[0] == "lake" else original(*args, **kw), - ) - worker.prepare_branch("v4.35.0") - assert git(worker.repository, "rev-parse", "--is-shallow-repository") == "false" - git(worker.repository, "merge-base", "--is-ancestor", repair, "HEAD") - git(worker.repository, "merge-base", "--is-ancestor", upstream, "HEAD") - - -@pytest.mark.parametrize( - "path", [".github/workflows/check.yml", "LeanPool/Other/File.lean"] -) -def test_out_of_scope_repairs_are_preserved_but_never_committed( - runner: Runner, monkeypatch: pytest.MonkeyPatch, path: str -) -> None: - """A checkpoint cannot silently include unrelated agent edits.""" - monkeypatch.setattr(runner, "changed_paths", lambda: [path]) - commands = Mock() - monkeypatch.setattr(runner, "command", commands) - with pytest.raises(RuntimeError, match="unexpected path"): - runner.commit_repairs("Example") - commands.assert_not_called() - - -def test_build_success_with_warnings_still_needs_repair( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """Warnings remain a gate even when Lake returns zero.""" - (runner.root / "logs" / "build-Example.log").write_text( - "warning: unused simp argument" - ) - monkeypatch.setattr(runner, "logged", Mock(return_value=0)) - assert not runner.build_project("Example") - - -def test_all_existing_gates_run_and_failure_is_retained( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """The agent's exit status never substitutes for build and quality gates.""" - (runner.root / "logs" / "whole-pool.log").write_text("Build completed successfully") - calls = [] - - def logged(arguments: list[str], name: str) -> int: - calls.append(name) - return int(name == "gate-quality.log") - - monkeypatch.setattr(runner, "logged", logged) - results = runner.validate() - assert results == dict( - build=True, indexes=True, linter=True, style=True, quality=False - ) - assert len(calls) == 5 - assert runner.state_path.exists() - - -def test_pin_update_is_recovered_before_checkout_fetch( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """An interruption between rewriting pins and refreshing manifests is resumable.""" - runner.checkpoint(phase="pins") - runner.repository.mkdir() - calls = [] - - def command(*arguments: str) -> str: - calls.append(arguments) - if arguments[:3] == ("git", "remote", "get-url"): - return bump_vm.REMOTE - return "false" - - def update() -> None: - calls.append(("finish-pins",)) - - monkeypatch.setattr(runner, "command", command) - monkeypatch.setattr(runner, "changed_paths", lambda: []) - monkeypatch.setattr(runner, "update_pins", update) - runner.checkout() - finish = calls.index(("finish-pins",)) - fetch = next(i for i, call in enumerate(calls) if call[:2] == ("git", "fetch")) - assert finish < fetch - - -def test_unfinished_project_does_not_skip_other_repairs( - runner: Runner, monkeypatch: pytest.MonkeyPatch -) -> None: - """A difficult proof must not starve the rest of the migration.""" - for project in ("First", "Second"): - directory = runner.repository / "LeanPool" / project - directory.mkdir(parents=True) - (directory / "Imports.lean").write_text("-- example") - monkeypatch.setattr(runner, "checkout", Mock()) - monkeypatch.setattr(runner, "select_target", Mock(return_value="v4.35.0")) - monkeypatch.setattr(runner, "prepare_branch", Mock()) - monkeypatch.setattr(runner, "build_project", Mock(return_value=False)) - repairs = Mock(side_effect=[bump_vm.RepairIncompleteError("unfinished"), None]) - monkeypatch.setattr(runner, "repair", repairs) - monkeypatch.setattr(runner, "command", Mock()) - monkeypatch.setattr(runner, "validate", Mock(return_value={"build": False})) - monkeypatch.setattr(runner, "publish", Mock()) - with pytest.raises(RuntimeError, match="failing gates"): - runner.run(None, False, False) - assert [call.args[0] for call in repairs.call_args_list] == ["First", "Second"] - assert runner.state_path.exists() 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()) diff --git a/scripts/version-bump/README.md b/scripts/version-bump/README.md deleted file mode 100644 index e9bb55bd95..0000000000 --- a/scripts/version-bump/README.md +++ /dev/null @@ -1,101 +0,0 @@ -# Version bumps on the Lean VM - -The `lean-pool-version-bump.timer` user timer checks for new Mathlib releases, -including release candidates, at **05:23 UTC daily**. It also activates five -minutes after boot to resume interrupted work. The service runs entirely on -`lean`, independently of GitHub runners. It survives logout through user lingering. - -The controller resumes the oldest pending target, keeps a full-history private -checkout, merges current main without force-pushing, updates both sets of pins -and manifests, and fetches Mathlib's build cache. It builds each project's public -`Imports` module. Failing projects and warnings are repaired sequentially through -`cx`; each attempt probes quotas and picks the eligible account with the lowest -maximum used percentage across the reported windows. Thus the account with the -most remaining usable quota starts first, rather than the account resetting soonest. -Every eligible account is tried at most once per project per activation. Failed -attempts retain partial edits and refresh diagnostics for the next account. - -Repairs use `gpt-6.1-sol` / `xhigh`, with a workspace sandbox and CLI Lake/Lean. -Account configuration and MCP servers are not loaded into the agent. Subscription -credentials are supplied by `cx`; the runner clears inherited API credentials. -There is no Claude or API fallback, purchase, or reset-credit action. - -The service limits its process tree to 24 GiB and four CPU cores, with two Lean -threads, low scheduling weight and a 30 GiB free-space startup check. It neither -switches the shared `/data/lean-pool` checkout nor changes global account policy. -The account pool remains available to other services. - -## Deploy - -Use an authenticated VM operator account with GitHub push and PR access, elan, -Lake, uv, and the VM's existing `cx` installation. Enable user lingering if needed. -Install a trusted revision's Python package separately from the migration checkout: - -```sh -# From the trusted LeanPool checkout on the VM: -install -d -m 700 /data/lean-pool-bump/engine /data/lean-pool-bump/tmp -# Record the deployed commit outside the archive. -git rev-parse HEAD > /data/lean-pool-bump/engine-revision -# Do not replace the controller while its service is running. -git archive HEAD python scripts/version-bump | tar -x -C /data/lean-pool-bump/engine -cd /data/lean-pool-bump/engine/python -uv sync --locked -uv run python -m lean_pool.bump_vm --help -install -m 644 ../scripts/version-bump/*.service ../scripts/version-bump/*.timer \ - ~/.config/systemd/user/ -systemctl --user daemon-reload -systemctl --user enable --now lean-pool-version-bump.timer -systemctl --user start --no-block lean-pool-version-bump.service -``` - -During migration from the old GitHub workflow, disable `mathlib-bump.yml` before -starting the VM service, so two controllers cannot write the same branch. This -change removes that workflow from the repository; its historical logs remain. - -## Operate - -```sh -systemctl --user status lean-pool-version-bump.service -systemctl --user list-timers lean-pool-version-bump.timer -journalctl --user -u lean-pool-version-bump.service -n 30 -cat /data/lean-pool-bump/pending.json -# Manual check/resume, through the same process lock: -systemctl --user start --no-block lean-pool-version-bump.service -# Stop and disable future scheduling: -systemctl --user disable --now lean-pool-version-bump.timer -systemctl --user stop lean-pool-version-bump.service -``` - -With the service stopped, the installed module also accepts `--version v4.35.0`, -`--stable-only`, and `--probe-only`. Explicit targets must be published Mathlib -releases newer than main; a pending target cannot be silently replaced. Probe-only -runs still validate and publish a draft, but never invoke a repair account. -`LEAN_POOL_BUMP_MODEL` can override the repair model through the private optional -`/data/lean-pool-bump/environment` file. - -`pending.json`, the private checkout, logs and PR-body staging stay under -`/data/lean-pool-bump` with a private umask. A process lock prevents timer/manual -activation overlap. Systemd retries failures after an hour, while boot activation -resumes after restarts. Partial project edits and pin updates are checkpointed -before upstream merges. Unexpected edits, merge conflicts and racing pushes stop -without discarding changes; inspect and repair those explicitly. Do not delete a -pending checkpoint to force a fresh run. - -The controller commits and pushes repairs incrementally. An unfinished project does not skip other project repairs. A failed account -waterfall retains saved progress for the draft and leaves the checkpoint pending. -Whole-pool build, warning, index, linter, style and quality results are measured -outside the agent. Only passing every gate clears the checkpoint; even then the -PR remains a draft for statement review and normal current-head CI. - -## Tests - -```sh -cd python -uv run ruff check -uv run ruff format --check -uv run --group test pytest tests/test_bump.py tests/test_bump_vm.py -``` - -Tests reproduce resuming a shallow clone with a real diverged Git history, check -live quota ordering and reordering, preserve failed-attempt checkpoints, reject -out-of-scope edits, and enforce independent warning and quality validation. diff --git a/scripts/version-bump/lean-pool-version-bump.service b/scripts/version-bump/lean-pool-version-bump.service deleted file mode 100644 index bc5307fe1d..0000000000 --- a/scripts/version-bump/lean-pool-version-bump.service +++ /dev/null @@ -1,26 +0,0 @@ -[Unit] -Description=Resume Lean Pool version bumps on the Lean VM using cx -ConditionPathIsMountPoint=/data -Wants=network-online.target -After=network-online.target -StartLimitIntervalSec=0 - -[Service] -Type=oneshot -WorkingDirectory=/data/lean-pool-bump/engine/python -Environment=PATH=/home/vasil/.local/bin:/home/vasil/.elan/bin:/usr/local/bin:/usr/bin:/bin -Environment=TMPDIR=/data/lean-pool-bump/tmp -EnvironmentFile=-/data/lean-pool-bump/environment -ExecStart=/data/lean-pool-bump/engine/python/.venv/bin/python -m lean_pool.bump_vm -UMask=0077 -TimeoutStartSec=infinity -TimeoutStopSec=30s -KillMode=control-group -Restart=on-failure -RestartSec=1h -MemoryMax=24G -CPUQuota=400% -TasksMax=4096 -Nice=10 -CPUWeight=20 -IOWeight=20 diff --git a/scripts/version-bump/lean-pool-version-bump.timer b/scripts/version-bump/lean-pool-version-bump.timer deleted file mode 100644 index 6b7cadb432..0000000000 --- a/scripts/version-bump/lean-pool-version-bump.timer +++ /dev/null @@ -1,11 +0,0 @@ -[Unit] -Description=Check nightly for a new Lean/Mathlib release on the Lean VM - -[Timer] -OnCalendar=*-*-* 05:23:00 UTC -OnBootSec=5min -Persistent=true -Unit=lean-pool-version-bump.service - -[Install] -WantedBy=timers.target