lean4-htt/doc/dev
Kim Morrison 97d427b32b
doc: document release notes process and add guard check (#12158)
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>
2026-01-26 07:16:01 +00:00
..
bootstrap.md doc: clarify how to trigger automatic stage0 updates (#11413) 2025-11-28 12:56:59 +00:00
commit_convention.md doc: commit conventions and Mathlib CI (#6605) 2025-01-13 02:29:46 +00:00
debugging.md doc: stderrAsMessages is now the default on the cmdline as well (#4955) 2024-08-08 10:28:22 +00:00
ffi.md doc: replace ffi.md with links to the reference manual (#11737) 2025-12-19 07:23:06 +00:00
index.md doc: testing Lean while avoiding rebuilds for downstream projects (#10328) 2025-09-10 13:53:34 +00:00
release_checklist.md doc: document release notes process and add guard check (#12158) 2026-01-26 07:16:01 +00:00
testing.md doc: note that tests/lean/run disables linters (#11595) 2025-12-11 01:33:07 +00:00