From a3a6edcec15b69ae9847179dacc6aef6f786cabf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Feb 2025 20:24:45 +1100 Subject: [PATCH 1/5] updates to release_checklist --- doc/dev/release_checklist.md | 46 ++++++++++++++++++++++++++++++------ script/release_checklist.py | 2 +- script/release_repos.yml | 7 ++++++ 3 files changed, 47 insertions(+), 8 deletions(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 0500032df978..e62c5a5b852a 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -5,6 +5,8 @@ See below for the checklist for release candidates. We'll use `v4.6.0` as the intended release version as a running example. +- Run `scripts/release_checklist.py v4.6.0` to check the status of the release. + This script is purely informational, idempotent, and safe to run at any stage of the release process. - `git checkout releases/v4.6.0` (This branch should already exist, from the release candidates.) - `git pull` @@ -20,14 +22,24 @@ We'll use `v4.6.0` as the intended release version as a running example. - 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. +- Next we need to prepare the release notes. + - If the stable release is identical to the last release candidate (this should usually be the case), + you can reuse the release notes from `RELEASES.md`. + - If you want to regenerate the release notes, + use `script/release_notes.py --since v4.5.0`, run on the `releases/v4.6.0` branch, + and see the section "Writing the release notes" below for more information. + - Release notes should go in `RELEASES.md` on the `releases/v4.6.0` branch, + and should also be PR'd to `master` (suggested title: "chore: update release notes for v4.6.0"). - 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". - - 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. + - Verify on Github that "Set as the latest release" is checked. + - Copy the generated release note into the text box, adding - Next, we will move a curated list of downstream repos to the latest stable release. + - In order to have the access rights to push to these repositories and merge PRs, + you will need to be a member of the `lean-release-managers` team at both `leanprover-community` and `leanprover`. + Contact Kim Morrison (@kim-em) to arrange access. - For each of the repositories listed below: - Make a PR to `master`/`main` changing the toolchain to `v4.6.0` + - The usual branch name would be `bump_to_v4.6.0`. - Update the toolchain file - In the Lakefile, if there are dependencies on specific version tags of dependencies that you've already pushed as part of this process, update them to the new tag. If they depend on `main` or `master`, don't change this; you've just updated the dependency, so it will work and be saved in the manifest @@ -47,6 +59,11 @@ We'll use `v4.6.0` as the intended release version as a running example. - Toolchain bump PR - Create and push the tag - Merge the tag into `stable` + - [quote4](https://github.com/leanprover-community/quote4) + - No dependencies + - Toolchain bump PR + - Create and push the tag + - Merge the tag into `stable` - [doc-gen4](https://github.com/leanprover/doc-gen4) - Dependencies: exist, but they're not part of the release workflow - Toolchain bump PR including updated Lake manifest @@ -55,6 +72,7 @@ We'll use `v4.6.0` as the intended release version as a running example. - [Verso](https://github.com/leanprover/verso) - Dependencies: exist, but they're not part of the release workflow - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow + - Warnings during `lake build` are expected. - Toolchain bump PR including updated Lake manifest - Create and push the tag - There is no `stable` branch; skip this step @@ -102,7 +120,7 @@ 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` -- Run `scripts/release_checklist.py v4.6.0` to check that everything is in order. +- Run `script/release_checklist.py v4.6.0` to check that everything is in order. - 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` @@ -252,10 +270,24 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches. Release notes are automatically generated from the commit history, using `script/release_notes.py`. -Run this as `script/release_notes.py v4.6.0`, where `v4.6.0` is the *previous* release version. This will generate output -for all commits since that tag. Note that there is output on both stderr, which should be manually reviewed, +Run this as `script/release_notes.py --since v4.6.0`, where `v4.6.0` is the *previous* release version. +This script should be run on the `releases/v4.7.0` branch. +This will generate output for all commits since that tag. +Note that there is output on both stderr, which should be manually reviewed, and on stdout, which should be manually copied to `RELEASES.md`. +The output on stderr should mostly be about commits for which the script could not find an associated PR, +usually because a PR was rebase-merged because it contained an update to stage0. +Some judgement is required here: ignore commits which look minor, +but manually add items to the release notes for significant PRs that were rebase-merged. + 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. +# `release_checklist.py` + +The script `script/release_checklist.py` attempts to automate checking the status of the release. + +Future improvements: +* We check the release notes have been posted on Github, + but do not check that they are present in `RELEASES.md` on the release branch or on `master`. diff --git a/script/release_checklist.py b/script/release_checklist.py index ed6922a8ee4b..489f31e3bf34 100755 --- a/script/release_checklist.py +++ b/script/release_checklist.py @@ -179,7 +179,7 @@ def main(): # Check the first line of the release notes release_notes = get_release_notes(lean_repo_url, toolchain, github_token) - if release_notes and release_notes.splitlines()[0].strip() == toolchain: + if release_notes and toolchain in release_notes.splitlines()[0].strip(): print(f" ✅ Release notes look good.") else: previous_minor_version = version_minor - 1 diff --git a/script/release_repos.yml b/script/release_repos.yml index 5e805e70f936..4246f1c36a45 100644 --- a/script/release_repos.yml +++ b/script/release_repos.yml @@ -13,6 +13,13 @@ repositories: branch: master dependencies: [] + - name: quote4 + url: https://github.com/leanprover-community/quote4 + toolchain-tag: true + stable-branch: true + branch: master + dependencies: [] + - name: doc-gen4 url: https://github.com/leanprover/doc-gen4 toolchain-tag: true From 7d5cd47451ed15dd84ee338ba3320381b4243f10 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Feb 2025 21:32:25 +1100 Subject: [PATCH 2/5] release checklist updates --- doc/dev/release_checklist.md | 28 +++++++++++----------------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index e62c5a5b852a..f2193bef0da2 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -104,11 +104,10 @@ We'll use `v4.6.0` as the intended release version as a running example. - Create and push the tag - There is no `stable` branch; skip this step - [Mathlib](https://github.com/leanprover-community/mathlib4) - - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph` + - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `quote4`, `import-graph` - Toolchain bump PR notes: - - In addition to updating the `lean-toolchain` and `lakefile.lean`, - in `.github/workflows/lean4checker.yml` update the line - `git checkout v4.6.0` to the appropriate tag. + - Upstream dependencies should use their `main` or `master` branch, not toolchain tags. + (Unlike for other repos.) - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably - Create and push the tag - Create a new branch from the tag, push it, and open a pull request against `stable`. @@ -120,17 +119,12 @@ 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` -- Run `script/release_checklist.py v4.6.0` to check that everything is in order. -- 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 +- Run `script/release_checklist.py v4.6.0` again to check that everything is in order. - 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. + If there is a blog post, link to that from the zulip announcement. - Make sure that whoever is handling social media knows the release is out. ## Optimistic(?) time estimates: @@ -150,6 +144,7 @@ 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 to choose the nightly that will become the release candidate as early as possible, to avoid confusion. - It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly. - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29` in their `lean-toolchain`. @@ -162,10 +157,9 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. git checkout -b releases/v4.7.0 ``` - In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.` -- 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`). + - change the `LEAN_VERSION_IS_RELEASE` line to `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` @@ -174,9 +168,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. - This step can take up to an hour. - (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/ - Verify that the release is marked as a prerelease (this should have been done automatically by the CI release job). - - 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 "update stage0" commits, and anything with a completely inscrutable commit message. + - Generate release notes by running `script/release_notes.py --since v4.6.0` on the `releases/v4.7.0` branch. + See the section "Writing the release notes" below for more information. - Next, we will move a curated list of downstream repos to the release candidate. - This assumes that for each repository either: * There is already a *reviewed* branch `bump/v4.7.0` containing the required adaptations. @@ -204,7 +197,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch for the next development cycle. Set the `lean-toolchain` file on this branch to same `nightly` you used for this release. - - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag + - (Note: we're currently uncertain if we really want to do this step. Check with Kim Morrison if you're unsure.) + For Batteries/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! From eaf2e5f402fb291c480ab851a18d3a4bc924a4e0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Feb 2025 23:10:30 +1100 Subject: [PATCH 3/5] Update doc/dev/release_checklist.md Co-authored-by: Johan Commelin --- doc/dev/release_checklist.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index f2193bef0da2..4f4cedec1734 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -32,7 +32,11 @@ We'll use `v4.6.0` as the intended release version as a running example. and should also be PR'd to `master` (suggested title: "chore: update release notes for v4.6.0"). - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears. - Verify on Github that "Set as the latest release" is checked. - - Copy the generated release note into the text box, adding + - Copy the generated release note into the text box, adding the header + ``` + v4.6.0 + ---------- + ``` - Next, we will move a curated list of downstream repos to the latest stable release. - In order to have the access rights to push to these repositories and merge PRs, you will need to be a member of the `lean-release-managers` team at both `leanprover-community` and `leanprover`. From e8b19801524877924a2ef83c3fe5d36c4c7f6707 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Feb 2025 23:11:03 +1100 Subject: [PATCH 4/5] Update doc/dev/release_checklist.md --- doc/dev/release_checklist.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 4f4cedec1734..53c5c594fa18 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -76,7 +76,7 @@ We'll use `v4.6.0` as the intended release version as a running example. - [Verso](https://github.com/leanprover/verso) - Dependencies: exist, but they're not part of the release workflow - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow - - Warnings during `lake build` are expected. + - Warnings during `lake update` and `lake build` are expected. - Toolchain bump PR including updated Lake manifest - Create and push the tag - There is no `stable` branch; skip this step From c03d519d7f31e1a283a7f0a932fcc16e12dc28bc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 3 Feb 2025 23:12:17 +1100 Subject: [PATCH 5/5] Update doc/dev/release_checklist.md --- doc/dev/release_checklist.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 53c5c594fa18..80c40ba5d601 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -149,6 +149,7 @@ 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 to choose the nightly that will become the release candidate as early as possible, to avoid confusion. +- Throughout this process you can use `script/release_checklist.py v4.7.0-rc1` to track progress. - It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly. - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29` in their `lean-toolchain`.