This PR adds two safety notes to the Claude Code release command:
- Mathlib bump branches live on `mathlib4-nightly-testing`, not the main
`mathlib4` repo
- Never force-update remote refs without explicit user confirmation
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes `release_checklist.py` to report failing CI checks
immediately, even when other checks are still in progress. Previously,
having any in-progress checks would return `"pending"` status, masking
failures that had already occurred. Now it returns `"failure"` with a
message like `"1 check(s) failing, 2 still in progress"`.
Also adds a section to `.claude/commands/release.md` instructing the AI
assistant to investigate any CI failure immediately rather than
reporting it as "in progress" and moving on.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR adds a section to the /release command explaining how to use `gh
pr checks --watch` to wait for CI or merges without polling.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds guidance to the release slash command to check actual PR
merge state (using `gh pr view`) when reporting status, rather than
relying on cached CI results. This prevents incorrectly reporting
already-merged PRs as still needing review.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR documents the release notes writing process in detail and adds a
guard check to `release_checklist.py` to ensure release notes are
created for `-rc1` releases before proceeding with downstream repository
updates.
- **doc/dev/release_checklist.md**: Expanded "Writing the release notes"
section with detailed steps for generating, reviewing, and formatting
release notes in Verso format
- **script/release_checklist.py**: Added
`check_release_notes_file_exists()` to verify the release notes file
exists in reference-manual repository
- **.claude/commands/release.md**: Added "Release Notes" section
explaining the process for creating release notes during `-rc1` releases
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds documentation about the nightly build infrastructure to the
`/release` command to help future release managers understand the
relationship between branches and tags:
- `nightly` and `nightly-with-mathlib` are **branches** in
`leanprover/lean4`
- Dated tags like `nightly-YYYY-MM-DD` are **tags** in
`leanprover/lean4-nightly`
- When a nightly succeeds with mathlib, all three should point to the
same commit
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds explicit guidance to the `/release` command that Claude
should never merge PRs autonomously during the release process - always
wait for the user to do it.
🤖 Prepared with Claude Code
This PR improves the release automation. We link to CI output for
building the release tag, don't give instructions for bumping downstream
repositories until the release it ready, and improve documentation and
prompts.
This PR improves the scripts assisting with cutting Lean releases (by
reporting CI status of open PRs, and adding documentation), and adds a
`.claude/commands/release.md` prompt file so Claude can assist.
