feat: release checklist script (#6542)

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)
```

doc/dev/release_checklist.md

@@ -97,6 +97,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
+- Run `scripts/release_checklist.py v4.6.0` to check that everything is in order.
 - The `v4.6.0` section of `RELEASES.md` is out of sync between
   `releases/v4.6.0` and `master`. This should be reconciled:
   - Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`

script/release_checklist.py

@@ -0,0 +1,132 @@
+#!/usr/bin/env python3
+
+import argparse
+import yaml
+import requests
+import base64
+import subprocess
+import sys
+import os
+
+def parse_repos_config(file_path):
+    with open(file_path, "r") as f:
+        return yaml.safe_load(f)["repositories"]
+
+def get_github_token():
+    try:
+        import subprocess
+        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
+        if result.returncode == 0:
+            return result.stdout.strip()
+    except FileNotFoundError:
+        print("Warning: 'gh' CLI not found. Some API calls may be rate-limited.")
+    return None
+
+def get_branch_content(repo_url, branch, file_path, github_token):
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+    if response.status_code == 200:
+        content = response.json().get("content", "")
+        content = content.replace("\n", "")
+        try:
+            return base64.b64decode(content).decode('utf-8').strip()
+        except Exception:
+            return None
+    return None
+
+def tag_exists(repo_url, tag_name, github_token):
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/git/refs/tags/{tag_name}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+    return response.status_code == 200
+
+def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token):
+    # First get the commit SHA for the tag
+    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    # Get tag's commit SHA
+    tag_response = requests.get(f"{api_base}/git/refs/tags/{tag_name}", headers=headers)
+    if tag_response.status_code != 200:
+        return False
+    tag_sha = tag_response.json()['object']['sha']
+
+    # Get commits on stable branch containing this SHA
+    commits_response = requests.get(
+        f"{api_base}/commits?sha={stable_branch}&per_page=100",
+        headers=headers
+    )
+    if commits_response.status_code != 200:
+        return False
+
+    # Check if any commit in stable's history matches our tag's SHA
+    stable_commits = [commit['sha'] for commit in commits_response.json()]
+    return tag_sha in stable_commits
+
+def parse_version(version_str):
+    # Remove 'v' prefix and split into components
+    # Handle Lean toolchain format (leanprover/lean4:v4.x.y)
+    if ':' in version_str:
+        version_str = version_str.split(':')[1]
+    version = version_str.lstrip('v')
+    # Handle release candidates by removing -rc part for comparison
+    version = version.split('-')[0]
+    return tuple(map(int, version.split('.')))
+
+def is_version_gte(version1, version2):
+    """Check if version1 >= version2"""
+    return parse_version(version1) >= parse_version(version2)
+
+def is_release_candidate(version):
+    return "-rc" in version
+
+def main():
+    github_token = get_github_token()
+
+    if len(sys.argv) != 2:
+        print("Usage: python3 release_checklist.py <toolchain>")
+        sys.exit(1)
+
+    toolchain = sys.argv[1]
+
+    with open(os.path.join(os.path.dirname(__file__), "release_repos.yml")) as f:
+        repos = yaml.safe_load(f)["repositories"]
+
+    for repo in repos:
+        name = repo["name"]
+        url = repo["url"]
+        branch = repo["branch"]
+        check_stable = repo["stable-branch"]
+        check_tag = repo.get("toolchain-tag", True)
+
+        print(f"\nRepository: {name}")
+
+        # Check if branch is on at least the target toolchain
+        lean_toolchain_content = get_branch_content(url, branch, "lean-toolchain", github_token)
+        if lean_toolchain_content is None:
+            print(f"  ❌ No lean-toolchain file found in {branch} branch")
+            continue
+
+        on_target_toolchain = is_version_gte(lean_toolchain_content.strip(), toolchain)
+        if not on_target_toolchain:
+            print(f"  ❌ Not on target toolchain (needs ≥ {toolchain}, but {branch} is on {lean_toolchain_content.strip()})")
+            continue
+        print(f"  ✅ On compatible toolchain (>= {toolchain})")
+
+        # Only check for tag if toolchain-tag is true
+        if check_tag:
+            if not tag_exists(url, toolchain, github_token):
+                print(f"  ❌ Tag {toolchain} does not exist")
+                continue
+            print(f"  ✅ Tag {toolchain} exists")
+
+        # Only check merging into stable if stable-branch is true and not a release candidate
+        if check_stable and not is_release_candidate(toolchain):
+            if not is_merged_into_stable(url, toolchain, "stable", github_token):
+                print(f"  ❌ Tag {toolchain} is not merged into stable")
+                continue
+            print(f"  ✅ Tag {toolchain} is merged into stable")
+
+if __name__ == "__main__":
+    main()

script/release_repos.yml

@@ -0,0 +1,79 @@
+repositories:
+  - name: Batteries
+    url: https://github.com/leanprover-community/batteries
+    toolchain-tag: true
+    stable-branch: true
+    branch: main
+    dependencies: []
+
+  - name: lean4checker
+    url: https://github.com/leanprover/lean4checker
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies: []
+
+  - name: doc-gen4
+    url: https://github.com/leanprover/doc-gen4
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: Verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: ProofWidgets4
+    url: https://github.com/leanprover-community/ProofWidgets4
+    toolchain-tag: false
+    stable-branch: false
+    branch: main
+    dependencies:
+      - Batteries
+
+  - name: Aesop
+    url: https://github.com/leanprover-community/aesop
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Batteries
+
+  - name: import-graph
+    url: https://github.com/leanprover-community/import-graph
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: plausible
+    url: https://github.com/leanprover-community/plausible
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: Mathlib
+    url: https://github.com/leanprover-community/mathlib4
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Aesop
+      - ProofWidgets4
+      - lean4checker
+      - Batteries
+      - doc-gen4
+      - import-graph
+
+  - name: REPL
+    url: https://github.com/leanprover-community/repl
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies:
+      - Mathlib