max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: simplify lean4checker step in release checklist (#4355)

Browse source
This commit is contained in:
Kim Morrison 2024-06-05 05:14:36 +01:00 • committed by GitHub
parent 28b8778218
commit 8f507b1008
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
doc/dev/release_checklist.md
View file

@ -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`.