feat: improvements to release automation

Author: kim-em

.claude/commands/release.md

@@ -0,0 +1,57 @@
+# Release Management Command
+
+Execute the release process for a given version by running the release checklist and following its instructions.
+
+## Before Starting
+
+**IMPORTANT**: Before beginning the release process, read the in-file documentation:
+- Read `script/release_checklist.py` for what the checklist script does
+- Read `script/release_steps.py` for what the release steps script does
+
+These comments explain the scripts' behavior, which repositories get special handling, and how errors are handled.
+
+## Arguments
+- `version`: The version to release (e.g., v4.24.0)
+
+## Process
+
+1. Run `script/release_checklist.py {version}` to check the current status
+2. Create a todo list tracking all repositories that need updates
+3. For each repository that needs updating:
+   - Run `script/release_steps.py {version} {repo_name}` to create the PR
+   - Mark it complete when the PR is created
+4. After creating PRs, notify the user which PRs need review and merging
+5. Continuously rerun `script/release_checklist.py {version}` to check progress
+6. As PRs are merged, dependent repositories will become ready - create PRs for those as well
+7. Continue until all repositories are updated and the release is complete
+
+## Important Notes
+
+- The `release_steps.py` script is idempotent - it's safe to rerun
+- The `release_checklist.py` script is idempotent - it's safe to rerun
+- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)
+- Wait for user to merge PRs before dependent repos can be updated
+- Alert user if anything unusual or scary happens
+- Use appropriate timeouts for long-running builds (verso can take 10+ minutes)
+- ProofWidgets4 uses semantic versioning (v0.0.X) - it's okay to create and push the next sequential tag yourself when needed for a release
+
+## PR Status Reporting
+
+Every time you run `release_checklist.py`, you MUST:
+1. Parse the output to identify ALL open PRs mentioned (lines with "✅ PR with title ... exists")
+2. Provide a summary to the user listing ALL open PRs that need review
+3. Group them by status:
+   - PRs for repositories that are blocked by dependencies (show these but note they're blocked)
+   - PRs for repositories that are ready to merge (highlight these)
+4. Format the summary clearly with PR numbers and URLs
+
+This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
+The user needs to see the complete picture of what's waiting for review.
+
+## Error Handling
+
+**CRITICAL**: If something goes wrong or a command fails:
+- **DO NOT** try to manually reproduce the failing steps yourself
+- **DO NOT** try to fix things by running git commands or other manual operations
+- Both scripts are idempotent and designed to handle partial completion gracefully
+- If a script continues to fail after retrying, report the error to the user and wait for instructions

script/release_checklist.py

@@ -1,5 +1,51 @@
 #!/usr/bin/env python3
 
+"""
+Release Checklist for Lean4 and Downstream Repositories
+
+This script validates the status of a Lean4 release across all dependent repositories.
+It checks whether repositories are ready for release and identifies missing steps.
+
+IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
+
+What this script does:
+1. Validates preliminary Lean4 release infrastructure:
+   - Checks that the release branch (releases/vX.Y.0) exists
+   - Verifies CMake version settings are correct
+   - Confirms the release tag exists
+   - Validates the release page exists on GitHub
+   - Checks the release notes page on lean-lang.org
+
+2. For each downstream repository (batteries, mathlib4, etc.):
+   - Checks if dependencies are ready (e.g., mathlib4 depends on batteries)
+   - Verifies the main branch is on the target toolchain (or newer)
+   - Checks if a PR exists to bump the toolchain (if not yet updated)
+   - Validates tags exist for the release version
+   - Ensures tags are merged into stable branches (for non-RC releases)
+   - Verifies bump branches exist and are configured correctly
+   - Special handling for ProofWidgets4 release tags
+
+3. Optionally automates missing steps (when not in --dry-run mode):
+   - Creates missing release tags using push_repo_release_tag.py
+   - Merges tags into stable branches using merge_remote.py
+
+Usage:
+    ./release_checklist.py v4.24.0           # Check release status
+    ./release_checklist.py v4.24.0 --verbose # Show detailed debug info
+    ./release_checklist.py v4.24.0 --dry-run # Check only, don't execute fixes
+
+For automated release management with Claude Code:
+    /release v4.24.0                 # Run full release process with Claude
+
+The script reads repository configurations from release_repos.yml and reports:
+- ✅ for completed requirements
+- ❌ for missing requirements (with instructions to fix)
+- 🟡 for repositories waiting on dependencies
+- ⮕ for automated actions being taken
+
+This script is idempotent and safe to rerun multiple times.
+"""
+
 import argparse
 import yaml
 import requests
@@ -286,6 +332,68 @@ def check_bump_branch_toolchain(url, bump_branch, github_token):
     print(f"  ✅ Bump branch correctly uses toolchain: {content}")
     return True
 
+def get_pr_ci_status(repo_url, pr_number, github_token):
+    """Get the CI status for a pull request."""
+    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    # Get PR details to find the head SHA
+    pr_response = requests.get(f"{api_base}/pulls/{pr_number}", headers=headers)
+    if pr_response.status_code != 200:
+        return "unknown", "Could not fetch PR details"
+
+    pr_data = pr_response.json()
+    head_sha = pr_data['head']['sha']
+
+    # Get check runs for the commit
+    check_runs_response = requests.get(
+        f"{api_base}/commits/{head_sha}/check-runs",
+        headers=headers
+    )
+
+    if check_runs_response.status_code != 200:
+        return "unknown", "Could not fetch check runs"
+
+    check_runs_data = check_runs_response.json()
+    check_runs = check_runs_data.get('check_runs', [])
+
+    if not check_runs:
+        # No check runs, check for status checks (legacy)
+        status_response = requests.get(
+            f"{api_base}/commits/{head_sha}/status",
+            headers=headers
+        )
+        if status_response.status_code == 200:
+            status_data = status_response.json()
+            state = status_data.get('state', 'unknown')
+            if state == 'success':
+                return "success", "All status checks passed"
+            elif state == 'failure':
+                return "failure", "Some status checks failed"
+            elif state == 'pending':
+                return "pending", "Status checks in progress"
+        return "unknown", "No CI checks found"
+
+    # Analyze check runs
+    conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
+    in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
+
+    if in_progress:
+        return "pending", f"{len(in_progress)} check(s) in progress"
+
+    if not conclusions:
+        return "pending", "Checks queued"
+
+    if all(c == 'success' for c in conclusions):
+        return "success", f"All {len(conclusions)} checks passed"
+
+    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
+    if failed > 0:
+        return "failure", f"{failed} check(s) failed"
+
+    # Some checks are cancelled, skipped, or neutral
+    return "warning", f"Some checks did not complete normally"
+
 def pr_exists_with_title(repo_url, title, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + "/pulls"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -471,6 +579,19 @@ def main():
             if pr_info:
                 pr_number, pr_url = pr_info
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
+
+                # Check CI status
+                ci_status, ci_message = get_pr_ci_status(url, pr_number, github_token)
+                if ci_status == "success":
+                    print(f"     ✅ CI: {ci_message}")
+                elif ci_status == "failure":
+                    print(f"     ❌ CI: {ci_message}")
+                elif ci_status == "pending":
+                    print(f"     🔄 CI: {ci_message}")
+                elif ci_status == "warning":
+                    print(f"     ⚠️  CI: {ci_message}")
+                else:
+                    print(f"     ❓ CI: {ci_message}")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
                 print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")

script/release_steps.py

@@ -1,30 +1,53 @@
 #!/usr/bin/env python3
 
 """
-Execute release steps for Lean4 repositories.
+Execute Release Steps for Lean4 Downstream Repositories
 
-This script helps automate the release process for Lean4 and its dependent repositories
-by actually executing the step-by-step instructions for updating toolchains, creating tags,
-and managing branches.
+This script automates the process of updating a downstream repository to a new Lean4 release.
+It handles creating branches, updating toolchains, merging changes, building, testing, and
+creating pull requests.
+
+IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
+
+What this script does:
+1. Sets up the downstream_releases/ directory for cloning repositories
+
+2. Clones or updates the target repository
+
+3. Creates a branch named bump_to_{version} for the changes
+
+4. Updates the lean-toolchain file to the target version
+
+5. Handles repository-specific variations:
+   - Different dependency update mechanisms
+   - Special merging strategies for repositories with nightly-testing branches
+   - Safety checks for repositories using bump branches
+   - Custom build and test procedures
+
+6. Commits the changes with message "chore: bump toolchain to {version}"
+
+7. Builds the project (with a clean .lake cache)
+
+8. Runs tests if available
+
+9. Pushes the branch to GitHub
+
+10. Creates a pull request (or reports if one already exists)
 
 Usage:
-    python3 release_steps.py <version> <repo>
-
-Arguments:
-    version: The version to set in the lean-toolchain file (e.g., v4.6.0)
-    repo: The repository name as specified in release_repos.yml
-
-Example:
-    python3 release_steps.py v4.6.0 mathlib4
-    python3 release_steps.py v4.6.0 batteries
-
-The script reads repository configurations from release_repos.yml in the same directory.
-Each repository may have specific requirements for:
-- Branch management
-- Toolchain updates
-- Dependency updates
-- Tagging conventions
-- Stable branch handling
+    ./release_steps.py v4.24.0 batteries    # Update batteries to v4.24.0
+    ./release_steps.py v4.24.0-rc1 mathlib4 # Update mathlib4 to v4.24.0-rc1
+
+The script reads repository configurations from release_repos.yml.
+Each repository has specific handling for merging, dependencies, and testing.
+
+This script is idempotent - it's safe to rerun if it fails partway through.
+Existing branches, commits, and PRs will be reused rather than duplicated.
+
+Error handling:
+- If build or tests fail, the script continues to create the PR anyway
+- Manual conflicts must be resolved by the user
+- Network issues during push/PR creation are reported with manual instructions
 """
 
 import argparse