Automate NOTICE generation, Mathlib bumps, and import-PR rebasing - #290
Conversation
NOTICE had drifted badly: 75 of 141 projects had no attribution entry at
all, which is an Apache-2.0 section 4(d) and MIT notice gap for every one
of them. Rather than lint a hand-maintained file, generate it.
- python/lean_pool/notice.py builds NOTICE from LeanPool/projects.yml
(which already carries `license` and `source.github_repo` for all 141)
plus NOTICE.extra.yml for the prose that cannot be derived: MIT
copyright lines, relicensing statements, upstream citation requests.
- notice.yml regenerates after merge, so drift cannot persist. It is not
a PR gate on purpose: a content PR may not touch NOTICE under
content-pr-guard, so gating there would be unsatisfiable.
- Regenerating also corrected four stale upstream URLs whose repositories
had been renamed (BrauerGroup_new, FLDutchmann/selberg-sieve4, RMT4,
AxiomMath/fel-polynomial).
mathlib-bump.yml migrates the pool to a new release in stages, only the
last of which needs a human: detect a newer tag, move the four pins and
plan shards, probe-build every project in parallel, triage the logs into a
per-project breakage map, fan out one Claude repair job per broken project,
then reassemble and open a draft PR. Pool projects never import each other,
so a bump decomposes into independent per-project repairs; the assemble
stage still rebuilds the whole pool, which is what catches the
cross-project effects per-project repair cannot see.
Repair jobs authenticate with a Claude subscription token and upload
patches rather than pushing, so parallel jobs cannot race the branch.
Probing is free and runs nightly regardless, so a release never lands as a
surprise; `repair: auto` spends quota on final releases only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Bumps now target the newest available release, candidates included: mid
release-cycle that is what "latest Lean and Mathlib" means, and the pool
tracks the latest. `detect` therefore reports v4.33.0-rc1 rather than
v4.32.1, `--stable-only` opts out, and the repair fan-out no longer skips
rc targets (it would otherwise never have run).
auto-rebase.yml keeps the import queue mergeable without hand-holding.
When a content PR lands, every other open import PR conflicts in exactly
two files, and in both the resolution is mechanical:
- LeanPool.lean is a sorted list of imports regenerated from the file
tree. It reproduces the committed 2,885-line index byte-for-byte, so
the job needs no Lean toolchain and runs in seconds.
- LeanPool/projects.yml takes the merged base's registry plus the cards
the branch adds, moved as verbatim text blocks. Round-tripping 141
cards through a YAML dumper would reformat every one and bury the
real change.
Any other conflicted path is a genuine content overlap: the merge is
abandoned and the PR labelled needs-manual-rebase rather than guessed at.
Verified against real pull request data by simulating #285 landing, which
makes #287 conflict exactly as predicted. The regenerated index is the
exact sorted union of both branches' modules with no conflict markers, and
the merged registry is 143 cards with no duplicates, valid YAML, required
fields intact, and the 142 pre-existing cards byte-identical.
Pushing to a fork branch needs REBASE_TOKEN (a GitHub App installation
token or a PAT); GITHUB_TOKEN has no write access to forks even with
"Allow edits by maintainers" set. Without it, fork PRs are labelled
instead of rebased and same-repo PRs still work.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| 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"] |
There was a problem hiding this comment.
newer_versions does not ignore unparseable tags
The test constructs tags = ["v4.33.0", "nightly-2026-07-01"] but then filters the nightly tag before calling newer_versions, so the function is only ever called with ["v4.33.0"]. The name and docstring claim that newer_versions itself ignores unparseable tags, but it doesn't — version_key raises ValueError inside the list comprehension if given a non-release tag. The protection is in remote_tags(), which pre-filters via VERSION_RE.match. Any future caller who passes an unfiltered list expecting newer_versions to be resilient would hit a runtime crash.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
| 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) |
There was a problem hiding this comment.
If two PRs both add a card with the same slug, and the first one merges before the second, merge_registry silently drops the second PR's version: the condition slug not in our_slugs is False once the first card is in main, so the block is never appended. Meanwhile the Lean files from the second PR are already in the tree (the rebase succeeds), so LeanPool.lean will contain import LeanPool.SomeProject but projects.yml will carry the first PR's card — a silent registry/tree mismatch. Since this is a genuine content conflict (two independent authors claiming the same slug), it might be safer to bail out and apply the needs-manual-rebase label when theirs adds a slug that appears in our_slugs but not in base_slugs.
| 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. |
There was a problem hiding this comment.
elan-init.sh fetched from master with no hash verification
The installer is downloaded from https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh and piped straight to sh in three separate jobs (pin, probe, assemble). Because this points at a mutable master ref with no checksum, a compromised push to the upstream repo (or a MITM) could execute arbitrary code inside a runner that holds contents: write access. Pinning to a specific commit hash or a tagged release URL (e.g. refs/tags/v4.1.2) and verifying a checksum would close this window.
| root / "lakefile.toml", | ||
| re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"'), | ||
| f'rev = "{version}"', | ||
| ), | ||
| ( |
There was a problem hiding this comment.
re.compile(r'rev\s*=\s*"v[\d.]+(?:-rc\d+)?"') matches every rev = "v…" line in lakefile.toml, not just Mathlib's. Right now the main lakefile.toml has only one such entry, so this is harmless. But if a future [[require]] dependency is pinned to a release tag (e.g. an Alloy or Batteries rev = "v1.0.0"), it would silently get overwritten to the new Mathlib version during a bump. The fix is to match only the Mathlib block, for example by anchoring the pattern to scope = "leanprover-community" on the preceding line.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
Greptile SummaryAdds three infrastructure-only automation pieces: generated
Confidence Score: 4/5Safe to merge as infrastructure-only automation; no Lean content is touched and all workflows open draft PRs or label rather than self-merging. The three new Python modules are well-tested (244 tests, live round-trips against committed files). The main workflow concerns are: the elan installer is fetched from an unpinned Files Needing Attention:
|
| Filename | Overview |
|---|---|
| python/lean_pool/bump.py | New module: version detection, pin rewriting, and build-log triage for Mathlib bumps. Solid design with one concern: the version-rev regex in pin_files would over-match if a future lakefile dependency uses a release-style rev. |
| python/lean_pool/rebase.py | New module: deterministic conflict resolution for import PRs. Index regeneration and three-way registry merge look correct; edge case where two PRs claim the same slug results in silent card drop rather than a manual-rebase flag. |
| .github/workflows/mathlib-bump.yml | New 521-line workflow: detect → pin → probe → triage → repair → assemble pipeline. All GitHub Actions SHAs are pinned; however, elan-init.sh is fetched from an unpinned master ref and executed directly in three jobs that hold write permissions. |
| .github/workflows/auto-rebase.yml | New workflow: serialised rebase of open import PRs after a content PR merges. Concurrency group prevents races; fork vs. same-repo token logic is correct; fall-through to needs-manual-rebase is appropriately conservative. |
| .github/workflows/python_ci.yml | Adds NOTICE and NOTICE.extra.yml to the path trigger; the exit-code-5 workaround comment says to remove it once tests exist, which they now do. |
| python/tests/test_bump.py | 39 new tests covering version ordering, pin rewriting, and build-log parsing. One test (test_newer_versions_ignores_unparseable_tags) pre-filters before calling the function and does not test the stated behaviour. |
Comments Outside Diff (1)
-
.github/workflows/python_ci.yml, line 72-86 (link)Now that this PR adds 64 tests, the exit-code-5 workaround should be retired per the inline comment ("Remove this once tests exist"). Keeping it around means a future misconfiguration that produces zero collected tests would silently pass CI.
Reviews (1): Last reviewed commit: "Bump to the newest release; auto-rebase ..." | Re-trigger Greptile
|
LLM review skipped: PR touches no |
1 participant
Three pieces of maintenance automation, all infrastructure-only (no
LeanPool/**content touched).NOTICE is now generated, not hand-maintained
NOTICEhad drifted badly: 75 of 141 projects had no attribution entry, an Apache-2.0 §4(d) and MIT notice gap for each. Every input was already inprojects.yml(all 141 cards carrylicenseandsource.github_repo), sopython/lean_pool/notice.pyderives the list sections andNOTICE.extra.ymlholds only the prose that cannot be derived — MIT copyright lines, relicensing statements, upstream citation requests.Verified against the previous file: all 141 present, 75 added, nothing dropped and no prose lost. Regenerating also corrected four upstream URLs whose repositories had been renamed —
BrauerGroup_new,FLDutchmann/selberg-sieve4,rmt4,axiommath— each confirmed against the GitHub API.notice.ymlregenerates after merge, so drift cannot persist. It is deliberately not a PR gate: a content PR may not touchNOTICEundercontent-pr-guard, so gating there would be unsatisfiable. Hand-edits are still caught bytest_repository_notice_is_current.Automated Mathlib bumps
mathlib-bump.ymlruns nightly:detect → pin → probe → triage → repair → assemble. Onlyrepaircosts anything (Claude subscription quota viaCLAUDE_CODE_OAUTH_TOKEN); everything else is free runner minutes. The probe shards across 10 parallel jobs and buckets failures per project, which becomes the repair fan-out's matrix — pool projects never import each other, so a bump decomposes into independent per-project repairs.assemblestill rebuilds the whole pool, which is what catches the cross-project effects per-project repair cannot see.Bumps target the newest available release, candidates included, so the current target is
v4.33.0-rc1rather thanv4.32.1. Repair jobs upload patches instead of pushing, so parallel jobs cannot race the branch. The PR it opens is always a draft.Statement-level changes are deliberately not gated: a lemma absorbed by Mathlib is a legitimate loss during a bump, so agents report absorbed declarations for a human to judge instead.
Auto-rebase for the import queue
auto-rebase.ymlkeeps open import PRs mergeable when a content PR lands. Both conflict points are mechanical:LeanPool.leanis regenerated from the file tree (it reproduces the committed 2,885-line index byte-for-byte, so no Lean toolchain is needed), andprojects.ymltakes the merged base plus the branch's added cards as verbatim text blocks. Anything else in conflict is a real content overlap — the merge is abandoned and the PR labelledneeds-manual-rebase.Validated against real PR data by simulating #285 landing, which makes #287 conflict exactly as predicted: the regenerated index is the exact sorted union of both branches with no conflict markers, and the merged registry is 143 cards, no duplicates, valid YAML, required fields intact, 142 pre-existing cards byte-identical.
Verification
actionlintclean on all workflows, every action SHA-pinneddetectsmoke-tested against the live Mathlib remote;pinrun end-to-end againstv4.33.0-rc1with all three upstream tags confirmed to exist and[leanOptions]preservedNot yet exercised: the bump workflow has never run a real build or repair job —
workflow_dispatchrequires the file on the default branch, so that can only happen after this merges.Before the automation is live
CLAUDE_CODE_OAUTH_TOKEN— fromclaude setup-token; without it the free stages still work and onlyrepairfailsREBASE_TOKEN— only needed to rebase fork PRs;GITHUB_TOKENcannot push to forks even with "Allow edits by maintainers". Same-repo PRs work without it.See
.github/BUMP_AUTOMATION.md.