fix: gate reference-manual tagging on release notes title correctness (#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>
This commit is contained in:
Kim Morrison 2026-02-17 12:20:36 +11:00 committed by GitHub
parent 69393c4d9e
commit 2a8650f975
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 41 additions and 0 deletions

View file

@ -836,6 +836,14 @@ def main():
continue
print(f" ✅ On compatible toolchain (>= {toolchain})")
# For reference-manual, check that the release notes title is correct BEFORE tagging.
# This catches the case where the toolchain bump PR was merged without updating
# the release notes title (e.g., still showing "-rc1" for a stable release).
if name == "reference-manual":
if not check_reference_manual_release_title(url, toolchain, branch, github_token):
repo_status[name] = False
continue
# Special handling for ProofWidgets4
if name == "ProofWidgets4":
if not check_proofwidgets4_release(url, toolchain, github_token):

View file

@ -483,6 +483,39 @@ def execute_release_steps(repo, version, config):
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
run_command("lake update", cwd=repo_path, stream_output=True)
# For reference-manual, update the release notes title to match the target version.
# e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
# e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
if repo_name == "reference-manual":
base_version = version.lstrip('v').split('-')[0] # "4.28.0"
file_name = f"v{base_version.replace('.', '_')}.lean"
release_notes_file = repo_path / "Manual" / "Releases" / file_name
if release_notes_file.exists():
is_rc = "-rc" in version
if is_rc:
# For RC releases, update to the exact RC version
display_version = version.lstrip('v') # "4.28.0-rc2"
else:
# For stable releases, strip any RC suffix
display_version = base_version # "4.28.0"
print(blue(f"Updating release notes title in {file_name}..."))
content = release_notes_file.read_text()
# Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
new_content = re.sub(
r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
rf'\g<1>{display_version}\3',
content
)
if new_content != content:
release_notes_file.write_text(new_content)
print(green(f"Updated release notes title to Lean {display_version}"))
else:
print(green("Release notes title already correct"))
else:
print(yellow(f"Release notes file {file_name} not found, skipping title update"))
# For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
if repo_name == "mathlib4":
print(blue("Checking ProofWidgets4 version pin..."))