diff --git a/.claude/commands/release.md b/.claude/commands/release.md index e8e1810f0c..97dd671b0a 100644 --- a/.claude/commands/release.md +++ b/.claude/commands/release.md @@ -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 --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: diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index b16f46993a..487575285c 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -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 ` (e.g. replacing `` 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`.