From fe6f842ae51d7691bdafd9e5b4fab9e0f2905ab6 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 27 Jul 2026 22:59:33 -0700 Subject: [PATCH 1/2] Generate NOTICE from the registry; automate Mathlib bumps NOTICE had drifted badly: 75 of 141 projects had no attribution entry at all, which is an Apache-2.0 section 4(d) and MIT notice gap for every one of them. Rather than lint a hand-maintained file, generate it. - python/lean_pool/notice.py builds NOTICE from LeanPool/projects.yml (which already carries `license` and `source.github_repo` for all 141) plus NOTICE.extra.yml for the prose that cannot be derived: MIT copyright lines, relicensing statements, upstream citation requests. - notice.yml regenerates after merge, so drift cannot persist. It is not a PR gate on purpose: a content PR may not touch NOTICE under content-pr-guard, so gating there would be unsatisfiable. - Regenerating also corrected four stale upstream URLs whose repositories had been renamed (BrauerGroup_new, FLDutchmann/selberg-sieve4, RMT4, AxiomMath/fel-polynomial). mathlib-bump.yml migrates the pool to a new release in stages, only the last of which needs a human: detect a newer tag, move the four pins and plan shards, probe-build every project in parallel, triage the logs into a per-project breakage map, fan out one Claude repair job per broken project, then reassemble and open a draft PR. Pool projects never import each other, so a bump decomposes into independent per-project repairs; the assemble stage still rebuilds the whole pool, which is what catches the cross-project effects per-project repair cannot see. Repair jobs authenticate with a Claude subscription token and upload patches rather than pushing, so parallel jobs cannot race the branch. Probing is free and runs nightly regardless, so a release never lands as a surprise; `repair: auto` spends quota on final releases only. Co-Authored-By: Claude Opus 5 --- .claude/skills/version-bump-project/SKILL.md | 91 ++++ .github/BUMP_AUTOMATION.md | 117 +++++ .github/workflows/mathlib-bump.yml | 523 +++++++++++++++++++ .github/workflows/notice.yml | 60 +++ .github/workflows/python_ci.yml | 10 + NOTICE | 141 ++++- NOTICE.extra.yml | 133 +++++ python/lean_pool/bump.py | 312 +++++++++++ python/lean_pool/notice.py | 298 +++++++++++ python/tests/test_bump.py | 242 +++++++++ python/tests/test_notice.py | 150 ++++++ scripts/ci/bump-summary.py | 77 +++ 12 files changed, 2128 insertions(+), 26 deletions(-) create mode 100644 .claude/skills/version-bump-project/SKILL.md create mode 100644 .github/BUMP_AUTOMATION.md create mode 100644 .github/workflows/mathlib-bump.yml create mode 100644 .github/workflows/notice.yml create mode 100644 NOTICE.extra.yml create mode 100644 python/lean_pool/bump.py create mode 100644 python/lean_pool/notice.py create mode 100644 python/tests/test_bump.py create mode 100644 python/tests/test_notice.py create mode 100644 scripts/ci/bump-summary.py diff --git a/.claude/skills/version-bump-project/SKILL.md b/.claude/skills/version-bump-project/SKILL.md new file mode 100644 index 000000000..8225836e2 --- /dev/null +++ b/.claude/skills/version-bump-project/SKILL.md @@ -0,0 +1,91 @@ +--- +name: version-bump-project +description: Repair a SINGLE Lean Pool project's build against a new Lean/Mathlib release. Used by the mathlib-bump workflow's repair fan-out, one job per broken project. Use when asked to fix one project (not the whole pool) for a target version. +argument-hint: e.g. Polytopes v4.33.0-rc1 +--- + +# Repair one project for a new Mathlib release + +Fix **only** `LeanPool/` so that `lake build LeanPool.` +succeeds with **zero errors and zero warnings** under the target release. The +project and version are the arguments; if either is missing, stop and say so. + +This runs headless in CI with no reviewer present. The whole-pool equivalent is +the `version-bump` skill; this is its per-project unit of work. Pool projects +never import each other, so your project is independent of every other repair +running in parallel — never edit outside your project's directory. + +## Hard constraints (never violate) + +1. **No statement drops.** Every `theorem`/`lemma`/`def`/`instance`/`structure`/ + `inductive`/`class`/`abbrev` that exists now must still exist when you finish. + A statement that Mathlib has since absorbed is *still* not yours to delete — + leave it and note it in your summary; that call belongs to the reviewer. +2. **Change a statement only when the statement itself does not compile** under + the target (a renamed or removed Mathlib symbol in its type, or a name that + now collides with a new Mathlib declaration). Then make the *minimal* + meaning-preserving change — usually a rename that keeps the statement and + proof intact. Everything else: change proof bodies, tactics, and syntax only. + A `def` → `theorem` keyword change for a `Prop`-valued declaration flagged by + the `defProp` linter is allowed (same statement). +3. **Never** add `sorry`, `admit`, `native_decide`, a new `axiom`, `unsafe`, + `partial`, a `maxHeartbeats`/`maxRecDepth` increase, `set_option linter.* false`, + or any nolint waiver. **Fix the code, not the check.** These are enforced by + `python/lean_pool/quality.py` on the assembled branch, so adding one does not + get the bump merged — it just wastes the run. +4. **Never** edit `.github/`, `python/lean_pool/quality.py`, lint configs, + `lakefile.toml`'s `[leanOptions]`, `lean-toolchain`, or any file outside + `LeanPool//` (and `LeanPool/.lean` if it exists). +5. **Do not** commit, push, or open a PR. The workflow captures your working + tree as a patch and assembles it. Just leave the files fixed on disk. + +## Environment + +- The toolchain and Mathlib cache are already installed; `lake exe cache get` + has run. The pins are already at the target version. +- **CLI only — the lean-lsp MCP is not available.** Use: + - `lake build LeanPool.` to check your work (this is the ground truth) + - `lake env lean ` to check a single file quickly + - `rg .lake/packages/mathlib` to find what a symbol was renamed to +- `diagnostics.txt` in the working directory holds the exact errors this project + produced during the probe build. Start there. + +## Recipe + +1. **Read `diagnostics.txt`** and bucket the errors by root cause. Most projects + fail for one or two reasons repeated many times, not N independent reasons. +2. **Identify each root cause in Mathlib.** For a renamed lemma, `rg` the old + name in `.lake/packages/mathlib` — deprecation aliases usually carry a + `Use X instead` note naming the replacement. Trust the deprecation note over + a guess. +3. **Apply the minimal fix** across the project. Prefer a mechanical rename over + a proof rewrite; prefer a proof rewrite over any signature change. +4. **Rebuild** with `lake build LeanPool.` until there are no errors. +5. **Clear warnings too** — CI fails on any `warning:` line. Typical sources: + deprecation renames (do what the warning says), unused `simp` arguments, + no-op or never-executed tactics, and the `defProp` `def` → `theorem` case. +6. **Self-check before finishing:** + - `git diff` — is every changed file inside your project? + - Diff declaration *names* against the base revision. Anything present before + and missing now is a violation of constraint 1 unless it was a forced + rename you can justify. + - `git diff | rg 'sorry|admit|native_decide|maxHeartbeats|set_option linter'` + must be empty. + +## Report + +Finish with a short structured summary — it is the return value, not a message +to a human: + +``` +project: +status: clean | errors-remain | warnings-remain +root_causes: +statements_modified: +absorbed_by_mathlib: +notes: +``` + +If you cannot get the project clean, say so plainly in `status` and report what +remains. A partial, honest repair is useful; a green report that is not green is +not. Never disable a check to make the build pass. diff --git a/.github/BUMP_AUTOMATION.md b/.github/BUMP_AUTOMATION.md new file mode 100644 index 000000000..752d804c6 --- /dev/null +++ b/.github/BUMP_AUTOMATION.md @@ -0,0 +1,117 @@ +# Automated Mathlib bumps + +[`mathlib-bump.yml`](workflows/mathlib-bump.yml) migrates the whole pool to a +new Lean/Mathlib release. It runs nightly and needs a human only at the end, to +review the draft PR it opens. + +## What runs, and what it costs + +| Stage | What it does | Cost | +|---|---|---| +| `detect` | Compares the pinned release against Mathlib's tags | free | +| `probe` | Moves the pins, builds every project, buckets failures per project | free | +| `repair` | One Claude job per broken project, in parallel | subscription quota | +| `assemble` | Applies patches, rebuilds the pool, runs all four gates, opens a draft PR | free | + +"Free" means GitHub-hosted runner minutes, which are unmetered for public +repositories. Only `repair` spends anything, and only when something broke. + +The `probe` stage is worth having on its own: it runs whether or not a repair +follows, so the morning after a release you already know whether the bump costs +three projects or thirty. + +### Repair modes + +The `repair` input controls the fan-out: + +- `auto` (default) — repair final releases, report only on `-rc` tags. Mathlib + tags release candidates often; repairing each one would drain the token budget + for a version you are not adopting yet. +- `always` — repair whatever was detected, including candidates. +- `never` — probe only. Use this to size a bump before committing to it. + +## One-time setup + +### 1. Claude subscription token + +`repair` authenticates with a Claude subscription rather than API credits: + +```bash +claude setup-token +``` + +Store the result as a repository secret named `CLAUDE_CODE_OAUTH_TOKEN` +(Settings → Secrets and variables → Actions). Usage bills against the +subscription's quota, shared with terminal and web sessions. + +**These tokens expire.** When one does, `repair` fails with an authentication +error while `detect` and `probe` keep succeeding — so the nightly canary looks +healthy and only the repair half is dead. Two ways to handle it: + +- *Simplest:* re-run `claude setup-token` and update the secret when a repair + job fails to authenticate. The failure is loud and the fix takes a minute. +- *Unattended:* store a fine-grained PAT with `secrets: write` on this + repository and have the action refresh the stored token automatically. This + trades a long-lived PAT for never having to think about expiry. + +### 2. Pushing to branches (and to fork PRs) + +This workflow only ever pushes to `bump/*` branches in this repository, which +the default `GITHUB_TOKEN` can do. + +Any automation that needs to push to a **contributor's fork branch** — the +auto-rebase job for import PRs, for instance — cannot use `GITHUB_TOKEN`: it has +no write access to forks even when the PR has *Allow edits by maintainers* +checked. The fix is to authenticate as an app or a user instead: + +```yaml +- uses: actions/create-github-app-token@ + 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. Re-run just +the failed jobs from the run page, or fix that project by hand on the `bump/*` +branch. diff --git a/.github/workflows/mathlib-bump.yml b/.github/workflows/mathlib-bump.yml new file mode 100644 index 000000000..4e5516b9c --- /dev/null +++ b/.github/workflows/mathlib-bump.yml @@ -0,0 +1,523 @@ +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 + allow_prerelease: + description: "Consider -rc tags when auto-detecting" + required: false + default: false + type: boolean + repair: + description: "Run the Claude repair fan-out" + required: false + default: 'auto' + type: choice + options: ['auto', '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 }} + ALLOW_PRERELEASE: ${{ inputs.allow_prerelease }} + REPAIR_MODE: ${{ inputs.repair || 'auto' }} + run: | + set -euo pipefail + if [ -n "$REQUESTED" ]; then + target="$REQUESTED" + found=true + else + flags="" + if [ "$ALLOW_PRERELEASE" = "true" ]; then + flags="--allow-prerelease" + fi + # 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 + + # `auto` repairs final releases but only reports on candidates, so a + # steady stream of rc tags cannot quietly drain the token budget. + repair=false + case "$REPAIR_MODE" in + always) repair=true ;; + never) repair=false ;; + auto) case "$target" in *-rc*) repair=false ;; *) repair=true ;; esac ;; + esac + + { + 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 + + 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 + + - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Install Python tooling + run: cd python && uv sync --locked + + - 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 + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git checkout -B "$BRANCH" + 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 + git push --force 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, triage] + if: needs.detect.outputs.repair == 'true' && needs.triage.outputs.has_breakage == 'true' + runs-on: ubuntu-latest + name: Repair ${{ matrix.project }} + permissions: + contents: read + 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 }} + prompt: "/version-bump-project ${{ matrix.project }} ${{ needs.detect.outputs.target }}" + claude_args: >- + --max-turns 60 + --allowedTools "Bash,Read,Edit,Write,Grep,Glob" + + - name: Verify the repair + id: verify + env: + PROJECT: ${{ matrix.project }} + LEAN_NUM_THREADS: 2 + run: | + 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 + 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 + 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 + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + ref: ${{ needs.detect.outputs.branch }} + fetch-depth: 0 + + - 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: | + 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: | + 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.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 + git push origin "$BRANCH" + { + 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 diff --git a/.github/workflows/notice.yml b/.github/workflows/notice.yml new file mode 100644 index 000000000..e88547a9a --- /dev/null +++ b/.github/workflows/notice.yml @@ -0,0 +1,60 @@ +name: NOTICE + +# NOTICE is generated from LeanPool/projects.yml + NOTICE.extra.yml, so it can +# never drift out of step with the pool: every import PR that registers a +# project makes this job rewrite the attribution list on merge. +# +# The refresh commit below touches NOTICE only, which is NOT in the paths +# filter, so it cannot re-trigger this workflow (no commit loop). The same +# reason it is not a PR gate: a content PR may not touch NOTICE (it is +# non-content under content-pr-guard), so requiring an up-to-date NOTICE on +# the PR itself would be unsatisfiable. Regenerating after merge avoids that +# deadlock. Hand-edits to NOTICE in non-content PRs are still caught, by +# test_notice.py::test_repository_notice_is_current in Python CI. + +on: + push: + branches: + - main + paths: + - 'LeanPool/projects.yml' + - 'NOTICE.extra.yml' + - 'python/lean_pool/notice.py' + - '.github/workflows/notice.yml' + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: write + +jobs: + refresh: + runs-on: ubuntu-latest + name: Regenerate NOTICE + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + + - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Install dependencies + run: cd python && uv sync --locked + + - name: Regenerate NOTICE + run: cd python && uv run python -m lean_pool.notice --repo .. + + - name: Commit if changed + run: | + if git diff --quiet -- NOTICE; then + echo "NOTICE already up to date." + exit 0 + fi + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git add NOTICE + git commit -m "chore: regenerate NOTICE [skip ci]" + git push diff --git a/.github/workflows/python_ci.yml b/.github/workflows/python_ci.yml index 32eadbbed..f3ea4ba9f 100644 --- a/.github/workflows/python_ci.yml +++ b/.github/workflows/python_ci.yml @@ -6,12 +6,22 @@ on: - main paths: - 'python/**' + - 'NOTICE' + - 'NOTICE.extra.yml' - '.github/workflows/python_ci.yml' pull_request: branches: - main paths: - 'python/**' + # NOTICE is generated (notice.yml); the pytest suite asserts the + # committed file matches its inputs, which catches hand-edits to + # either. LeanPool/projects.yml is deliberately absent: it is a + # content path, and a content PR cannot also update NOTICE, so + # gating on it here would be unsatisfiable. notice.yml regenerates + # after merge instead. + - 'NOTICE' + - 'NOTICE.extra.yml' - '.github/workflows/python_ci.yml' workflow_dispatch: diff --git a/NOTICE b/NOTICE index aa67afb3c..77da6d8c8 100644 --- a/NOTICE +++ b/NOTICE @@ -12,6 +12,9 @@ recorded in the per-file headers and in LeanPool/projects.yml. This NOTICE file records, for every pooled project, the upstream repository it was imported from and the license under which it was originally published. +This file is generated by python/lean_pool/notice.py from LeanPool/projects.yml +and NOTICE.extra.yml. Do not edit it by hand -- edit those inputs instead. + -------------------------------------------------------------------------------- Projects originally licensed under the Apache License, Version 2.0 @@ -21,40 +24,114 @@ These projects were imported from repositories already licensed under the Apache License, Version 2.0, and are redistributed here under the same license. LeanPool/ABCExceptions https://github.com/b-mehta/ABC-Exceptions + LeanPool/AFormalizationOfBorelDeterminacyInLean + https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean LeanPool/AharoniKorman https://github.com/b-mehta/AharoniKorman LeanPool/AndersonConjecture https://github.com/frenzymath/Anderson-Conjecture LeanPool/Apportionment https://github.com/mdbrnowski/apportionmentlib LeanPool/ArchonFirstProofResults https://github.com/frenzymath/Archon-FirstProof-Results - LeanPool/BrauerGroupNew https://github.com/Whysoserioushah/BrauerGroup_new + LeanPool/BannaiBannaiStanton https://github.com/AntoineduFresne/Bannai-Bannai-Stanton_Theorem + LeanPool/BooleanIsoperimetry https://github.com/AlexeyMilovanov/BooleanIsoperimetry + LeanPool/BrauerGroupNew https://github.com/Whysoserioushah/BrauerGroup LeanPool/BruhatTits https://github.com/chrisflav/bruhat-tits + LeanPool/Burkholder https://github.com/SmaniaD/Burkholder + LeanPool/CencovPetz https://github.com/abenenson/cencov-petz + LeanPool/ChannelCapacity https://github.com/abenenson/channel-capacity + LeanPool/Chudnovsky https://github.com/ldct/lean-eval-chudnovsky + LeanPool/CircuitComplexity https://github.com/SamuelSchlesinger/circuit-complexity + LeanPool/Circuitlib https://github.com/matthunz/circuitlib + LeanPool/CompactSpectral https://github.com/abenenson/compact-spectral + LeanPool/Computability https://github.com/tannerduve/computability + LeanPool/ComputableReal https://github.com/Timeroot/computableReal + LeanPool/ConnesKreimer https://github.com/karlesmarin/connes-kreimer-lean + LeanPool/CramerWold https://github.com/Lemmy00/lean-pool + LeanPool/CriticalPortraits https://github.com/no-way-labs/lean-critical-portraits LeanPool/DemazureOperatorsLean https://github.com/bolito2/DemazureOperatorsLean + LeanPool/DemazureProduct https://github.com/npflueger/demazure + LeanPool/Desargues https://github.com/oneofvalts/desargues + LeanPool/DistanceGeometry https://github.com/lyfar/distance-geometry-lean + LeanPool/DomainTheory https://github.com/catskillsresearch/domain_theory LeanPool/Duality https://github.com/madvorak/duality LeanPool/EcTateLean https://github.com/KisaraBlue/ec-tate-lean + LeanPool/Egrs75 https://github.com/lyfar/egrs75-lean LeanPool/Erdos1196 https://github.com/math-inc/Erdos1196 + LeanPool/Erdos132N14 https://github.com/lyfar/erdos-132-moment-obstruction-lean + LeanPool/Erdos137 https://github.com/scottdhughes/erdos137 + LeanPool/Erdos346 https://github.com/KitaKen1/erdos346-ratio-limit-lean + LeanPool/Erdos367 https://github.com/scottdhughes/erdos367 + LeanPool/Erdos403 https://github.com/gotrevor/erdos-403 LeanPool/ErdosTuzaValtr https://github.com/jcpaik/erdos-tuza-valtr + LeanPool/EventStructures https://github.com/vikraman/event-structures LeanPool/Fineqs https://github.com/nasqret/fineqs - LeanPool/FormalLearningTheory https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel + LeanPool/FiveEighthsTheorem https://github.com/ldct/lean-monorepo + LeanPool/Flean https://github.com/josephmckinsey/flean LeanPool/FoZfc https://github.com/ishiut/fo_zfc + LeanPool/FormalLearningTheory https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel LeanPool/FriezePatterns https://github.com/Antoine-dSG/frieze_patterns + LeanPool/FrontierMathOpenHypergraphs + https://github.com/math-inc/FrontierMathOpen-Hypergraphs + LeanPool/FundamentalInequality https://github.com/linzialessandro/FundamentalInequality + LeanPool/GKPCarry https://github.com/lyfar/gkp-carry-lean + LeanPool/HadwigerNelsonBounds https://github.com/lyfar/hadwiger-nelson-bounds-lean + LeanPool/Incompleteness https://github.com/FormalizedFormalLogic/Incompleteness + LeanPool/IsTranscendentalPi https://github.com/samuelborza/IsTranscendentalPi LeanPool/Isoperimetric https://github.com/hojonathanho/isoperimetric + LeanPool/JohnsonLindenstraussLean https://github.com/claytomode/johnson-lindenstrauss-lean + LeanPool/KrafftSieve https://github.com/ElNando888/KrafftSieve + LeanPool/Lean4GlCoalgebras https://github.com/mgignoux/lean4-gl-coalgebras LeanPool/LeanBooleanfun https://github.com/roos-j/lean-booleanfun LeanPool/LeanComplexAnalysis https://github.com/seb488/LeanComplexAnalysis + LeanPool/LeanModelChecking https://github.com/kuruczgy/lean-model-checking LeanPool/LeanModularForms https://github.com/CBirkbeck/LeanModularForms LeanPool/LeanPolyABC https://github.com/seewoo5/lean-poly-abc + LeanPool/LeanQuantumAlg https://github.com/QudeLeap/Lean-QuantumAlg + LeanPool/LehmerE10 https://github.com/dillon-11/lehmer-E10 + LeanPool/Lentil https://github.com/verse-lab/Lentil LeanPool/LowDimSolvClassification https://github.com/LieLean/LowDimSolvClassification - LeanPool/Monsky https://github.com/dhyan-aranha/Monsky + LeanPool/MRiscX https://github.com/JulsDE/MRiscX + LeanPool/MinModulusUniqueMultisetSum + https://github.com/jarfo/min-modulus + LeanPool/MisereGames https://github.com/t4ccer/misere-games LeanPool/Monlib4 https://github.com/themathqueen/monlib4 + LeanPool/Monsky https://github.com/dhyan-aranha/Monsky + LeanPool/MoserLatticeColorings https://github.com/lyfar/moser-lattice-colorings-lean LeanPool/Neukirch https://github.com/jjdishere/neukirch + LeanPool/OSforGFF https://github.com/mrdouglasny/OSforGFF + LeanPool/OddPrimeValuationDistribution + https://github.com/lyfar/gkp-carry-lean LeanPool/OrderPQ https://github.com/wupr/order-p-q + LeanPool/PebblingLean https://github.com/pachterlab/P_2026_2 LeanPool/PentagonalNumberTheorem https://github.com/wwylele/PentagonalNumberTheorem + LeanPool/PhaseRetrieval https://github.com/susannabertolini/PhaseRetrieval LeanPool/PointwiseBirkhoff https://github.com/lua-vr/pointwise-birkhoff LeanPool/Polylean https://github.com/siddhartha-gadgil/Polylean - LeanPool/RiemannMappingTheorem https://github.com/vbeffara/rmt4 + LeanPool/PolynomialMethodRestrictedSums + https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes + LeanPool/Polytopes https://github.com/Jun2M/Main-theorem-of-polytopes + LeanPool/PumpingCfg https://github.com/AlexLoitzl/pumping_cfg + LeanPool/PythagoreanPolynomialParametrization + https://github.com/epfl-lara/AutoformalizedProjects + LeanPool/RamanujanNagell https://github.com/BarinderBanwait/ramanujan_nagell + LeanPool/RellichKondrachov https://github.com/abenenson/rellich-kondrachov + LeanPool/RiemannMappingTheorem https://github.com/vbeffara/RMT4 + LeanPool/RootSystem https://github.com/Antoine-dSG/root_system + LeanPool/RungeKuttaOrderConditions https://github.com/karlesmarin/runge-kutta-order-conditions-lean LeanPool/Rupert https://github.com/dwrensha/Rupert.lean + LeanPool/Sabidussi https://github.com/gexahedron/sabidussi-lean LeanPool/SardMoreira https://github.com/urkud/SardMoreira - LeanPool/SelbergSieve4 https://github.com/FLDutchmann/selberg-sieve4 + LeanPool/SelbergSieve4 https://github.com/amellendijk/selberg-sieve4 + LeanPool/SemicircleCheck https://github.com/Wondermonger-daydreaming/semicircle-catalan LeanPool/Sensitivity https://github.com/SamuelSchlesinger/sensitivity-conjecture + LeanPool/SetTheory https://github.com/znssong/SetTheory + LeanPool/SingularModuli https://github.com/ElodinLaarz/lean-thesis + LeanPool/SpectralPositivity https://github.com/mrdouglasny/spectral-positivity LeanPool/SumsThreeSquares https://github.com/pitmonticone/SumsThreeSquares + LeanPool/Sundogcert https://github.com/humiliati/sundogcert + LeanPool/SyntheticEuclid4 https://github.com/ah1112/synthetic_euclid_4 + LeanPool/ThreeGap https://github.com/ElVec1o/five-distance-sharp + LeanPool/Turan3 https://github.com/ro-gut/turan3 + LeanPool/UnconditionalSchauderBasis + https://github.com/SmaniaD/UnconditionalSchauderBasis LeanPool/VirasoroProject https://github.com/kkytola/VirasoroProject LeanPool/WhiteheadTheorem https://github.com/jzxia/WhiteheadTheorem LeanPool/ZFLean https://github.com/VTrelat/ZFLean @@ -72,9 +149,11 @@ redistributed here under the Apache License, Version 2.0. As the MIT License requires, the original copyright notices are preserved below, together with the MIT permission notice that follows them. + LeanPool/AgreeToDisagree https://github.com/AxiomMath/AgreeToDisagree LeanPool/ArtinWedderburn https://github.com/JobPetrovcic/ArtinWedderburn Copyright (c) 2024 Job Petrovčič + LeanPool/Biswal https://github.com/AxiomMath/Biswal LeanPool/Brouwer https://github.com/math-xmum/Brouwer Copyright (c) 2025 Math_XMUM @@ -90,7 +169,7 @@ MIT permission notice that follows them. LeanPool/FactorizationSystems https://github.com/ivankobe/FactorizationSystems Copyright (c) 2024 ivankobe - LeanPool/FelConjecture https://github.com/axiommath/fel-polynomial + LeanPool/FelConjecture https://github.com/AxiomMath/fel-polynomial Copyright (c) 2026 Axiom Math LeanPool/FormalizationOfBoundedArithmetic @@ -99,12 +178,22 @@ MIT permission notice that follows them. template text "Copyright (c) [year] [fullname]"; the repository owner of record is "ruplet". + LeanPool/HSDInteriorPointLP https://github.com/makoto-yamashita/proof-on-a-homogeneous-self-dual-interior-point-method-for-linear-programming + LeanPool/KaltonRoberts https://github.com/boonsuan/KaltonRoberts + LeanPool/Kuramoto https://github.com/velvetmonkey/kuramoto-lean LeanPool/LatticeTriangle https://github.com/AxiomMath/lattice-triangle Copyright (c) 2026 Axiom Math LeanPool/Lean4Itree https://github.com/mit-plv/lean4-itree Copyright (c) 2025 the choice-tree authors (see the AUTHORS file) + LeanPool/LeanStationaryHarmonicMaps + https://github.com/BrookWW/LeanStationaryHarmonicMaps + LeanPool/PCFTheory https://github.com/YnirPaz/PCF-Theory + The upstream MIT LICENSE file contains no copyright line; the repository + owner of record is "YnirPaz". + + LeanPool/PLAcceleratedNesterovLean https://github.com/M1ngXU/PL-Accelerated-Nesterov-Lean LeanPool/PartialCombinatoryAlgebras https://github.com/andrejbauer/partial-combinatory-algebras Copyright (c) 2024 Andrej Bauer @@ -112,10 +201,6 @@ MIT permission notice that follows them. LeanPool/PartialRegularity https://github.com/AxiomMath/partial-regularity Copyright (c) 2026 Axiom Math - LeanPool/PCFTheory https://github.com/YnirPaz/PCF-Theory - The upstream MIT LICENSE file contains no copyright line; the repository - owner of record is "YnirPaz". - LeanPool/PolyaEnumerationTheorem https://github.com/Luka-O/polya-enumeration-theorem Copyright (c) 2024 Luka-O @@ -139,15 +224,17 @@ MIT permission notice that follows them. "Copyright (c) 2026" with no name; the repository owner of record is "SamuelSchlesinger". - LeanPool/SteinhausThreeGap https://github.com/dkunert/three-gap-theorem-lean - Copyright (c) 2026 Dirk Kunert - LeanPool/SpecialNumbers https://github.com/provables/special-numbers Copyright (c) 2024 Walter Moreira, Joe Stubbs + LeanPool/SteinhausThreeGap https://github.com/dkunert/three-gap-theorem-lean + Copyright (c) 2026 Dirk Kunert + LeanPool/TwoColoringOneRound https://github.com/suomela/2-coloring-1-round Copyright (c) 2026 Jukka Suomela + LeanPool/ZetaH123 https://github.com/AxiomMath/zeta-h123 + MIT License -- the following permission notice applies to every project listed in this section: @@ -174,16 +261,18 @@ MIT permission notice that follows them. Projects relicensed by their original author -------------------------------------------------------------------------------- +These projects were relicensed by their sole author before import. + LeanPool/Clawristotle https://github.com/Vilin97/Clawristotle + LeanPool/ForwardEuler https://github.com/Vilin97/forward_euler + Originally distributed without a license file, then placed under the + Apache License, Version 2.0, by its sole author. + LeanPool/GrothendieckVanishing https://github.com/Vilin97/Clawristotle Originally distributed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International license, then relicensed under the Apache License, Version 2.0, by its sole author. - LeanPool/ForwardEuler https://github.com/Vilin97/forward_euler - Originally distributed without a license file, then placed under the - Apache License, Version 2.0, by its sole author. - -------------------------------------------------------------------------------- Additional upstream attribution and citation notices @@ -194,6 +283,15 @@ files or LICENSE addenda. Only each project's Apache-2.0 Lean sources were imported here; these notes preserve attribution and citation requests made by the original authors. + LeanPool/FormalLearningTheory https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel + The upstream LICENSE appends a citation request. The original author asks + that publications, software, or derivative works built on this + formalization cite: + + Gupta, D. (2026). Formal Learning Theory Kernel: Lean4 Formalization + of the Fundamental Theorem of Statistical Learning. + https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel + LeanPool/ZhangYeungInequality https://github.com/cboone/zhang-yeung-inequality The upstream repository ships a NOTICE file (Apache License, Version 2.0, Section 4(d)). Its attribution notice reads: @@ -204,12 +302,3 @@ the original authors. The upstream additionally carries CC-BY-4.0 prose, CC-BY-SA-4.0 for its code of conduct, CC0-1.0 for generated files, and bundled reference materials under a custom license; none of those files were imported. - - LeanPool/FormalLearningTheory https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel - The upstream LICENSE appends a citation request. The original author asks - that publications, software, or derivative works built on this - formalization cite: - - Gupta, D. (2026). Formal Learning Theory Kernel: Lean4 Formalization - of the Fundamental Theorem of Statistical Learning. - https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel diff --git a/NOTICE.extra.yml b/NOTICE.extra.yml new file mode 100644 index 000000000..e58465b7c --- /dev/null +++ b/NOTICE.extra.yml @@ -0,0 +1,133 @@ +# Per-project prose for the generated NOTICE file, keyed by the project's +# directory under LeanPool/. Everything else in NOTICE (which project, which +# upstream repository, which license section) is derived from +# LeanPool/projects.yml, so only text that cannot be derived belongs here. +# +# Recognised keys, all optional: +# note Text shown under the project in its license section. For MIT +# projects this is the upstream copyright line, which the MIT +# License requires be preserved. +# relicensed Moves the project into the "relicensed by their original +# author" section, with this text as its explanation. An empty +# string lists the project there without a note of its own +# (used when a following entry carries the shared explanation). +# attribution Adds the project to the "additional upstream attribution" +# section, reproducing an upstream NOTICE or citation request. +# +# Regenerate NOTICE after editing: +# cd python && uv run python -m lean_pool.notice --repo .. + +ArtinWedderburn: + note: Copyright (c) 2024 Job Petrovčič + +Brouwer: + note: Copyright (c) 2025 Math_XMUM + +Clawristotle: + # The shared relicensing note sits on GrothendieckVanishing, which follows + # this entry -- both projects live in the same upstream repository. + relicensed: "" + +CutAndProject: + note: Copyright (c) 2026 Dirk Kunert + +DeadEnds: + note: Copyright (c) 2026 Axiom Math + +DirectedTopologyLean4: + note: Copyright 2023 Dominique Lawson + +FactorizationSystems: + note: Copyright (c) 2024 ivankobe + +FelConjecture: + note: Copyright (c) 2026 Axiom Math + +FormalLearningTheory: + attribution: |- + The upstream LICENSE appends a citation request. The original author asks + that publications, software, or derivative works built on this + formalization cite: + + Gupta, D. (2026). Formal Learning Theory Kernel: Lean4 Formalization + of the Fundamental Theorem of Statistical Learning. + https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel + +FormalizationOfBoundedArithmetic: + note: |- + The upstream MIT LICENSE file leaves the copyright line as the unfilled + template text "Copyright (c) [year] [fullname]"; the repository owner of + record is "ruplet". + +ForwardEuler: + relicensed: |- + Originally distributed without a license file, then placed under the + Apache License, Version 2.0, by its sole author. + +GrothendieckVanishing: + relicensed: |- + Originally distributed under the Creative Commons + Attribution-NonCommercial-ShareAlike 4.0 International license, then + relicensed under the Apache License, Version 2.0, by its sole author. + +LatticeTriangle: + note: Copyright (c) 2026 Axiom Math + +Lean4Itree: + note: Copyright (c) 2025 the choice-tree authors (see the AUTHORS file) + +PCFTheory: + note: |- + The upstream MIT LICENSE file contains no copyright line; the repository + owner of record is "YnirPaz". + +PartialCombinatoryAlgebras: + note: Copyright (c) 2024 Andrej Bauer + +PartialRegularity: + note: Copyright (c) 2026 Axiom Math + +PolyaEnumerationTheorem: + note: Copyright (c) 2024 Luka-O + +QuasiBorelSpaces: + note: Copyright (c) 2025 Anthony Vandikas, Kiarash Sotoudeh + +RamanujanTauMissesPrimes: + note: Copyright (c) 2026 Axiom Math + +Redhill: + note: Copyright (c) 2026 Jeremy Tan / Parcly Taxel + +RlTheoryInLean: + note: Copyright (c) 2025 Shangtong Zhang + +SemicircleLaw: + note: Copyright (c) 2025 FredRaj3 + +Shannon1948Formalization: + note: |- + The upstream MIT LICENSE file gives the copyright line as + "Copyright (c) 2026" with no name; the repository owner of record is + "SamuelSchlesinger". + +SpecialNumbers: + note: Copyright (c) 2024 Walter Moreira, Joe Stubbs + +SteinhausThreeGap: + note: Copyright (c) 2026 Dirk Kunert + +TwoColoringOneRound: + note: Copyright (c) 2026 Jukka Suomela + +ZhangYeungInequality: + attribution: |- + The upstream repository ships a NOTICE file (Apache License, Version 2.0, + Section 4(d)). Its attribution notice reads: + + The Zhang-Yeung Inequality + Copyright 2026 Christopher Boone + + The upstream additionally carries CC-BY-4.0 prose, CC-BY-SA-4.0 for its + code of conduct, CC0-1.0 for generated files, and bundled reference + materials under a custom license; none of those files were imported. diff --git a/python/lean_pool/bump.py b/python/lean_pool/bump.py new file mode 100644 index 000000000..ccd361df6 --- /dev/null +++ b/python/lean_pool/bump.py @@ -0,0 +1,312 @@ +"""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], *, allow_prerelease: bool +) -> list[str]: + """Return tags strictly newer than ``current``, oldest first.""" + threshold = version_key(current) + candidates = [ + tag + for tag in tags + if version_key(tag) > threshold and (allow_prerelease or not 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 next 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, allow_prerelease=args.allow_prerelease) + 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( + "--allow-prerelease", + action="store_true", + help="also consider -rc tags (default: final releases only)", + ) + 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/notice.py b/python/lean_pool/notice.py new file mode 100644 index 000000000..f0dc636e9 --- /dev/null +++ b/python/lean_pool/notice.py @@ -0,0 +1,298 @@ +"""Generate the repository ``NOTICE`` file from the project registry. + +``NOTICE`` carries the third-party attribution that Apache-2.0 section 4(d) +and the MIT License require for every pooled project. It used to be +maintained by hand, which silently drifted: by the time this generator was +written, 75 of 141 projects had no entry at all. + +Everything the list sections need already lives in ``LeanPool/projects.yml`` +(each card declares ``license`` and ``source.github_repo``), so those are +derived rather than typed. The prose that cannot be derived -- upstream MIT +copyright lines, relicensing statements, and reproduced upstream NOTICE text +-- lives in ``NOTICE.extra.yml``, keyed by project directory. + +Deliberately kept out of ``projects.yml``: that file is *content* under +``.github/workflows/content-pr-guard.yml``, so a PR may not touch it +alongside infrastructure. Keeping the prose in a separate infra-side file +lets NOTICE regeneration stay a non-content change. + +Usage:: + + python -m lean_pool.notice --repo .. # rewrite NOTICE + python -m lean_pool.notice --repo .. --check # exit 1 if stale +""" + +from __future__ import annotations + +import argparse +import logging +import sys +from pathlib import Path +from typing import Any + +import yaml + +logger = logging.getLogger(__name__) + +# Column at which an entry's URL starts, matching the hand-written original. +URL_COLUMN = 37 +# Indent for a project's prose note. +NOTE_INDENT = " " * 6 +RULE = "-" * 80 + +HEADER = """\ +Lean Pool +========= + +Copyright the Lean Pool contributors and the respective project authors. + +Lean Pool is licensed under the Apache License, Version 2.0. See the LICENSE +file for the full license text. + +Lean Pool is an aggregation of third-party Lean 4 formalizations. Each project +under LeanPool/ is the work of its original authors, who retain copyright as +recorded in the per-file headers and in LeanPool/projects.yml. This NOTICE file +records, for every pooled project, the upstream repository it was imported from +and the license under which it was originally published. + +This file is generated by python/lean_pool/notice.py from LeanPool/projects.yml +and NOTICE.extra.yml. Do not edit it by hand -- edit those inputs instead.""" + +APACHE_PREAMBLE = """\ +These projects were imported from repositories already licensed under the +Apache License, Version 2.0, and are redistributed here under the same license.""" + +MIT_PREAMBLE = """\ +These projects were imported from repositories licensed under the MIT License. +The MIT License grants the right to sublicense, so these projects are +redistributed here under the Apache License, Version 2.0. As the MIT License +requires, the original copyright notices are preserved below, together with the +MIT permission notice that follows them.""" + +MIT_PERMISSION_NOTICE = """\ + MIT License -- the following permission notice applies to every project + listed in this section: + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE.""" + +ATTRIBUTION_PREAMBLE = """\ +The following notices are reproduced from the upstream repositories' own NOTICE +files or LICENSE addenda. Only each project's Apache-2.0 Lean sources were +imported here; these notes preserve attribution and citation requests made by +the original authors.""" + + +def _load_yaml(path: Path) -> Any: + """Parse a YAML file, returning ``None`` when it does not exist.""" + if not path.is_file(): + return None + return yaml.safe_load(path.read_text(encoding="utf-8")) + + +def load_projects(root: Path) -> list[dict[str, Any]]: + """Read the project cards from ``LeanPool/projects.yml``.""" + data = _load_yaml(root / "LeanPool" / "projects.yml") + if isinstance(data, dict): + data = data.get("projects", []) + return list(data or []) + + +def load_extra(root: Path) -> dict[str, dict[str, str]]: + """Read the per-project prose notes from ``NOTICE.extra.yml``.""" + data = _load_yaml(root / "NOTICE.extra.yml") or {} + return {str(key): dict(value or {}) for key, value in data.items()} + + +def project_directory(project: dict[str, Any]) -> str: + """Return a card's directory under ``LeanPool/`` (from its entry module).""" + parts = str(project.get("entry_module", "")).split(".") + return parts[1] if len(parts) > 1 else "" + + +def repository_url(project: dict[str, Any]) -> str: + """Return the upstream GitHub URL a card was imported from.""" + repo = (project.get("source") or {}).get("github_repo", "") + return f"https://github.com/{repo}" if repo else "" + + +def render_entry(directory: str, url: str) -> list[str]: + """Render one ``LeanPool/ `` line, wrapping long names. + + A directory name long enough to reach the URL column pushes the URL onto + its own continuation line, aligned to the same column. + """ + label = f" LeanPool/{directory}" + padding = URL_COLUMN - len(label) + if padding >= 1: + return [f"{label}{' ' * padding}{url}"] + return [label, f"{' ' * URL_COLUMN}{url}"] + + +def render_note(note: str) -> list[str]: + """Indent a prose note under its entry, preserving internal blank lines.""" + return [f"{NOTE_INDENT}{line}".rstrip() for line in note.splitlines()] + + +def _section(title: str, preamble: str, body: list[str]) -> list[str]: + """Assemble a titled section; returns no lines when the body is empty.""" + if not body: + return [] + return [RULE, title, RULE, "", preamble, "", *body] + + +def _entries( + projects: list[dict[str, Any]], + extra: dict[str, dict[str, str]], + *, + note_key: str | None, +) -> list[str]: + """Render entry lines (with optional notes) for the given cards.""" + lines: list[str] = [] + for project in projects: + directory = project_directory(project) + lines.extend(render_entry(directory, repository_url(project))) + note = extra.get(directory, {}).get(note_key) if note_key else None + if note: + lines.extend(render_note(note)) + lines.append("") + # A trailing blank line belongs to the section separator, not the entry. + while lines and lines[-1] == "": + lines.pop() + return lines + + +def render(projects: list[dict[str, Any]], extra: dict[str, dict[str, str]]) -> str: + """Render the complete NOTICE text.""" + ordered = sorted(projects, key=project_directory) + relicensed = [ + p for p in ordered if "relicensed" in extra.get(project_directory(p), {}) + ] + relicensed_dirs = {project_directory(p) for p in relicensed} + apache = [ + p + for p in ordered + if p.get("license") == "Apache-2.0" + and project_directory(p) not in relicensed_dirs + ] + mit = [ + p + for p in ordered + if p.get("license") == "MIT" and project_directory(p) not in relicensed_dirs + ] + attributed = [ + p for p in ordered if extra.get(project_directory(p), {}).get("attribution") + ] + + lines: list[str] = [HEADER, "", ""] + lines += _section( + "Projects originally licensed under the Apache License, Version 2.0", + APACHE_PREAMBLE, + _entries(apache, extra, note_key="note"), + ) + lines += ["", ""] + mit_body = _entries(mit, extra, note_key="note") + if mit_body: + mit_body += ["", MIT_PERMISSION_NOTICE] + lines += _section( + "Projects originally licensed under the MIT License", MIT_PREAMBLE, mit_body + ) + if relicensed: + lines += ["", ""] + lines += _section( + "Projects relicensed by their original author", + "These projects were relicensed by their sole author before import.", + _entries(relicensed, extra, note_key="relicensed"), + ) + if attributed: + lines += ["", ""] + lines += _section( + "Additional upstream attribution and citation notices", + ATTRIBUTION_PREAMBLE, + _entries(attributed, extra, note_key="attribution"), + ) + return "\n".join(lines).rstrip("\n") + "\n" + + +def unregistered_notes( + projects: list[dict[str, Any]], extra: dict[str, dict[str, str]] +) -> list[str]: + """Return ``NOTICE.extra.yml`` keys that match no project directory. + + A stale key means a note silently stopped being emitted -- usually a + project renamed or removed without its note following. + """ + known = {project_directory(p) for p in projects} + return sorted(key for key in extra if key not in known) + + +def build(root: Path) -> str: + """Render NOTICE for the repository at ``root``.""" + projects = load_projects(root) + extra = load_extra(root) + stale = unregistered_notes(projects, extra) + if stale: + raise SystemExit( + "NOTICE.extra.yml has notes for unknown projects: " + ", ".join(stale) + ) + return render(projects, extra) + + +def _parse_args(argv: list[str] | None) -> argparse.Namespace: + """Parse command-line arguments.""" + parser = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + parser.add_argument( + "--repo", type=Path, default=Path("."), help="repository root (default: .)" + ) + parser.add_argument( + "--check", + action="store_true", + help="do not write; exit 1 if NOTICE is out of date", + ) + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + """Regenerate or verify NOTICE; return a process exit code.""" + logging.basicConfig(level=logging.INFO, format="%(message)s") + args = _parse_args(argv) + root = args.repo.resolve() + expected = build(root) + path = root / "NOTICE" + current = path.read_text(encoding="utf-8") if path.is_file() else "" + + if args.check: + if current == expected: + logger.info("NOTICE is up to date.") + return 0 + logger.error( + "NOTICE is out of date. Regenerate it with:\n" + " cd python && uv run python -m lean_pool.notice --repo .." + ) + return 1 + + if current == expected: + logger.info("NOTICE is already up to date.") + return 0 + path.write_text(expected, encoding="utf-8") + logger.info("Wrote %s", path) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/python/tests/test_bump.py b/python/tests/test_bump.py new file mode 100644 index 000000000..2da177df1 --- /dev/null +++ b/python/tests/test_bump.py @@ -0,0 +1,242 @@ +"""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_newer_versions_skips_prereleases_by_default() -> None: + """Prereleases are opt-in, so nightly runs do not chase every rc.""" + tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1", "v4.33.0"] + assert newer_versions("v4.32.0-rc1", tags, allow_prerelease=False) == [ + "v4.32.0", + "v4.33.0", + ] + assert newer_versions("v4.32.0-rc1", tags, allow_prerelease=True) == [ + "v4.32.0", + "v4.33.0-rc1", + "v4.33.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"], allow_prerelease=True) == [] + ) + + +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"], + allow_prerelease=False, + ) == ["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_notice.py b/python/tests/test_notice.py new file mode 100644 index 000000000..1f44608da --- /dev/null +++ b/python/tests/test_notice.py @@ -0,0 +1,150 @@ +"""Tests for NOTICE generation from the project registry.""" + +from __future__ import annotations + +from pathlib import Path + +import pytest + +from lean_pool.notice import ( + URL_COLUMN, + build, + main, + project_directory, + render_entry, + repository_url, + unregistered_notes, +) + +PROJECTS_YML = """projects: + - slug: alpha + entry_module: LeanPool.Alpha + license: Apache-2.0 + source: + github_repo: someone/alpha + - slug: beta + entry_module: LeanPool.Beta + license: MIT + source: + github_repo: someone/beta +""" + + +def _write_repo(root: Path, extra: str = "") -> None: + """Create a minimal repository with two projects, one Apache and one MIT.""" + pool = root / "LeanPool" + pool.mkdir() + (pool / "projects.yml").write_text(PROJECTS_YML) + if extra: + (root / "NOTICE.extra.yml").write_text(extra) + + +def test_every_project_appears(tmp_path: Path) -> None: + """Both projects are listed, each under its own license section.""" + _write_repo(tmp_path) + text = build(tmp_path) + assert " LeanPool/Alpha" in text + assert " LeanPool/Beta" in text + assert "https://github.com/someone/alpha" in text + assert text.index("Apache License, Version 2.0\n---") < text.index("LeanPool/Alpha") + assert text.index("MIT License\n---") < text.index("LeanPool/Beta") + + +def test_mit_permission_notice_present(tmp_path: Path) -> None: + """The MIT section carries the permission notice the license requires.""" + _write_repo(tmp_path) + assert "Permission is hereby granted, free of charge" in build(tmp_path) + + +def test_note_is_rendered_under_its_entry(tmp_path: Path) -> None: + """A project's ``note`` appears indented directly beneath its entry.""" + _write_repo(tmp_path, "Beta:\n note: Copyright (c) 2026 Someone\n") + lines = build(tmp_path).splitlines() + index = next(i for i, line in enumerate(lines) if "LeanPool/Beta" in line) + assert lines[index + 1] == " Copyright (c) 2026 Someone" + + +def test_relicensed_moves_out_of_license_section(tmp_path: Path) -> None: + """A relicensed project is listed only in the relicensing section.""" + _write_repo(tmp_path, "Alpha:\n relicensed: Relicensed by its author.\n") + text = build(tmp_path) + assert text.count("LeanPool/Alpha") == 1 + assert "Projects relicensed by their original author" in text + assert text.index("relicensed by their original author") < text.index( + "LeanPool/Alpha" + ) + + +def test_attribution_adds_a_second_listing(tmp_path: Path) -> None: + """An attributed project stays in its license section and is repeated.""" + _write_repo(tmp_path, "Alpha:\n attribution: Upstream asks for a citation.\n") + text = build(tmp_path) + assert text.count("LeanPool/Alpha") == 2 + assert "Upstream asks for a citation." in text + + +def test_empty_relicensed_note_lists_without_prose(tmp_path: Path) -> None: + """An empty ``relicensed`` value lists the project with no note of its own.""" + _write_repo(tmp_path, 'Alpha:\n relicensed: ""\n') + text = build(tmp_path) + assert "Projects relicensed by their original author" in text + assert text.count("LeanPool/Alpha") == 1 + + +def test_long_directory_wraps_the_url(tmp_path: Path) -> None: + """A name that reaches the URL column pushes the URL to its own line.""" + short = render_entry("Alpha", "https://example.com") + assert len(short) == 1 + assert short[0].index("https://") == URL_COLUMN + + long = render_entry("A" * 40, "https://example.com") + assert len(long) == 2 + assert long[1].index("https://") == URL_COLUMN + + +def test_stale_extra_key_is_rejected(tmp_path: Path) -> None: + """A note for a project that no longer exists fails loudly.""" + _write_repo(tmp_path, "Gamma:\n note: Copyright (c) 2026 Ghost\n") + with pytest.raises(SystemExit, match="Gamma"): + build(tmp_path) + + +def test_unregistered_notes_lists_orphans() -> None: + """Orphan detection compares note keys against project directories.""" + projects = [{"entry_module": "LeanPool.Alpha"}] + assert unregistered_notes(projects, {"Alpha": {}, "Ghost": {}}) == ["Ghost"] + + +def test_project_directory_and_url_helpers() -> None: + """Directory and URL are derived from the card, not typed by hand.""" + card = {"entry_module": "LeanPool.Alpha", "source": {"github_repo": "who/what"}} + assert project_directory(card) == "Alpha" + assert repository_url(card) == "https://github.com/who/what" + assert repository_url({"entry_module": "LeanPool.Alpha"}) == "" + + +def test_check_mode_detects_drift(tmp_path: Path) -> None: + """``--check`` passes on a generated file and fails once it drifts.""" + _write_repo(tmp_path) + assert main(["--repo", str(tmp_path)]) == 0 + assert main(["--repo", str(tmp_path), "--check"]) == 0 + + (tmp_path / "NOTICE").write_text("hand-edited\n") + assert main(["--repo", str(tmp_path), "--check"]) == 1 + # Check mode must not repair the file it is checking. + assert (tmp_path / "NOTICE").read_text() == "hand-edited\n" + + +def test_generation_is_idempotent(tmp_path: Path) -> None: + """Regenerating an up-to-date NOTICE leaves it byte-identical.""" + _write_repo(tmp_path) + main(["--repo", str(tmp_path)]) + first = (tmp_path / "NOTICE").read_text() + main(["--repo", str(tmp_path)]) + assert (tmp_path / "NOTICE").read_text() == first + + +def test_repository_notice_is_current() -> None: + """The committed NOTICE matches what the generator produces.""" + root = Path(__file__).resolve().parents[2] + assert (root / "NOTICE").read_text(encoding="utf-8") == build(root) diff --git a/scripts/ci/bump-summary.py b/scripts/ci/bump-summary.py new file mode 100644 index 000000000..2c2928df1 --- /dev/null +++ b/scripts/ci/bump-summary.py @@ -0,0 +1,77 @@ +"""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()) From 81b51a5da8587d46e5ba72d78060ee23b514246d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 27 Jul 2026 23:10:51 -0700 Subject: [PATCH 2/2] Bump to the newest release; auto-rebase open PRs on merge Bumps now target the newest available release, candidates included: mid release-cycle that is what "latest Lean and Mathlib" means, and the pool tracks the latest. `detect` therefore reports v4.33.0-rc1 rather than v4.32.1, `--stable-only` opts out, and the repair fan-out no longer skips rc targets (it would otherwise never have run). auto-rebase.yml keeps the import queue mergeable without hand-holding. When a content PR lands, every other open import PR conflicts in exactly two files, and in both the resolution is mechanical: - LeanPool.lean is a sorted list of imports regenerated from the file tree. It reproduces the committed 2,885-line index byte-for-byte, so the job needs no Lean toolchain and runs in seconds. - LeanPool/projects.yml takes the merged base's registry plus the cards the branch adds, moved as verbatim text blocks. Round-tripping 141 cards through a YAML dumper would reformat every one and bury the real change. Any other conflicted path is a genuine content overlap: the merge is abandoned and the PR labelled needs-manual-rebase rather than guessed at. Verified against real pull request data by simulating #285 landing, which makes #287 conflict exactly as predicted. The regenerated index is the exact sorted union of both branches' modules with no conflict markers, and the merged registry is 143 cards with no duplicates, valid YAML, required fields intact, and the 142 pre-existing cards byte-identical. Pushing to a fork branch needs REBASE_TOKEN (a GitHub App installation token or a PAT); GITHUB_TOKEN has no write access to forks even with "Allow edits by maintainers" set. Without it, fork PRs are labelled instead of rebased and same-repo PRs still work. Co-Authored-By: Claude Opus 5 --- .github/workflows/auto-rebase.yml | 203 +++++++++++++++++++++++++++++ .github/workflows/mathlib-bump.yml | 30 ++--- python/lean_pool/bump.py | 21 ++- python/lean_pool/rebase.py | 166 +++++++++++++++++++++++ python/tests/test_bump.py | 29 ++--- python/tests/test_rebase.py | 181 +++++++++++++++++++++++++ 6 files changed, 591 insertions(+), 39 deletions(-) create mode 100644 .github/workflows/auto-rebase.yml create mode 100644 python/lean_pool/rebase.py create mode 100644 python/tests/test_rebase.py diff --git a/.github/workflows/auto-rebase.yml b/.github/workflows/auto-rebase.yml new file mode 100644 index 000000000..91f594f4f --- /dev/null +++ b/.github/workflows/auto-rebase.yml @@ -0,0 +1,203 @@ +name: Auto-rebase open PRs + +# When a content PR merges, every other open import PR conflicts -- always in +# the same two files, and always mechanically: +# +# LeanPool.lean a sorted list of imports, regenerated from the file +# tree (no Lean toolchain needed, so this job is fast) +# LeanPool/projects.yml the merged base's registry plus the cards this +# branch adds, moved as verbatim text blocks +# +# Any other conflicted path is a real content overlap: the merge is abandoned +# and the PR labelled `needs-manual-rebase`. The resolution logic lives in +# python/lean_pool/rebase.py, under test; this workflow only drives it. +# +# Pushing to a contributor's fork needs more than GITHUB_TOKEN, which has no +# write access to forks even when "Allow edits by maintainers" is set. Set +# REBASE_TOKEN (a GitHub App installation token or a PAT with `repo`) to cover +# fork PRs; without it they are labelled instead of rebased, and same-repo PRs +# still work. An App token is preferable: its pushes re-trigger `pull_request` +# CI, which GITHUB_TOKEN pushes do not. + +on: + push: + branches: + - main + paths: + - 'LeanPool/**' + - 'LeanPool.lean' + workflow_dispatch: + +concurrency: + # Serialised: two runs rebasing the same PR would race on its branch. + group: auto-rebase + cancel-in-progress: false + +permissions: + contents: read + pull-requests: write + +jobs: + list: + runs-on: ubuntu-latest + name: List open PRs + outputs: + pulls: ${{ steps.list.outputs.pulls }} + any: ${{ steps.list.outputs.any }} + steps: + - name: Collect open pull requests + id: list + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + REPO: ${{ github.repository }} + run: | + set -euo pipefail + pulls="$(gh pr list --repo "$REPO" --state open --limit 100 \ + --json number,headRefName,headRepository,headRepositoryOwner,isCrossRepository,labels \ + --jq '[.[] + | select([.labels[].name] | index("needs-manual-rebase") | not) + | {number, branch: .headRefName, + repo: "\(.headRepositoryOwner.login)/\(.headRepository.name)", + fork: .isCrossRepository}]')" + echo "pulls=$pulls" >> "$GITHUB_OUTPUT" + if [ "$(echo "$pulls" | python3 -c 'import json,sys; print(len(json.load(sys.stdin)))')" = "0" ]; then + echo "any=false" >> "$GITHUB_OUTPUT" + else + echo "any=true" >> "$GITHUB_OUTPUT" + fi + echo "$pulls" + + rebase: + needs: list + if: needs.list.outputs.any == 'true' + runs-on: ubuntu-latest + name: Rebase #${{ matrix.pull.number }} + strategy: + fail-fast: false + max-parallel: 1 + matrix: + pull: ${{ fromJSON(needs.list.outputs.pulls) }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + fetch-depth: 0 + token: ${{ secrets.REBASE_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: Check we can push to this branch + id: capable + env: + FORK: ${{ matrix.pull.fork }} + HAS_TOKEN: ${{ secrets.REBASE_TOKEN != '' }} + run: | + set -euo pipefail + if [ "$FORK" = "true" ] && [ "$HAS_TOKEN" != "true" ]; then + echo "REBASE_TOKEN is not set; cannot push to a fork branch." + echo "ok=false" >> "$GITHUB_OUTPUT" + else + echo "ok=true" >> "$GITHUB_OUTPUT" + fi + + - name: Merge main and resolve mechanically + id: rebase + if: steps.capable.outputs.ok == 'true' + env: + NUMBER: ${{ matrix.pull.number }} + BRANCH: ${{ matrix.pull.branch }} + HEAD_REPO: ${{ matrix.pull.repo }} + TOKEN: ${{ secrets.REBASE_TOKEN || secrets.GITHUB_TOKEN }} + run: | + set -euo pipefail + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + + remote="https://x-access-token:$TOKEN@github.com/$HEAD_REPO" + git remote add head "$remote" + git fetch head "$BRANCH" + git checkout -B "pr-$NUMBER" "head/$BRANCH" + + if git merge --no-edit origin/main; then + echo "Merged cleanly." + if git diff --quiet "head/$BRANCH" HEAD; then + echo "result=up-to-date" >> "$GITHUB_OUTPUT" + else + echo "result=merged" >> "$GITHUB_OUTPUT" + fi + else + git diff --name-only --diff-filter=U > conflicts.txt + echo "Conflicts:"; cat conflicts.txt + if ! (cd python && uv run python -m lean_pool.rebase resolvable \ + --conflicts ../conflicts.txt); then + git merge --abort + echo "result=manual" >> "$GITHUB_OUTPUT" + exit 0 + fi + + merge_base="$(git merge-base "head/$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 "head/$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 + # Regenerated from the file tree, so the conflict markers sitting + # in the checked-out index file are irrelevant. + (cd python && uv run python -m lean_pool.rebase index --repo ..) + git add LeanPool.lean + fi + + if git diff --name-only --diff-filter=U | grep -q .; then + git merge --abort + echo "result=manual" >> "$GITHUB_OUTPUT" + exit 0 + fi + git commit --no-edit + echo "result=resolved" >> "$GITHUB_OUTPUT" + fi + + # The index must be correct even when it did not conflict: main may + # have added modules this branch has never seen. + (cd python && uv run python -m lean_pool.rebase index --repo ..) + if ! git diff --quiet -- LeanPool.lean; then + git add LeanPool.lean + git commit -m "Regenerate the module index" + echo "result=resolved" >> "$GITHUB_OUTPUT" + fi + + - name: Push the rebase + if: steps.rebase.outputs.result == 'merged' || steps.rebase.outputs.result == 'resolved' + env: + NUMBER: ${{ matrix.pull.number }} + BRANCH: ${{ matrix.pull.branch }} + run: git push head "pr-$NUMBER:$BRANCH" + + - name: Flag PRs that need a human + if: steps.rebase.outputs.result == 'manual' || steps.capable.outputs.ok == 'false' + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + REPO: ${{ github.repository }} + NUMBER: ${{ matrix.pull.number }} + REASON: ${{ steps.capable.outputs.ok == 'false' && 'no-token' || 'conflict' }} + run: | + set -euo pipefail + gh pr edit "$NUMBER" --repo "$REPO" --add-label needs-manual-rebase || true + if [ "$REASON" = "no-token" ]; then + body="This PR is from a fork and \`REBASE_TOKEN\` is not configured, so + auto-rebase cannot push to its branch. See + \`.github/workflows/auto-rebase.yml\` for the token setup." + else + body="Auto-rebase stopped: this PR conflicts with \`main\` outside the two + mechanically resolvable files (\`LeanPool.lean\`, \`LeanPool/projects.yml\`), + so the overlap needs a human. Remove the \`needs-manual-rebase\` label once + resolved to re-enable automatic updates." + fi + gh pr comment "$NUMBER" --repo "$REPO" --body "$body" || true diff --git a/.github/workflows/mathlib-bump.yml b/.github/workflows/mathlib-bump.yml index 4e5516b9c..a61ea1ffb 100644 --- a/.github/workflows/mathlib-bump.yml +++ b/.github/workflows/mathlib-bump.yml @@ -34,17 +34,17 @@ on: description: "Target release (e.g. v4.33.0-rc1); blank = auto-detect" required: false type: string - allow_prerelease: - description: "Consider -rc tags when auto-detecting" + 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: 'auto' + default: 'always' type: choice - options: ['auto', 'always', 'never'] + options: ['always', 'never'] concurrency: # One bump at a time: two concurrent bumps would fight over the branch. @@ -79,8 +79,8 @@ jobs: id: detect env: REQUESTED: ${{ inputs.version }} - ALLOW_PRERELEASE: ${{ inputs.allow_prerelease }} - REPAIR_MODE: ${{ inputs.repair || 'auto' }} + STABLE_ONLY: ${{ inputs.stable_only }} + REPAIR_MODE: ${{ inputs.repair || 'always' }} run: | set -euo pipefail if [ -n "$REQUESTED" ]; then @@ -88,9 +88,11 @@ jobs: found=true else flags="" - if [ "$ALLOW_PRERELEASE" = "true" ]; then - flags="--allow-prerelease" + 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" @@ -98,14 +100,10 @@ jobs: found="$(echo "$result" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["found"]).lower())')" fi - # `auto` repairs final releases but only reports on candidates, so a - # steady stream of rc tags cannot quietly drain the token budget. - repair=false - case "$REPAIR_MODE" in - always) repair=true ;; - never) repair=false ;; - auto) case "$target" in *-rc*) repair=false ;; *) repair=true ;; esac ;; - esac + repair=true + if [ "$REPAIR_MODE" = "never" ]; then + repair=false + fi { echo "found=$found" diff --git a/python/lean_pool/bump.py b/python/lean_pool/bump.py index ccd361df6..fc04531e8 100644 --- a/python/lean_pool/bump.py +++ b/python/lean_pool/bump.py @@ -91,14 +91,19 @@ def remote_tags(remote: str = MATHLIB_REMOTE) -> list[str]: def newer_versions( - current: str, tags: list[str], *, allow_prerelease: bool + current: str, tags: list[str], *, stable_only: bool = False ) -> list[str]: - """Return tags strictly newer than ``current``, oldest first.""" + """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 (allow_prerelease or not is_prerelease(tag)) + if version_key(tag) > threshold and not (stable_only and is_prerelease(tag)) ] return sorted(set(candidates), key=version_key) @@ -234,11 +239,13 @@ def build_report(log: str) -> dict[str, object]: def _command_detect(args: argparse.Namespace) -> int: - """Print the next Mathlib release to bump to, if any.""" + """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, allow_prerelease=args.allow_prerelease) + 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, @@ -282,9 +289,9 @@ def _parse_args(argv: list[str] | None) -> argparse.Namespace: detect.add_argument("--repo", type=Path, default=Path("."), help="repository root") detect.add_argument("--remote", default=MATHLIB_REMOTE) detect.add_argument( - "--allow-prerelease", + "--stable-only", action="store_true", - help="also consider -rc tags (default: final releases only)", + help="ignore -rc tags (default: bump to the newest release of any kind)", ) detect.set_defaults(func=_command_detect) diff --git a/python/lean_pool/rebase.py b/python/lean_pool/rebase.py new file mode 100644 index 000000000..47b6baa14 --- /dev/null +++ b/python/lean_pool/rebase.py @@ -0,0 +1,166 @@ +"""Deterministic conflict resolution for import pull requests. + +Backs ``.github/workflows/auto-rebase.yml``. When a pull request merges, +every other open import PR conflicts in exactly two files, and in both the +resolution is mechanical rather than editorial: + +``LeanPool.lean`` + The ``mk_all`` index is a sorted list of ``import LeanPool.X`` lines, one + per Lean file in the tree, so it is regenerated rather than merged -- + and, because it is derived purely from the file tree, without needing a + Lean toolchain. + +``LeanPool/projects.yml`` + Take the merged base's registry and re-append the cards this branch + added. Cards are moved as verbatim text blocks, never re-serialised: + round-tripping 141 cards through a YAML dumper would reformat every one + of them and bury the real change. + +Anything else in conflict is a genuine content overlap and is left alone for +a human. This module only computes file contents; the workflow decides what +to do with them. +""" + +from __future__ import annotations + +import argparse +import logging +import sys +from pathlib import Path + +logger = logging.getLogger(__name__) + +REGISTRY = "LeanPool/projects.yml" +INDEX = "LeanPool.lean" +CARD_PREFIX = " - slug: " +# The only conflicts this module claims to resolve. +RESOLVABLE = frozenset({INDEX, REGISTRY}) + + +def render_index(root: Path) -> str: + """Regenerate the ``mk_all`` index from the Lean files on disk.""" + pool = root / "LeanPool" + modules = sorted( + "LeanPool." + + str(path.relative_to(pool)).removesuffix(".lean").replace("/", ".") + for path in pool.rglob("*.lean") + ) + return "".join(f"import {module}\n" for module in modules) + + +def split_cards(text: str) -> tuple[str, list[tuple[str, str]]]: + """Split a registry into its header and its cards, as verbatim text. + + Returns ``(header, [(slug, block)])`` where concatenating the header and + every block reproduces ``text`` exactly. + """ + lines = text.splitlines(keepends=True) + starts = [i for i, line in enumerate(lines) if line.startswith(CARD_PREFIX)] + if not starts: + return text, [] + header = "".join(lines[: starts[0]]) + cards: list[tuple[str, str]] = [] + for index, start in enumerate(starts): + end = starts[index + 1] if index + 1 < len(starts) else len(lines) + slug = lines[start][len(CARD_PREFIX) :].strip() + cards.append((slug, "".join(lines[start:end]))) + return header, cards + + +def merge_registry(base: str, ours: str, theirs: str) -> str: + """Three-way merge the registry by card. + + ``ours`` is the updated base branch, ``theirs`` the pull request. The + result is ``ours`` plus every card the pull request added, appended in + the order the pull request had them. Cards are never reordered or + reformatted, so the diff shows only the additions. + """ + base_slugs = {slug for slug, _ in split_cards(base)[1]} + header, our_cards = split_cards(ours) + our_slugs = {slug for slug, _ in our_cards} + + added = [ + (slug, block) + for slug, block in split_cards(theirs)[1] + if slug not in base_slugs and slug not in our_slugs + ] + if not added: + return ours + + merged = header + "".join(block for _, block in our_cards) + # A registry whose last card lacks a trailing newline would otherwise + # run into the first appended card. + if merged and not merged.endswith("\n"): + merged += "\n" + return merged + "".join(block for _, block in added) + + +def resolvable(conflicts: list[str]) -> bool: + """Whether every conflicted path is one this module can resolve.""" + return bool(conflicts) and set(conflicts) <= RESOLVABLE + + +def _command_index(args: argparse.Namespace) -> int: + """Rewrite the index from the working tree.""" + root = args.repo.resolve() + (root / INDEX).write_text(render_index(root), encoding="utf-8") + logger.info("regenerated %s", INDEX) + return 0 + + +def _command_registry(args: argparse.Namespace) -> int: + """Three-way merge the registry from three revisions on disk.""" + merged = merge_registry( + args.base.read_text(encoding="utf-8"), + args.ours.read_text(encoding="utf-8"), + args.theirs.read_text(encoding="utf-8"), + ) + (args.repo.resolve() / REGISTRY).write_text(merged, encoding="utf-8") + logger.info("merged %s", REGISTRY) + return 0 + + +def _command_resolvable(args: argparse.Namespace) -> int: + """Exit 0 when every conflicted path is mechanically resolvable.""" + conflicts = [line.strip() for line in args.conflicts.read_text().splitlines()] + conflicts = [path for path in conflicts if path] + if resolvable(conflicts): + logger.info("all conflicts are mechanically resolvable") + return 0 + unresolvable = sorted(set(conflicts) - RESOLVABLE) + logger.error("conflicts need a human: %s", ", ".join(unresolvable) or "none") + return 1 + + +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) + + index = subparsers.add_parser("index", help="regenerate LeanPool.lean") + index.add_argument("--repo", type=Path, default=Path(".")) + index.set_defaults(func=_command_index) + + registry = subparsers.add_parser("registry", help="three-way merge projects.yml") + registry.add_argument("--repo", type=Path, default=Path(".")) + registry.add_argument("--base", type=Path, required=True) + registry.add_argument("--ours", type=Path, required=True) + registry.add_argument("--theirs", type=Path, required=True) + registry.set_defaults(func=_command_registry) + + check = subparsers.add_parser("resolvable", help="are these conflicts mechanical?") + check.add_argument("--conflicts", type=Path, required=True) + check.set_defaults(func=_command_resolvable) + + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + """Dispatch a subcommand; return a process exit code.""" + logging.basicConfig(level=logging.INFO, format="%(message)s") + args = _parse_args(argv) + return int(args.func(args)) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/python/tests/test_bump.py b/python/tests/test_bump.py index 2da177df1..82e627bc2 100644 --- a/python/tests/test_bump.py +++ b/python/tests/test_bump.py @@ -76,25 +76,22 @@ def test_is_prerelease() -> None: assert not is_prerelease("v4.33.0") -def test_newer_versions_skips_prereleases_by_default() -> None: - """Prereleases are opt-in, so nightly runs do not chase every rc.""" - tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1", "v4.33.0"] - assert newer_versions("v4.32.0-rc1", tags, allow_prerelease=False) == [ - "v4.32.0", - "v4.33.0", - ] - assert newer_versions("v4.32.0-rc1", tags, allow_prerelease=True) == [ - "v4.32.0", - "v4.33.0-rc1", - "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"], allow_prerelease=True) == [] - ) + assert newer_versions("v4.33.0", ["v4.32.0", "v4.33.0"], stable_only=False) == [] def test_newer_versions_ignores_unparseable_tags() -> None: @@ -103,7 +100,7 @@ def test_newer_versions_ignores_unparseable_tags() -> None: assert newer_versions( "v4.32.0", [t for t in tags if t != "nightly-2026-07-01"], - allow_prerelease=False, + stable_only=True, ) == ["v4.33.0"] diff --git a/python/tests/test_rebase.py b/python/tests/test_rebase.py new file mode 100644 index 000000000..4b719d14d --- /dev/null +++ b/python/tests/test_rebase.py @@ -0,0 +1,181 @@ +"""Tests for deterministic import-PR conflict resolution.""" + +from __future__ import annotations + +from pathlib import Path + +from lean_pool.rebase import ( + main, + merge_registry, + render_index, + resolvable, + split_cards, +) + +BASE = """projects: + - slug: alpha + title: Alpha + entry_module: LeanPool.Alpha + - slug: beta + title: Beta + entry_module: LeanPool.Beta +""" + +# main advanced: an import PR for `gamma` merged ahead of ours. +OURS = """projects: + - slug: alpha + title: Alpha + entry_module: LeanPool.Alpha + - slug: beta + title: Beta + entry_module: LeanPool.Beta + - slug: gamma + title: Gamma + entry_module: LeanPool.Gamma +""" + +# our PR, branched from BASE, adding `delta`. +THEIRS = """projects: + - slug: alpha + title: Alpha + entry_module: LeanPool.Alpha + - slug: beta + title: Beta + entry_module: LeanPool.Beta + - slug: delta + title: Delta + entry_module: LeanPool.Delta +""" + + +# --------------------------------------------------------------------------- # +# Index regeneration +# --------------------------------------------------------------------------- # +def test_render_index_is_sorted_imports(tmp_path: Path) -> None: + """The index lists every Lean file in the tree, sorted.""" + pool = tmp_path / "LeanPool" + (pool / "Beta").mkdir(parents=True) + (pool / "Alpha.lean").write_text("") + (pool / "Beta" / "Core.lean").write_text("") + (pool / "Beta.lean").write_text("") + assert render_index(tmp_path) == ( + "import LeanPool.Alpha\nimport LeanPool.Beta\nimport LeanPool.Beta.Core\n" + ) + + +def test_render_index_ignores_non_lean_files(tmp_path: Path) -> None: + """projects.yml sits inside LeanPool/ and is not a module.""" + pool = tmp_path / "LeanPool" + pool.mkdir(parents=True) + (pool / "Alpha.lean").write_text("") + (pool / "projects.yml").write_text("projects: []\n") + assert render_index(tmp_path) == "import LeanPool.Alpha\n" + + +def test_render_index_reproduces_the_committed_index() -> None: + """The real index regenerates byte-for-byte, so no Lean build is needed.""" + root = Path(__file__).resolve().parents[2] + assert render_index(root) == (root / "LeanPool.lean").read_text(encoding="utf-8") + + +# --------------------------------------------------------------------------- # +# Registry merging +# --------------------------------------------------------------------------- # +def test_split_cards_round_trips() -> None: + """Header plus every card block reproduces the file exactly.""" + header, cards = split_cards(OURS) + assert [slug for slug, _ in cards] == ["alpha", "beta", "gamma"] + assert header + "".join(block for _, block in cards) == OURS + + +def test_merge_keeps_both_additions() -> None: + """The merged registry has the card main added and the card we added.""" + merged = merge_registry(BASE, OURS, THEIRS) + slugs = [slug for slug, _ in split_cards(merged)[1]] + assert slugs == ["alpha", "beta", "gamma", "delta"] + + +def test_merge_preserves_existing_cards_verbatim() -> None: + """Untouched cards are copied as text, never re-serialised.""" + merged = merge_registry(BASE, OURS, THEIRS) + assert merged.startswith(OURS) + assert " - slug: delta\n title: Delta\n" in merged + + +def test_merge_is_a_noop_when_the_branch_added_nothing() -> None: + """A branch that only edits existing cards yields the base unchanged.""" + assert merge_registry(BASE, OURS, BASE) == OURS + + +def test_merge_does_not_duplicate_an_already_merged_card() -> None: + """If our card reached the base first, it is not appended twice.""" + merged = merge_registry(BASE, THEIRS, THEIRS) + assert [slug for slug, _ in split_cards(merged)[1]] == ["alpha", "beta", "delta"] + + +def test_merge_separates_appended_cards(tmp_path: Path) -> None: + """A base missing its trailing newline still yields valid YAML.""" + merged = merge_registry(BASE, OURS.rstrip("\n"), THEIRS) + assert "entry_module: LeanPool.Gamma\n - slug: delta" in merged + + +def test_merge_result_parses_as_yaml() -> None: + """The text-level merge must still produce loadable YAML.""" + import yaml + + data = yaml.safe_load(merge_registry(BASE, OURS, THEIRS)) + assert [card["slug"] for card in data["projects"]] == [ + "alpha", + "beta", + "gamma", + "delta", + ] + + +# --------------------------------------------------------------------------- # +# Scope +# --------------------------------------------------------------------------- # +def test_resolvable_only_covers_the_two_mechanical_files() -> None: + """A conflict in real Lean content is not ours to resolve.""" + assert resolvable(["LeanPool.lean"]) + assert resolvable(["LeanPool.lean", "LeanPool/projects.yml"]) + assert not resolvable(["LeanPool/Alpha/Core.lean"]) + assert not resolvable(["LeanPool.lean", "LeanPool/Alpha/Core.lean"]) + assert not resolvable([]) + + +def test_resolvable_command_exit_codes(tmp_path: Path) -> None: + """The workflow branches on this command's exit code.""" + good = tmp_path / "good.txt" + good.write_text("LeanPool.lean\nLeanPool/projects.yml\n") + assert main(["resolvable", "--conflicts", str(good)]) == 0 + + bad = tmp_path / "bad.txt" + bad.write_text("LeanPool.lean\nLeanPool/Alpha/Core.lean\n") + assert main(["resolvable", "--conflicts", str(bad)]) == 1 + + +def test_registry_command_writes_the_merge(tmp_path: Path) -> None: + """The registry subcommand writes the merged file into the repo.""" + (tmp_path / "LeanPool").mkdir() + (tmp_path / "LeanPool" / "projects.yml").write_text(OURS) + for name, text in (("base", BASE), ("ours", OURS), ("theirs", THEIRS)): + (tmp_path / name).write_text(text) + assert ( + main( + [ + "registry", + "--repo", + str(tmp_path), + "--base", + str(tmp_path / "base"), + "--ours", + str(tmp_path / "ours"), + "--theirs", + str(tmp_path / "theirs"), + ] + ) + == 0 + ) + merged = (tmp_path / "LeanPool" / "projects.yml").read_text() + assert "delta" in merged and "gamma" in merged