chore: improve CI failure reporting in release checklist (#12786)

This PR fixes `release_checklist.py` to report failing CI checks
immediately, even when other checks are still in progress. Previously,
having any in-progress checks would return `"pending"` status, masking
failures that had already occurred. Now it returns `"failure"` with a
message like `"1 check(s) failing, 2 still in progress"`.

Also adds a section to `.claude/commands/release.md` instructing the AI
assistant to investigate any CI failure immediately rather than
reporting it as "in progress" and moving on.

🤖 Prepared with Claude Code

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>

.claude/commands/release.md

@@ -121,6 +121,24 @@ The nightly build system uses branches and tags across two repositories:
 
 When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
 
+## CI Failures: Investigate Immediately
+
+**CRITICAL: If the checklist reports `❌ CI: X check(s) failing` for any PR, investigate immediately.**
+
+Do NOT:
+- Report it as "CI in progress" or "some checks pending"
+- Wait for the remaining checks to finish before investigating
+- Assume it's a transient failure without checking
+
+DO:
+1. Run `gh pr checks <number> --repo <owner>/<repo>` to see which specific check failed
+2. Run `gh run view <run-id> --repo <owner>/<repo> --log-failed` to see the failure output
+3. Diagnose the failure and report clearly to the user: what failed and why
+4. Propose a fix if one is obvious (e.g., subverso version mismatch, transient elan install error)
+
+The checklist now distinguishes `❌ X check(s) failing, Y still in progress` from `🔄 Y check(s) in progress`.
+Any `❌` in CI status requires immediate investigation — do not move on.
+
 ## Waiting for CI or Merges
 
 Use `gh pr checks --watch` to block until a PR's CI checks complete (no polling needed).
@@ -135,6 +153,10 @@ For multiple PRs, launch one background command per PR in parallel. When each co
 you'll be notified automatically via a task-notification. Do NOT use sleep-based polling
 loops — `--watch` is event-driven and exits as soon as checks finish.
 
+Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail). If some checks
+fail while others are still running, `--watch` will continue until everything settles, then exit
+with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
+
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

script/release_checklist.py

@@ -11,7 +11,7 @@ IMPORTANT: Keep this documentation up-to-date when modifying the script's behavi
 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
+   - Verifies CMake version settings are correct (both src/ and stage0/)
    - Confirms the release tag exists
    - Validates the release page exists on GitHub (created automatically by CI after tag push)
    - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
@@ -311,21 +311,56 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
         print(f"  ❌ Could not retrieve {cmake_file_path} from {branch}")
         return False
 
-    expected_prefixes = [
-        f"set(LEAN_VERSION_MAJOR {version_major}",
-        f"set(LEAN_VERSION_MINOR {version_minor}",
-        f"set(LEAN_VERSION_PATCH 0",
-        f"set(LEAN_VERSION_IS_RELEASE 1"
+    expected_lines = [
+        f"set(LEAN_VERSION_MAJOR {version_major})",
+        f"set(LEAN_VERSION_MINOR {version_minor})",
+        f"set(LEAN_VERSION_PATCH 0)",
+        f"set(LEAN_VERSION_IS_RELEASE 1)"
     ]
 
-    for prefix in expected_prefixes:
-        if not any(l.strip().startswith(prefix) for l in content.splitlines()):
-            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {prefix}...)")
+    for line in expected_lines:
+        if not any(l.strip().startswith(line) for l in content.splitlines()):
+            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {line}")
             return False
 
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
     return True
 
+def check_stage0_version(repo_url, branch, version_major, version_minor, github_token):
+    """Verify that stage0/src/CMakeLists.txt has the same version as src/CMakeLists.txt.
+
+    The stage0 pre-built binaries stamp .olean headers with their baked-in version.
+    If stage0 has a different version (e.g. from a 'begin development cycle' bump),
+    the release tarball will contain .olean files with the wrong version.
+    """
+    stage0_cmake = "stage0/src/CMakeLists.txt"
+    content = get_branch_content(repo_url, branch, stage0_cmake, github_token)
+    if content is None:
+        print(f"  ❌ Could not retrieve {stage0_cmake} from {branch}")
+        return False
+
+    errors = []
+    for line in content.splitlines():
+        stripped = line.strip()
+        if stripped.startswith("set(LEAN_VERSION_MAJOR "):
+            actual = stripped.split()[-1].rstrip(")")
+            if actual != str(version_major):
+                errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
+        elif stripped.startswith("set(LEAN_VERSION_MINOR "):
+            actual = stripped.split()[-1].rstrip(")")
+            if actual != str(version_minor):
+                errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
+
+    if errors:
+        print(f"  ❌ stage0 version mismatch in {stage0_cmake}:")
+        for error in errors:
+            print(f"     {error}")
+        print(f"     The stage0 compiler stamps .olean headers with its baked-in version.")
+        print(f"     Run `make update-stage0` to rebuild stage0 with the correct version.")
+        return False
+
+    print(f"  ✅ stage0 version matches in {stage0_cmake}")
+    return True
 
 def extract_org_repo_from_url(repo_url):
     """Extract the 'org/repo' part from a GitHub URL."""
@@ -442,7 +477,10 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     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']]
 
+    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
     if in_progress:
+        if failed > 0:
+            return "failure", f"{failed} check(s) failing, {len(in_progress)} still in progress"
         return "pending", f"{len(in_progress)} check(s) in progress"
 
     if not conclusions:
@@ -451,7 +489,6 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     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"
 
@@ -681,6 +718,9 @@ def main():
         # Check CMake version settings
         if not check_cmake_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
             lean4_success = False
+        # Check that stage0 version matches (stage0 stamps .olean headers with its version)
+        if not check_stage0_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
+            lean4_success = False
 
     # Check for tag and release page
     if not tag_exists(lean_repo_url, toolchain, github_token):