diff --git a/.claude/commands/release.md b/.claude/commands/release.md index b0b38c876a..06e7dfd06a 100644 --- a/.claude/commands/release.md +++ b/.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 --repo /` to see which specific check failed +2. Run `gh run view --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: diff --git a/script/release_checklist.py b/script/release_checklist.py index 95c7a13dce..721315db76 100755 --- a/script/release_checklist.py +++ b/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):