v4.16.0-rc2

Stream: nightly-testing

[Kim Morrison]

I've just started the v4.16.0-rc2 release, thanks very much to @Mac Malone for quickly resolving the cache issues as soon as he was back from vacation!

[Kim Morrison]

We have a new tool that checks the status of the release checklist, and I'm going to experiment by posting updates from that checklist tool as I proceed. I hope later this tool will run automatically via a bot, and will also actually perform many of the steps!

[Kim Morrison]

Performing preliminary checks...
  ✅ Branch releases/v4.16.0 exists
  ✅ CMake version settings are correct in src/CMakeLists.txt
  ✅ Tag v4.16.0-rc2 exists
  ✅ Release page for v4.16.0-rc2 exists
  ✅ Release notes look good.

Checking repositories...

Repository: Batteries
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: lean4checker
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: doc-gen4
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: Verso
  ❌ Not on target toolchain (needs ≥ v4.16.0-rc2, but main is on leanprover/lean4:v4.16.0-rc1)

Repository: Cli
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: ProofWidgets4
  ✅ On compatible toolchain (>= v4.16.0-rc2)

Repository: Aesop
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: import-graph
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: plausible
  ✅ On compatible toolchain (>= v4.16.0-rc2)
  ✅ Tag v4.16.0-rc2 exists

Repository: Mathlib
  ❌ Not on target toolchain (needs ≥ v4.16.0-rc2, but master is on leanprover/lean4:v4.16.0-rc1)

Repository: REPL
  ❌ Not on target toolchain (needs ≥ v4.16.0-rc2, but master is on leanprover/lean4:v4.15.0)

[Kim Morrison]

(Added a check that the versions and release flag are set correctly on the releases/v4.16.0 branch.)

[Kim Morrison]

(Added a check that the release notes look good, and otherwise prompt to run the generation script.)

[Kim Morrison]

(Update release note)

[Kim Morrison]

(bump lean4checker)

[Kim Morrison]

(bump batteries)

[Kim Morrison]

(bump doc-gen4)

[Kim Morrison]

(bump lean4-cli)

[Kim Morrison]

(tag batteries and lean4checker)

[Kim Morrison]

(bump aesop)

[Kim Morrison]

(bump ProofWidgets and import-graph)

[Kim Morrison]

(bump plausible)

[Kim Morrison]

(tag doc-gen4, lean4-cli, import-graph)

[Kim Morrison]

(Just pausing a moment to automate tag creation, and have the checklist script suggest running the creation script.)

[Kim Morrison]

(running recommended script script/push_repo_release_tag.py leanprover-community/aesop master v4.16.0-rc2)

[Kim Morrison]

(#20727 is the Mathlib bump)

[Kim Morrison]

A few outstanding issues with the release process:

• Automate creation of the bump branches?
  • Easy for the repos with no dependencies.
  • Otherwise, this requires editing the lakefile.toml / lakefile.lean to update dependencies...
  • For bump to stable releases or not-the-first-release-candidate, everything is easy. For the first release candidate, we need to merge all the bump/v4.16.0 and/or nightly-testing branches at each step, and this is harder to automate.
• For now it requires some human judgement about whether a new release of ProofWidgets will be needed or not.
• The release checklist script could detect whether the relevant bump PRs are in flight and need merging, or need to be created.
• For everything but Mathlib, I think the plan is to pin dependencies to toolchain tags.
• For Mathlib, the plan is just to depend on master / main of each upstream dependency, so that the auto-update bot works.
• The release checklist script could verify, after updating the lakefile and running lake update, that all upstream dependencies are actually using the right lean-toolchain. However doc-gen4 would need an exception, as we don't regularly bump its dependencies.

[Kim Morrison]

• The release checklist could pay attention to the dependency information it has available, in order to tell you which repositories are ready to be bumped.