Compare commits

...

3 Commits

Author SHA1 Message Date
Kim Morrison
7fad169044 revert one change 2026-02-17 21:13:06 +00:00
Kim Morrison
18a33d9666 chore: note that mathlib CI transient commit check can be ignored
This PR adds a note to the release checklist that the "Verify Transient
and Automated Commits" CI check on mathlib4 toolchain bump PRs can be
safely ignored, as it often fails on automated commits from the
nightly-testing history.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-17 21:05:33 +00:00
Kim Morrison
2aa9c6c5e8 chore: improve release command PR status checking
Add guidance to check actual PR merge state (not just cached CI results)
when reporting status between checklist runs. This prevents incorrectly
reporting already-merged PRs as still needing review.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-17 20:55:23 +00:00
2 changed files with 15 additions and 0 deletions

View File

@@ -103,6 +103,15 @@ Every time you run `release_checklist.py`, you MUST:
This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
The user needs to see the complete picture of what's waiting for review.
## Checking PR Status When Asked
When the user asks for "status" or you need to report on PRs between checklist runs:
- **ALWAYS check actual PR state** using `gh pr view <number> --repo <repo> --json state,mergedAt`
- Do NOT rely on cached CI results or previous checklist output
- The user may have merged PRs since your last check
- Report which PRs are MERGED, which are OPEN with CI status, and which are still pending
- After discovering merged PRs, rerun `release_checklist.py` to advance the release process
## Nightly Infrastructure
The nightly build system uses branches and tags across two repositories:

View File

@@ -70,6 +70,9 @@ We'll use `v4.6.0` as the intended release version as a running example.
The `release_steps.py` script handles this automatically by looking up the latest
ProofWidgets4 tag compatible with the target toolchain.
- Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
- The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored —
it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be
reproduced in CI. This does not block merging.
- `repl`:
There are two copies of `lean-toolchain`/`lakefile.lean`:
in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
@@ -150,6 +153,9 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
* The repository does not need any changes to move to the new version.
* Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository.
If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually.
* The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`,
`fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle.
These should be reviewed and removed if no longer needed, as they can interfere with CI checks.
- For each of the repositories listed in `script/release_repos.yml`,
- Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
- Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.