From 8f507b100848a99f04396cc9b7476f6c89400e8e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 5 Jun 2024 05:14:36 +0100 Subject: [PATCH] chore: simplify lean4checker step in release checklist (#4355) --- doc/dev/release_checklist.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 2e0b06b576..aa80e5cf6c 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -46,7 +46,6 @@ We'll use `v4.6.0` as the intended release version as a running example. - We do this for the repositories: - [lean4checker](https://github.com/leanprover/lean4checker) - No dependencies - - Note: `lean4checker` uses a different version tagging scheme: use `toolchain/v4.6.0` rather than `v4.6.0`. - Toolchain bump PR - Create and push the tag - Merge the tag into `stable` @@ -82,10 +81,8 @@ We'll use `v4.6.0` as the intended release version as a running example. - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph` - Toolchain bump PR notes: - 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`. Coordinate with - a Mathlib maintainer to get this merged. + in `.github/workflows/lean4checker.yml` update the line + `git checkout v4.6.0` to the appropriate tag. - 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`.