The semantics of `release_notes.py` was slightly confusing. It is meant
to be run a `script/release_notes.py v4.15.0` on the `releases/v4.16.0`
branch. To help, I've changed the usage to `script/release_notes.py
--since v4.15.0`.
This PR updates the release checklist script to:
* validate the `releases/v4.X.0` branch
* check that the release has been tagged
* appears on the releases list
* and has release notes (and if not, prompts to run the script
* and when checking downstream repositories, if something is not tagged
properly, suggests the script to run to push the missing tag.
This PR introduces a script that automates checking whether major
downstream repositories have been updated for a new toolchain release.
Sample output:
```
% ./release_checklist.py v4.16.0-rc1
Repository: Batteries
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: lean4checker
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: doc-gen4
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: Verso
❌ Not on target toolchain (needs ≥ v4.16.0-rc1, but main is on leanprover/lean4:v4.15.0)
Repository: ProofWidgets4
✅ On compatible toolchain (>= v4.16.0-rc1)
Repository: Aesop
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: import-graph
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: plausible
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: Mathlib
✅ On compatible toolchain (>= v4.16.0-rc1)
✅ Tag v4.16.0-rc1 exists
Repository: REPL
❌ Not on target toolchain (needs ≥ v4.16.0-rc1, but master is on leanprover/lean4:v4.14.0)
```
