doc: clarify release notes title format requirements

- Add explicit section explaining title format for -rc1, subsequent RCs, and stable releases
- Update example to use realistic date format instead of YYYY-MM-DD
- Clarify that only content is written for -rc1, subsequent releases just update the title

doc/dev/release_checklist.md

@@ -218,8 +218,18 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-Release notes are only needed for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
-just update the version number in the title of the existing release notes file.
+Release notes content is only written for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
+just update the title in the existing release notes file (see "Release notes title format" below).
+
+## Release notes title format
+
+The title in the `#doc (Manual)` line must follow these formats:
+
+- **For -rc1**: `"Lean 4.7.0-rc1 (2024-03-15)"` — Include the RC suffix and the release date
+- **For -rc2, -rc3, etc.**: `"Lean 4.7.0-rc2 (2024-03-20)"` — Update the RC number and date
+- **For stable release**: `"Lean 4.7.0 (2024-04-01)"` — Remove the RC suffix but keep the date
+
+The date should be the actual date when the tag was pushed (or when CI completed and created the release page).
 
 ## Generating the release notes
 
@@ -273,7 +283,7 @@ open Verso.Genre
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 
-#doc (Manual) "Lean 4.7.0-rc1 (YYYY-MM-DD)" =>
+#doc (Manual) "Lean 4.7.0-rc1 (2024-03-15)" =>
 %%%
 tag := "release-v4.7.0"
 file := "v4.7.0"
@@ -316,7 +326,27 @@ Common errors and fixes:
 
 ## Creating the PR
 
-Create a separate PR for the release notes (don't bundle with the toolchain bump PR):
+**Important: Timing with the reference-manual tag**
+
+The reference-manual repository deploys documentation when a version tag is pushed. If you merge
+release notes AFTER the tag is created, the deployed documentation won't include them.
+
+You have two options:
+
+1. **Preferred**: Include the release notes in the same PR as the toolchain bump (or merge the
+   release notes PR before creating the tag). This ensures the tag includes the release notes.
+
+2. **If release notes are merged after the tag**: You must regenerate the tag to trigger a new deployment:
+   ```bash
+   cd /path/to/reference-manual
+   git fetch origin
+   git tag -d v4.7.0-rc1  # Delete local tag
+   git tag v4.7.0-rc1 origin/main  # Create tag at current main (which has release notes)
+   git push origin :refs/tags/v4.7.0-rc1  # Delete remote tag
+   git push origin v4.7.0-rc1  # Push new tag (triggers Deploy workflow)
+   ```
+
+If creating a separate PR for release notes:
 ```bash
 git checkout -b v4.7.0-release-notes
 git add Manual/Releases/v4_7_0.lean Manual/Releases.lean