chore: improvements to release checklist and scripts (#8586)

This PR improves the release checklist and scripts:

* Check that the release's commit hash is not all-numeric starting with
0 (this can break SemVer, which [required us to release
v4.21.0-rc2](https://github.com/leanprover/lean4/releases/tag/v4.21.0-rc2)).
* Check that projects being bumped to a release tag do not reference
`nightly-testing` anymore.
* Clarify how to create subsequent release candidates if an `-rc1`
already exists.
* Fix typos in the release checklist documentation.

doc/dev/release_checklist.md

@@ -50,7 +50,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - Re-running `script/release_checklist.py` will then create the tag `v4.6.0` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
     - `script/release_checklist.py` will then merge the tag `v4.6.0` into the `stable` branch and push it (unless `stable-branch: false` in the `release_repos.yml` file).
   - Special notes on repositories with exceptional requirements:
-    - `doc-gen4` has addition dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually.
+    - `doc-gen4` has additional dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually.
     - `verso`:
       - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
         Usually you don't need to do anything.
@@ -94,6 +94,8 @@ We'll use `v4.6.0` as the intended release version as a running example.
 
 This checklist walks you through creating the first release candidate for a version of Lean.
 
+For subsequent release candidates, the process is essentially the same, but we start out with the `releases/v4.7.0` branch already created.
+
 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.
@@ -112,7 +114,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     git fetch nightly tag nightly-2024-02-29
     git checkout nightly-2024-02-29
     git checkout -b releases/v4.7.0
-    git push --set-upstream origin releases/v4.18.0
+    git push --set-upstream origin releases/v4.7.0
     ```
 - 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.

script/release_checklist.py

@@ -53,6 +53,23 @@ def tag_exists(repo_url, tag_name, github_token):
     matching_tags = response.json()
     return any(tag["ref"] == f"refs/tags/{tag_name}" for tag in matching_tags)
 
+def commit_hash_for_tag(repo_url, tag_name, github_token):
+    # Use /git/matching-refs/tags/ to get all matching tags
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/matching-refs/tags/{tag_name}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+
+    if response.status_code != 200:
+        return False
+
+    # Check if any of the returned refs exactly match our tag
+    matching_tags = response.json()
+    matching_commits = [tag["object"]["sha"] for tag in matching_tags if tag["ref"] == f"refs/tags/{tag_name}"]
+    if len(matching_commits) != 1:
+        return None
+    else:
+        return matching_commits[0]
+
 def release_page_exists(repo_url, tag_name, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -286,6 +303,14 @@ def main():
         lean4_success = False
     else:
         print(f"  ✅ Tag {toolchain} exists")
+        commit_hash = commit_hash_for_tag(lean_repo_url, toolchain, github_token)
+        SHORT_HASH_LENGTH = 7 # Lake abbreviates the Lean commit to 7 characters.
+        if commit_hash is None:
+            print(f"  ❌ Could not resolve tag {toolchain} to a commit.")
+            lean4_success = False
+        elif commit_hash[0] == '0' and commit_hash[:SHORT_HASH_LENGTH].isnumeric():
+            print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
+            lean4_success = False
 
     if not release_page_exists(lean_repo_url, toolchain, github_token):
         print(f"  ❌ Release page for {toolchain} does not exist")

script/release_steps.py

@@ -94,6 +94,7 @@ def generate_script(repo, version, config):
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge origin/bump/{version.split('-rc')[0]}",
             "echo 'Please resolve any conflicts.'",
+            "grep nightly-testing lakefile.* && echo 'Please ensure the lakefile does not include nightly-testing versions.'",
             ""
         ])
     if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]: