update sections on release notes

message to explain why this merge is necessary, # especially if it merges an updated upstream into a topic branch. # #
Lines starting with '#' will be ignored, and an empty message aborts # the commit.

doc/SUMMARY.md

@@ -89,5 +89,6 @@
 - [Testing](./dev/testing.md)
 - [Debugging](./dev/debugging.md)
 - [Commit Convention](./dev/commit_convention.md)
+- [Release checklist](./dev/release_checklist.md)
 - [Building This Manual](./dev/mdbook.md)
 - [Foreign Function Interface](./dev/ffi.md)

doc/dev/release_checklist.md

@@ -0,0 +1,201 @@
+# Releasing a stable version
+
+This checklist walks you through releasing a stable version.
+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
+- `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)
+- It is possible that the `v4.6.0` section of `RELEASES.md` is out of sync between
+  `releases/v4.6.0` and `master`. This should be reconciled:
+  - Run `git diff master RELEASES.md`.
+  - You should expect to see additons on `master` in the `v4.7.0-rc1` section; ignore these.
+    (i.e. the new release notes for the upcoming release candidate).
+  - Reconcile discrepancies in the `v4.6.0` section,
+    usually via copy and paste and a commit to `releases/v4.6.0`.
+- `git tag v4.6.0`
+- `git push origin v4.6.0`
+- Now wait, while CI runs.
+  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
+    looking for the `v4.6.0` tag.
+  - This step can take up to an hour.
+  - If you are intending to cut the next release candidate on the same day,
+    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.
+- 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`.
+      The PR title should be "chore: bump toolchain to v4.6.0".
+      Since the `v4.6.0` release should be functionally identical to the last release candidate,
+      which the repository should already be on, this PR is a no-op besides changing the toolchain.
+    - Once this is merged, create the tag `v4.6.0` from `master`/`main` and push it.
+    - Merge the tag `v4.6.0` into the stable branch.
+  - We do this for the repositories:
+    - [lean4checker](https://github.com/leanprover/lean4checker)
+      - `lean4checker` uses a different version tagging scheme: use `toolchain/v4.6.0` rather than `v4.6.0`.
+    - [Std](https://github.com/leanprover-community/repl)
+    - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
+      - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
+        which does not refer to the toolchain being used.
+      - Make a new release in this sequence after merging the toolchain bump PR.
+      - `ProofWidgets` does not maintain a `stable` branch.
+    - [Aesop](https://github.com/leanprover-community/aesop)
+    - [Mathlib](https://github.com/leanprover-community/mathlib4)
+      - In addition to updating the `lean-toolchain` and `lakefile.lean`,
+        in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
+        `git checkout toolchain/v4.6.0` to the appropriate tag,
+        and then run `.github/workflows/mk_build_yml.sh`.
+    - [REPL](https://github.com/leanprover-community/repl)
+      - Note that there are two copies of `lean-toolchain`/`lakefile.lean`:
+        in the root, and in `test/Mathlib/`.
+  - Note that there are dependencies between these packages:
+    you should update the lakefile so that you are using the `v4.6.0` tag of upstream repositories
+    (or the sequential tag for `ProofWidgets4`), and run `lake update` before committing.
+  - This means that this process is sequential; each repository must have its bump PR merged,
+    and the new tag pushed, before you can make the PR for the downstream repositories.
+    - `lean4checker` has no dependencies
+    - `Std` has no dependencies
+    - `Aesop` depends on `Std`
+    - `ProofWidgets4` depends on `Std`
+    - `Mathlib` depends on `Aesop`, `ProofWidgets4`, and `lean4checker` (and transitively on `Std`)
+    - `REPL` depends on `Mathlib` (this dependency is only for testing).
+- 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`.
+  Please see previous announcements for suggested language.
+  You will want a few bullet points for main topics from the release notes.
+  Link to the blog post from the Zulip announcement.
+  Please also make sure that whoever is handling social media knows the release is out.
+
+## 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.
+- Waiting for Mathlib CI and bors: 120 minutes.
+- Finalizing Mathlib tags and stable branch, and updating REPL: 15 minutes.
+- Posting announcement and/or blog post: 20 minutes.
+
+# Creating a release candidate.
+
+This checklist walks you through creating the first release candidate for a version of Lean.
+
+We'll use `v4.7.0-rc1` as the intended release version in this example.
+
+- Decide which nightly release you want to turn into a release candidate.
+  We will use `nightly-2024-02-29` in this example.
+- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
+  - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
+    in their `lean-toolchain`.
+  - The steps required to reach that state are beyond the scope of this checklist, but see below!
+- Create the release branch from this nightly tag:
+    ```
+    git remote add nightly https://github.com/leanprover/lean4-nightly.git
+    git fetch nightly tag nightly-2024-02-29
+    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 `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`
+- 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/
+  - 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.
+    - 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`),
+      but for minor items don't put any work in expanding on commit messages.
+  - (How we want to release notes to look is evolving: please update this section if it looks wrong!)
+- Next, we will move a curated list of downstream repos to the release candidate.
+  - This assumes that there is already a *reviewed* branch `bump/v4.7.0` on each repository
+    containing the required adaptations (or no adaptations are required).
+    The preparation of this branch is beyond the scope of this document.
+  - For each of the target repositories:
+    - Checkout the `bump/v4.7.0` branch.
+    - Verify that the `lean-toolchain` is set to the nightly from which the release candidate was created.
+    - `git merge origin/master`
+    - Change the `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`
+    - In `lakefile.lean`, change any dependencies which were using `nightly-testing` or `bump/v4.7.0` branches
+      back to `master` or `main`, and run `lake update` for those dependencies.
+    - Run `lake build` to ensure that dependencies are found (but it's okay to stop it after a moment).
+    - `git commit`
+    - `git push`
+    - Open a PR from `bump/v4.7.0` to `master`, and either merge it yourself after CI, if appropriate,
+      or notify the maintainers that it is ready to go.
+    - Once this PR has been merged, tag `master` with `v4.7.0-rc1` and push this tag.
+  - We do this for the same list of repositories as for stable releases, see above.
+    As above, there are dependencies between these, and so the process above is iterative.
+    It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
+  - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
+    `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
+    (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
+- Make an announcement!
+  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
+  Please see previous announcements for suggested language.
+  You will want a few bullet points for main topics from the release notes.
+  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)`
+  - Removes `(in development)` from the section heading in `RELEASES.md` for `v4.7.0`,
+    and creates a new `v4.8.0 (in development)` section heading.
+
+## Time estimates:
+Slightly longer than the corresponding steps for a stable release.
+Similar process, but more things go wrong.
+In particular, updating the downstream repositories is significantly more work
+(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
+
+# Preparing `bump/v4.7.0` branches
+
+While not part of the release process per se,
+this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
+
+Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
+
+* Each repo has an unreviewed `nightly-testing` branch that
+  receives commits automatically from `master`, and
+  has its toolchain updated automatically for every nightly.
+  (Note: the aesop branch is not automated, and is updated on an as needed basis.)
+  As a consequence this branch is often broken.
+  A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches.
+* We fix the breakages by committing directly to `nightly-testing`: there is no PR process.
+  * This can either be done by the person managing this process directly,
+    or by soliciting assistance from authors of files, or generally helpful people on Zulip!
+* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
+* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we:
+  * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
+  * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
+  * In that branch, `git merge --squash nightly-testing` to bring across changes from `nightly-testing`.
+  * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
+  * Solicit review, merge the PR into `bump/v4,7,0`.
+* 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!