doc: update release checklist for new release notes workflow

doc/dev/release_checklist.md

@@ -5,19 +5,15 @@ See below for the checklist for release candidates.
 
 We'll use `v4.6.0` as the intended release version as a running example.
 
-- One week before the planned release, ensure that someone has written the first draft of the release blog post
+- One week before the planned release, ensure that (1) someone has written the release notes and (2) someone has written the first draft of the release blog post.
+  If there is any material in `./releases_drafts/`, then the release notes are not done. (See the section "Writing the release notes".)
 - `git checkout releases/v4.6.0`
   (This branch should already exist, from the release candidates.)
 - `git pull`
 - In `src/CMakeLists.txt`, verify you see
   - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
   - `set(LEAN_VERSION_IS_RELEASE 1)`
   - (both of these should already be in place from the release candidates)
-- In `RELEASES.md`, verify that the `v4.6.0` section has been completed during the release candidate cycle.
-  It should be in bullet point form, with a point for every significant PR,
-  and may have a paragraph describing each major new language feature.
-  It should have a "breaking changes" section calling out changes that are specifically likely
-  to cause problems for downstream users.
 - `git tag v4.6.0`
 - `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
@@ -28,8 +24,9 @@ We'll use `v4.6.0` as the intended release version as a running example.
     you may want to start on the release candidate checklist now.
 - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
   - Edit the release notes on Github to select the "Set as the latest release".
-  - Copy and paste the Github release notes from the previous releases candidate for this version
-    (e.g. `v4.6.0-rc1`), and quickly sanity check.
+  - Follow the instructions in creating a release candidate for the "GitHub release notes" step,
+    now that we have a written `RELEASES.md` section.
+    Do a quick sanity check.
 - Next, we will move a curated list of downstream repos to the latest stable release.
   - For each of the repositories listed below:
     - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
@@ -92,6 +89,10 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
+- The `v4.6.0` section of `RELEASES.md` is out of sync between
+  `releases/v4.6.0` and `master`. This should be reconciled:
+  - Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`
+    and commit this to `master`.
 - Merge the release announcement PR for the Lean website - it will be deployed automatically
 - Finally, make an announcement!
   This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
@@ -102,7 +103,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
 
 ## Optimistic(?) time estimates:
 - Initial checks and push the tag: 30 minutes.
-- Note that if `RELEASES.md` has discrepancies this could take longer!
 - Waiting for the release: 60 minutes.
 - Fixing release notes: 10 minutes.
 - Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
@@ -129,29 +129,26 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     git checkout nightly-2024-02-29
     git checkout -b releases/v4.7.0
     ```
-- In `RELEASES.md` remove `(development in progress)` from the `v4.7.0` section header.
-- Our current goal is to have written release notes only about major language features or breaking changes,
-  and to rely on automatically generated release notes for bugfixes and minor changes.
-  - Do not wait on `RELEASES.md` being perfect before creating the `release/v4.7.0` branch. It is essential to choose the nightly which will become the release candidate as early as possible, to avoid confusion.
-  - If there are major changes not reflected in `RELEASES.md` already, you may need to solicit help from the authors.
-  - Minor changes and bug fixes do not need to be documented in `RELEASES.md`: they will be added automatically on the Github release page.
-  - Commit your changes to `RELEASES.md`, and push.
-  - Remember that changes to `RELEASES.md` after you have branched `releases/v4.7.0` should also be cherry-picked back to `master`.
+- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
+- We will rely on automatically generated release notes for release candidates,
+  and the written release notes will be used for stable versions only.
+  It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
 - In `src/CMakeLists.txt`,
   - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
   - `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
   - Commit your changes to `src/CMakeLists.txt`, and push.
 - `git tag v4.7.0-rc1`
 - `git push origin v4.7.0-rc1`
+- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
 - Now wait, while CI runs.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
   - This step can take up to an hour.
-- Once the release appears at https://github.com/leanprover/lean4/releases/
+- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
   - Edit the release notes on Github to select the "Set as a pre-release box".
-  - Copy the section of `RELEASES.md` for this version into the Github release notes.
-  - Use the title "Changes since v4.6.0 (from RELEASES.md)"
-  - Then in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
-  - This will add a list of all the commits since the last stable version.
+  - If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
+    and use the title "Changes since v4.6.0 (from RELEASES.md)".
+  - Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
+    This will add a list of all the commits since the last stable version.
     - Delete anything already mentioned in the hand-written release notes above.
     - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
     - Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
@@ -190,12 +187,17 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   Please also make sure that whoever is handling social media knows the release is out.
 - Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
   - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - In `RELEASES.md`, update the `v4.7.0` section to say:
-    "Release candidate, release notes will be copied from branch `releases/v4.7.0` once completed."
-    Make sure that whoever is preparing the release notes during this cycle knows that it is their job to do so!
-  - In `RELEASES.md`, update the `v4.8.0` section to say:
-    "Development in progress".
-  - In `RELEASES.md`, verify that the old section `v4.6.0` has the full releases notes from the `releases/v4.6.0` branch.
+  - Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
+    ```
+    Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed.
+    ```
+    and inserts the following section before that section:
+    ```
+    v4.8.0
+    ----------
+    Development in progress.
+    ```
+  - Removes all the entries from the `./releases_drafts/` folder.
 
 ## Time estimates:
 Slightly longer than the corresponding steps for a stable release.
@@ -229,3 +231,18 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 * It is always okay to merge in the following directions:
   `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
   Please remember to push any merges you make to intermediate steps!
+
+# Writing the release notes
+
+We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
+The exact steps are a work in progress.
+Here is the general idea:
+
+* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
+  The release notes for `v4.6.0` will be copied to `master`.
+* There can be material for release notes entries in commit messages.
+* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
+  See `./releases_drafts/README.md` for more information.
+* The release notes should be written from a downstream expert user's point of view.
+
+This section will be updated when the next release notes are written (for `v4.10.0`).