Skip to content

fix: gate reference-manual tagging on release notes title correctness#12512

Merged
kim-em merged 2 commits intomasterfrom
fix-release-notes-title-ordering
Feb 17, 2026
Merged

fix: gate reference-manual tagging on release notes title correctness#12512
kim-em merged 2 commits intomasterfrom
fix-release-notes-title-ordering

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Feb 16, 2026

This PR fixes a release workflow bug where the reference-manual repository would get tagged with a stale release notes title (e.g., still showing "-rc1" for a stable release).

The root cause was a sequencing issue: release_steps.py didn't update the release notes title when bumping the reference-manual toolchain, and release_checklist.py only checked the title while the bump PR was open. Once merged, it went straight to tagging without rechecking.

Two fixes:

  • release_checklist.py: add a title correctness check before tagging reference-manual (blocks tagging if the title is wrong)
  • release_steps.py: automatically update the #doc title line in the release notes file when bumping reference-manual (handles both RC-to-stable and RC-to-RC transitions)

🤖 Prepared with Claude Code

This PR fixes a release workflow bug where the reference-manual repository
would get tagged with a stale release notes title (e.g., still showing
"-rc1" for a stable release).

The root cause was a sequencing issue: `release_steps.py` didn't update
the release notes title when bumping the reference-manual toolchain, and
`release_checklist.py` only checked the title while the bump PR was open.
Once merged, it went straight to tagging without rechecking.

Two fixes:
- `release_checklist.py`: add a title correctness check before tagging
  reference-manual (blocks tagging if the title is wrong)
- `release_steps.py`: automatically update the `#doc` title line in
  the release notes file when bumping reference-manual (handles both
  RC-to-stable and RC-to-RC transitions)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@kim-em kim-em added the changelog-no Do not include this PR in the release changelog label Feb 16, 2026
@kim-em kim-em added this pull request to the merge queue Feb 16, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to a conflict with the base branch Feb 16, 2026
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 16, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2f8c85af89b1afdb03cdb15005524886e18be414 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-16 23:38:07)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2f8c85af89b1afdb03cdb15005524886e18be414 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-16 23:38:08)

…itle-ordering

# Conflicts:
#	script/release_steps.py
@kim-em kim-em enabled auto-merge February 17, 2026 01:13
@kim-em kim-em added this pull request to the merge queue Feb 17, 2026
Merged via the queue into master with commit 2a8650f Feb 17, 2026
15 checks passed
kim-em added a commit that referenced this pull request Feb 17, 2026
…#12512)

This PR fixes a release workflow bug where the reference-manual
repository would get tagged with a stale release notes title (e.g.,
still showing "-rc1" for a stable release).

The root cause was a sequencing issue: `release_steps.py` didn't update
the release notes title when bumping the reference-manual toolchain, and
`release_checklist.py` only checked the title while the bump PR was
open. Once merged, it went straight to tagging without rechecking.

Two fixes:
- `release_checklist.py`: add a title correctness check before tagging
reference-manual (blocks tagging if the title is wrong)
- `release_steps.py`: automatically update the `#doc` title line in the
release notes file when bumping reference-manual (handles both
RC-to-stable and RC-to-RC transitions)

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants