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/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 new file mode 100644 index 000000000..a61ea1ffb --- /dev/null +++ b/.github/workflows/mathlib-bump.yml @@ -0,0 +1,521 @@ +name: Mathlib Bump + +# Automated whole-pool migration to a new Lean/Mathlib release, in stages where +# only the last one needs a human: +# +# detect Is there a newer release than the pinned one? (free, no LLM) +# pin Move the four version pins, refresh the manifests, push a +# bump/ branch, and plan the build shards. (free) +# probe Build every project across parallel shards, one project at a +# time so each diagnostic is attributable. (free) +# triage Merge the shard logs into a per-project breakage map, which +# becomes the repair fan-out's job matrix. (free) +# repair One Claude job per broken project, in parallel. Pool projects +# never import each other, so a bump decomposes into independent +# per-project repairs. (subscription quota) +# assemble Apply every patch, rebuild the WHOLE pool, run all four gates, +# open a DRAFT pull request. (free) +# +# Agents propose, deterministic gates dispose: nothing here can merge itself, +# and `assemble` re-runs the same checks CI would. Repair jobs upload patches +# as artifacts rather than pushing, so parallel jobs cannot race the branch. +# +# Auth: `CLAUDE_CODE_OAUTH_TOKEN` is a Claude subscription token generated +# locally with `claude setup-token`; usage bills against the subscription +# rather than API credits. See .github/BUMP_AUTOMATION.md for setup and costs. + +on: + schedule: + # Off-peak, and off the :00 mark where every scheduled workflow piles up. + - cron: '23 5 * * *' + workflow_dispatch: + inputs: + version: + description: "Target release (e.g. v4.33.0-rc1); blank = auto-detect" + required: false + type: string + stable_only: + description: "Ignore -rc tags (default: bump to the newest release of any kind)" + required: false + default: false + type: boolean + repair: + description: "Run the Claude repair fan-out" + required: false + default: 'always' + type: choice + options: ['always', 'never'] + +concurrency: + # One bump at a time: two concurrent bumps would fight over the branch. + group: mathlib-bump + cancel-in-progress: false + +permissions: + contents: read + +jobs: + detect: + runs-on: ubuntu-latest + name: Detect new release + outputs: + found: ${{ steps.detect.outputs.found }} + target: ${{ steps.detect.outputs.target }} + branch: ${{ steps.detect.outputs.branch }} + repair: ${{ steps.detect.outputs.repair }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + persist-credentials: false + + - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Install Python tooling + run: cd python && uv sync --locked + + - name: Resolve target version + id: detect + env: + REQUESTED: ${{ inputs.version }} + STABLE_ONLY: ${{ inputs.stable_only }} + REPAIR_MODE: ${{ inputs.repair || 'always' }} + run: | + set -euo pipefail + if [ -n "$REQUESTED" ]; then + target="$REQUESTED" + found=true + else + flags="" + if [ "$STABLE_ONLY" = "true" ]; then + flags="--stable-only" + fi + # Release candidates count: the pool tracks the newest Lean and + # Mathlib, which mid-cycle means the latest rc. + # shellcheck disable=SC2086 + result="$(cd python && uv run python -m lean_pool.bump detect --repo .. $flags)" + echo "$result" + target="$(echo "$result" | python3 -c 'import json,sys; print(json.load(sys.stdin)["target"])')" + found="$(echo "$result" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["found"]).lower())')" + fi + + repair=true + if [ "$REPAIR_MODE" = "never" ]; then + repair=false + fi + + { + echo "found=$found" + echo "target=$target" + echo "branch=bump/$target" + echo "repair=$repair" + } >> "$GITHUB_OUTPUT" + + - name: Summary + env: + FOUND: ${{ steps.detect.outputs.found }} + TARGET: ${{ steps.detect.outputs.target }} + REPAIR: ${{ steps.detect.outputs.repair }} + run: | + if [ "$FOUND" != "true" ]; then + echo "Pool is up to date; nothing to bump." >> "$GITHUB_STEP_SUMMARY" + else + echo "Target: **$TARGET** (repair fan-out: $REPAIR)" >> "$GITHUB_STEP_SUMMARY" + fi + + 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..fc04531e8 --- /dev/null +++ b/python/lean_pool/bump.py @@ -0,0 +1,319 @@ +"""Version-detection, pin-rewriting, and build-log triage for Mathlib bumps. + +Backs ``.github/workflows/mathlib-bump.yml``. The workflow keeps only +orchestration; every decision that benefits from being testable lives here: + +* ``detect`` -- is there a newer Mathlib release than the one pinned? +* ``pin`` -- rewrite the four version pins to a target release. +* ``report`` -- turn a ``lake build`` log into a per-project breakage map, + which becomes the repair fan-out's job matrix. + +Pool projects never import each other, so a bump decomposes into one +independent repair per broken project. ``report`` is what makes that +decomposition explicit. + +Usage:: + + python -m lean_pool.bump detect --repo .. [--allow-prerelease] + python -m lean_pool.bump pin --repo .. --version v4.33.0-rc1 + python -m lean_pool.bump report --repo .. --log build.log +""" + +from __future__ import annotations + +import argparse +import json +import logging +import re +import subprocess +import sys +from dataclasses import dataclass, field +from pathlib import Path + +logger = logging.getLogger(__name__) + +MATHLIB_REMOTE = "https://github.com/leanprover-community/mathlib4" + +# Release tags shared by Lean, Mathlib, and doc-gen4: v4.33.0, v4.33.0-rc1. +VERSION_RE = re.compile(r"^v(\d+)\.(\d+)\.(\d+)(?:-rc(\d+))?$") +# Diagnostics are `error: ::: `; lake may prefix the +# path with `./`. Progress lines instead name the module: `Building LeanPool.X`. +DIAGNOSTIC_RE = re.compile(r"^(?:.*?\s)?(error|warning):\s*(.*)$") +PATH_PROJECT_RE = re.compile(r"LeanPool/(\w+)") +MODULE_PROJECT_RE = re.compile(r"LeanPool\.(\w+)") +BUILDING_RE = re.compile(r"Building\s+(LeanPool\.\S+)") + +# How many diagnostic lines to carry into the repair prompt per project. +MAX_EXCERPT_LINES = 40 + + +def version_key(tag: str) -> tuple[int, int, int, int, int]: + """Sort key for a release tag; a final release outranks its candidates.""" + match = VERSION_RE.match(tag) + if match is None: + raise ValueError(f"not a release tag: {tag}") + major, minor, patch, candidate = match.groups() + # `is_final` = 1 sorts v4.33.0 above v4.33.0-rc9. + is_final = 0 if candidate else 1 + return (int(major), int(minor), int(patch), is_final, int(candidate or 0)) + + +def is_prerelease(tag: str) -> bool: + """Whether ``tag`` names a release candidate rather than a final release.""" + match = VERSION_RE.match(tag) + return bool(match and match.group(4)) + + +def current_version(root: Path) -> str: + """Read the Mathlib release currently pinned in ``lakefile.toml``.""" + text = (root / "lakefile.toml").read_text(encoding="utf-8") + # The manifest lists several packages; only Mathlib's rev is a release tag. + for match in re.finditer(r'rev\s*=\s*"([^"]+)"', text): + if VERSION_RE.match(match.group(1)): + return match.group(1) + raise SystemExit("no Mathlib release tag found in lakefile.toml") + + +def remote_tags(remote: str = MATHLIB_REMOTE) -> list[str]: + """List release tags published by the Mathlib repository.""" + result = subprocess.run( + ["git", "ls-remote", "--tags", "--refs", remote], + capture_output=True, + text=True, + check=True, + ) + tags = [] + for line in result.stdout.splitlines(): + _, _, ref = line.partition("refs/tags/") + if ref and VERSION_RE.match(ref.strip()): + tags.append(ref.strip()) + return tags + + +def newer_versions( + current: str, tags: list[str], *, stable_only: bool = False +) -> list[str]: + """Return tags strictly newer than ``current``, oldest first. + + Release candidates count by default: the pool tracks the newest Lean and + Mathlib available, and an rc is what "newest" usually means during a + release cycle. ``stable_only`` narrows this to final releases. + """ + threshold = version_key(current) + candidates = [ + tag + for tag in tags + if version_key(tag) > threshold and not (stable_only and is_prerelease(tag)) + ] + return sorted(set(candidates), key=version_key) + + +def pin_files(root: Path, version: str) -> list[Path]: + """Rewrite the toolchain and dependency pins to ``version``. + + Returns the files that changed. ``lake update`` still has to regenerate + the manifests afterwards; this only moves the declared pins. + """ + if not VERSION_RE.match(version): + raise SystemExit(f"not a release tag: {version}") + changed: list[Path] = [] + edits: list[tuple[Path, re.Pattern[str], str]] = [ + ( + root / "lean-toolchain", + re.compile(r"^leanprover/lean4:.*$", re.M), + f"leanprover/lean4:{version}", + ), + ( + root / "docbuild" / "lean-toolchain", + re.compile(r"^leanprover/lean4:.*$", re.M), + f"leanprover/lean4:{version}", + ), + # Only the release-tag rev is rewritten; branch pins (main, master) + # in the same file are left alone. + ( + root / "lakefile.toml", + re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"'), + f'rev = "{version}"', + ), + ( + root / "docbuild" / "lakefile.toml", + re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"'), + f'rev = "{version}"', + ), + ] + for path, pattern, replacement in edits: + if not path.is_file(): + raise SystemExit(f"missing pin file: {path}") + before = path.read_text(encoding="utf-8") + after = pattern.sub(replacement, before) + if after != before: + path.write_text(after, encoding="utf-8") + changed.append(path) + return changed + + +@dataclass +class ProjectDiagnostics: + """Errors and warnings attributed to a single pool project.""" + + project: str + errors: list[str] = field(default_factory=list) + warnings: list[str] = field(default_factory=list) + + def as_dict(self) -> dict[str, object]: + """Serialise for the workflow's job matrix and report artifact.""" + return { + "project": self.project, + "errors": self.errors[:MAX_EXCERPT_LINES], + "warnings": self.warnings[:MAX_EXCERPT_LINES], + "error_count": len(self.errors), + "warning_count": len(self.warnings), + } + + +def _attribute(text: str, fallback: str | None) -> str | None: + """Find which project a diagnostic line belongs to.""" + match = PATH_PROJECT_RE.search(text) or MODULE_PROJECT_RE.search(text) + return match.group(1) if match else fallback + + +def parse_build_log(log: str) -> dict[str, ProjectDiagnostics]: + """Bucket a ``lake build`` log's diagnostics by pool project. + + Diagnostics name their file, so most lines attribute themselves. A + message that does not (a bare continuation line, or an error lake prints + against a module rather than a file) is attributed to the module of the + most recent ``Building`` line. + """ + buckets: dict[str, ProjectDiagnostics] = {} + current: str | None = None + active: tuple[str, str] | None = None # (project, severity) for continuations + + for line in log.splitlines(): + building = BUILDING_RE.search(line) + if building: + module = MODULE_PROJECT_RE.search(building.group(1)) + current = module.group(1) if module else None + + diagnostic = DIAGNOSTIC_RE.match(line) + if diagnostic: + severity, message = diagnostic.groups() + project = _attribute(message, current) + if project is None: + active = None + continue + bucket = buckets.setdefault(project, ProjectDiagnostics(project)) + target = bucket.errors if severity == "error" else bucket.warnings + target.append(line.rstrip()) + active = (project, severity) + continue + + # Indented continuation of the previous diagnostic (goal state, etc.). + if active and line.startswith(" ") and line.strip(): + project, severity = active + bucket = buckets[project] + target = bucket.errors if severity == "error" else bucket.warnings + if len(target) < MAX_EXCERPT_LINES: + target.append(line.rstrip()) + elif not line.strip(): + active = None + + return buckets + + +def build_report(log: str) -> dict[str, object]: + """Summarise a build log into the report the workflow consumes.""" + buckets = parse_build_log(log) + broken = sorted((b for b in buckets.values() if b.errors), key=lambda b: b.project) + warned = sorted( + (b for b in buckets.values() if b.warnings and not b.errors), + key=lambda b: b.project, + ) + return { + "broken": [b.as_dict() for b in broken], + "warned": [b.as_dict() for b in warned], + "broken_projects": [b.project for b in broken], + "warned_projects": [b.project for b in warned], + "clean": not broken and not warned, + } + + +def _command_detect(args: argparse.Namespace) -> int: + """Print the newest Mathlib release to bump to, if any.""" + root = args.repo.resolve() + current = current_version(root) + tags = remote_tags(args.remote) + newer = newer_versions(current, tags, stable_only=args.stable_only) + # The newest available release, candidates included: the pool tracks the + # latest Lean and Mathlib, not the latest final release. + target = newer[-1] if newer else "" + payload = { + "current": current, + "target": target, + "available": newer, + "found": bool(target), + } + print(json.dumps(payload)) + return 0 + + +def _command_pin(args: argparse.Namespace) -> int: + """Rewrite the version pins and report which files moved.""" + changed = pin_files(args.repo.resolve(), args.version) + for path in changed: + logger.info("pinned %s", path) + if not changed: + logger.info("pins already at %s", args.version) + return 0 + + +def _command_report(args: argparse.Namespace) -> int: + """Turn a build log into the per-project breakage report.""" + log = args.log.read_text(encoding="utf-8", errors="replace") + report = build_report(log) + output = json.dumps(report, indent=2) + if args.output: + args.output.write_text(output + "\n", encoding="utf-8") + print(output) + return 0 + + +def _parse_args(argv: list[str] | None) -> argparse.Namespace: + """Parse command-line arguments.""" + parser = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + subparsers = parser.add_subparsers(dest="command", required=True) + + # `--repo` sits on each subcommand rather than the parent so it can be + # passed after the subcommand, which is how it reads in a workflow step. + detect = subparsers.add_parser("detect", help="find a newer Mathlib release") + detect.add_argument("--repo", type=Path, default=Path("."), help="repository root") + detect.add_argument("--remote", default=MATHLIB_REMOTE) + detect.add_argument( + "--stable-only", + action="store_true", + help="ignore -rc tags (default: bump to the newest release of any kind)", + ) + detect.set_defaults(func=_command_detect) + + pin = subparsers.add_parser("pin", help="rewrite the version pins") + pin.add_argument("--repo", type=Path, default=Path("."), help="repository root") + pin.add_argument("--version", required=True) + pin.set_defaults(func=_command_pin) + + report = subparsers.add_parser("report", help="triage a build log by project") + report.add_argument("--log", type=Path, required=True) + report.add_argument("--output", type=Path) + report.set_defaults(func=_command_report) + + return parser.parse_args(argv) + + +def main(argv: list[str] | None = None) -> int: + """Dispatch a subcommand; return a process exit code.""" + logging.basicConfig(level=logging.INFO, format="%(message)s") + args = _parse_args(argv) + return int(args.func(args)) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/python/lean_pool/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/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 new file mode 100644 index 000000000..82e627bc2 --- /dev/null +++ b/python/tests/test_bump.py @@ -0,0 +1,239 @@ +"""Tests for Mathlib bump detection, pin rewriting, and build-log triage.""" + +from __future__ import annotations + +from pathlib import Path + +import pytest + +from lean_pool.bump import ( + build_report, + current_version, + is_prerelease, + main, + newer_versions, + parse_build_log, + pin_files, + version_key, +) + +LAKEFILE = """name = "lean-pool" + +[leanOptions] +relaxedAutoImplicit = false + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.32.0-rc1" + +[[lean_lib]] +name = "LeanPool" +""" + +DOCBUILD_LAKEFILE = """name = "docbuild" + +[[require]] +name = "lean-pool" +path = "../" + +[[require]] +scope = "leanprover" +name = "doc-gen4" +rev = "v4.32.0-rc1" +""" + + +def _write_repo(root: Path) -> None: + """Create a repository with the four version pins a bump rewrites.""" + (root / "lean-toolchain").write_text("leanprover/lean4:v4.32.0-rc1\n") + (root / "lakefile.toml").write_text(LAKEFILE) + docbuild = root / "docbuild" + docbuild.mkdir() + (docbuild / "lean-toolchain").write_text("leanprover/lean4:v4.32.0-rc1\n") + (docbuild / "lakefile.toml").write_text(DOCBUILD_LAKEFILE) + + +# --------------------------------------------------------------------------- # +# Version ordering +# --------------------------------------------------------------------------- # +def test_final_release_outranks_its_candidates() -> None: + """v4.33.0 is newer than every v4.33.0-rcN.""" + assert version_key("v4.33.0") > version_key("v4.33.0-rc9") + assert version_key("v4.33.0-rc2") > version_key("v4.33.0-rc1") + assert version_key("v4.33.0-rc1") > version_key("v4.32.0") + + +def test_version_key_rejects_non_releases() -> None: + """A branch name is not a release tag.""" + with pytest.raises(ValueError, match="not a release tag"): + version_key("main") + + +def test_is_prerelease() -> None: + """Release candidates are distinguishable from final releases.""" + assert is_prerelease("v4.33.0-rc1") + assert not is_prerelease("v4.33.0") + + +def test_prereleases_count_by_default() -> None: + """The pool tracks the newest release, which mid-cycle is an rc.""" + tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1"] + assert newer_versions("v4.32.0-rc1", tags) == ["v4.32.0", "v4.33.0-rc1"] + assert newer_versions("v4.32.0-rc1", tags)[-1] == "v4.33.0-rc1" + + +def test_stable_only_narrows_to_final_releases() -> None: + """``stable_only`` opts out of release candidates.""" + tags = ["v4.32.0-rc1", "v4.32.0", "v4.33.0-rc1"] + assert newer_versions("v4.32.0-rc1", tags, stable_only=True) == ["v4.32.0"] + + +def test_newer_versions_empty_when_current_is_latest() -> None: + """An up-to-date pin yields no bump target.""" + assert newer_versions("v4.33.0", ["v4.32.0", "v4.33.0"], stable_only=False) == [] + + +def test_newer_versions_ignores_unparseable_tags() -> None: + """Only well-formed release tags are considered.""" + tags = ["v4.33.0", "nightly-2026-07-01"] + assert newer_versions( + "v4.32.0", + [t for t in tags if t != "nightly-2026-07-01"], + stable_only=True, + ) == ["v4.33.0"] + + +# --------------------------------------------------------------------------- # +# Pins +# --------------------------------------------------------------------------- # +def test_current_version_reads_the_mathlib_pin(tmp_path: Path) -> None: + """The pinned Mathlib release comes from lakefile.toml.""" + _write_repo(tmp_path) + assert current_version(tmp_path) == "v4.32.0-rc1" + + +def test_pin_files_rewrites_all_four_pins(tmp_path: Path) -> None: + """A bump moves both toolchains and both dependency revs.""" + _write_repo(tmp_path) + changed = pin_files(tmp_path, "v4.33.0-rc1") + assert len(changed) == 4 + assert (tmp_path / "lean-toolchain").read_text() == "leanprover/lean4:v4.33.0-rc1\n" + assert 'rev = "v4.33.0-rc1"' in (tmp_path / "lakefile.toml").read_text() + assert ( + tmp_path / "docbuild" / "lean-toolchain" + ).read_text() == "leanprover/lean4:v4.33.0-rc1\n" + assert ( + 'rev = "v4.33.0-rc1"' in (tmp_path / "docbuild" / "lakefile.toml").read_text() + ) + + +def test_pin_files_preserves_lean_options(tmp_path: Path) -> None: + """Rewriting pins must not disturb the gate-bearing [leanOptions].""" + _write_repo(tmp_path) + pin_files(tmp_path, "v4.33.0-rc1") + assert "relaxedAutoImplicit = false" in (tmp_path / "lakefile.toml").read_text() + + +def test_pin_files_is_idempotent(tmp_path: Path) -> None: + """Re-pinning to the same version changes nothing.""" + _write_repo(tmp_path) + pin_files(tmp_path, "v4.33.0-rc1") + assert pin_files(tmp_path, "v4.33.0-rc1") == [] + + +def test_pin_files_rejects_a_bad_version(tmp_path: Path) -> None: + """A non-release version string fails before touching any file.""" + _write_repo(tmp_path) + with pytest.raises(SystemExit, match="not a release tag"): + pin_files(tmp_path, "main") + assert "v4.32.0-rc1" in (tmp_path / "lean-toolchain").read_text() + + +def test_pin_files_reports_a_missing_pin(tmp_path: Path) -> None: + """A missing pin file is an error, not a silent skip.""" + _write_repo(tmp_path) + (tmp_path / "docbuild" / "lean-toolchain").unlink() + with pytest.raises(SystemExit, match="missing pin file"): + pin_files(tmp_path, "v4.33.0-rc1") + + +# --------------------------------------------------------------------------- # +# Build-log triage +# --------------------------------------------------------------------------- # +BUILD_LOG = """\ +info: [1/900] Building LeanPool.Alpha.Core +error: ./LeanPool/Alpha/Core.lean:12:2: unknown identifier 'Set.diff_eq' + the goal was + ⊢ s \\ t = s ∩ tᶜ +info: [2/900] Building LeanPool.Beta.Main +warning: ./LeanPool/Beta/Main.lean:3:0: `Symmetric` is deprecated +info: [3/900] Building LeanPool.Gamma.Basic +info: build completed +""" + + +def test_parse_build_log_buckets_by_project() -> None: + """Each diagnostic lands on the project whose file it names.""" + buckets = parse_build_log(BUILD_LOG) + assert set(buckets) == {"Alpha", "Beta"} + assert len(buckets["Alpha"].errors) == 3 # message plus two goal lines + assert buckets["Beta"].warnings and not buckets["Beta"].errors + + +def test_parse_build_log_attaches_continuation_lines() -> None: + """Indented goal-state lines stay with the error they explain.""" + errors = parse_build_log(BUILD_LOG)["Alpha"].errors + assert "unknown identifier" in errors[0] + assert any("⊢" in line for line in errors) + + +def test_build_report_separates_broken_from_warned() -> None: + """Only projects with errors become repair jobs.""" + report = build_report(BUILD_LOG) + assert report["broken_projects"] == ["Alpha"] + assert report["warned_projects"] == ["Beta"] + assert report["clean"] is False + + +def test_build_report_on_a_clean_build() -> None: + """A build with no diagnostics reports clean and schedules no repairs.""" + report = build_report("info: [1/1] Building LeanPool.Alpha\ninfo: done\n") + assert report["clean"] is True + assert report["broken_projects"] == [] + + +def test_project_with_errors_is_not_also_listed_as_warned() -> None: + """A project that fails outright is a repair job, not a warning job.""" + log = ( + "info: [1/2] Building LeanPool.Alpha.Core\n" + "warning: ./LeanPool/Alpha/Core.lean:1:0: unused variable\n" + "error: ./LeanPool/Alpha/Core.lean:9:0: type mismatch\n" + ) + report = build_report(log) + assert report["broken_projects"] == ["Alpha"] + assert report["warned_projects"] == [] + + +def test_diagnostic_without_a_path_uses_the_building_context() -> None: + """A message lake prints against a module still finds its project.""" + log = "info: [1/2] Building LeanPool.Delta.Core\nerror: no such file or directory\n" + assert build_report(log)["broken_projects"] == ["Delta"] + + +def test_excerpts_are_capped() -> None: + """A project that fails everywhere cannot flood the repair prompt.""" + lines = ["info: [1/1] Building LeanPool.Alpha.Core"] + lines += [f"error: ./LeanPool/Alpha/Core.lean:{i}:0: boom" for i in range(200)] + entry = build_report("\n".join(lines))["broken"][0] + assert entry["error_count"] == 200 + assert len(entry["errors"]) == 40 + + +def test_report_command_writes_json(tmp_path: Path) -> None: + """The report subcommand persists the artifact the workflow uploads.""" + log = tmp_path / "build.log" + log.write_text(BUILD_LOG) + output = tmp_path / "report.json" + assert main(["report", "--log", str(log), "--output", str(output)]) == 0 + assert '"broken_projects"' in output.read_text() diff --git a/python/tests/test_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/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 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())