lean4/script/release_steps.py

#!/usr/bin/env python3

"""
Execute Release Steps for Lean4 Downstream Repositories

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
   - lean-fro.org: runs scripts/update.sh to regenerate site content
   - mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y)

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:
    ./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
import yaml
import os
import sys
import re
import subprocess
import shutil
import json
import requests
import base64
from pathlib import Path

# Color functions for terminal output
def blue(text):
    """Blue text for 'I'm doing something' messages."""
    return f"\033[94m{text}\033[0m"

def green(text):
    """Green text for 'successful step' messages."""
    return f"\033[92m{text}\033[0m"

def red(text):
    """Red text for 'this looks bad' messages."""
    return f"\033[91m{text}\033[0m"

def yellow(text):
    """Yellow text for warnings."""
    return f"\033[93m{text}\033[0m"

def run_command(cmd, cwd=None, check=True, stream_output=False):
    """Run a shell command and return the result."""
    print(blue(f"Running: {cmd}"))
    try:
        if stream_output:
            # Stream output in real-time for long-running commands
            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, text=True)
            return result
        else:
            # Capture output for commands where we need to process the result
            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, 
                                  capture_output=True, text=True)
            if result.stdout:
                # Command output in plain white (default terminal color)
                print(result.stdout)
            return result
    except subprocess.CalledProcessError as e:
        print(red(f"Error running command: {cmd}"))
        print(red(f"Exit code: {e.returncode}"))
        if not stream_output:
            print(f"Stdout: {e.stdout}")
            print(f"Stderr: {e.stderr}")
        raise

def load_repos_config(file_path):
    with open(file_path, "r") as f:
        return yaml.safe_load(f)["repositories"]

def find_repo(repo_name, config):
    matching_repos = [r for r in config if r["name"] == repo_name]
    if not matching_repos:
        print(red(f"Error: No repository named '{repo_name}' found in configuration."))
        available_repos = [r["name"] for r in config]
        print(yellow(f"Available repositories: {', '.join(available_repos)}"))
        sys.exit(1)
    return matching_repos[0]

def get_github_token():
    try:
        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
        if result.returncode == 0:
            return result.stdout.strip()
    except FileNotFoundError:
        pass
    return None

def find_proofwidgets_tag(version):
    """Find the latest ProofWidgets4 tag that uses the given toolchain version.

    ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags.
    This function finds the most recent tag whose lean-toolchain matches the target version
    exactly, checking the 20 most recent tags.
    """
    github_token = get_github_token()
    api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4"
    headers = {'Authorization': f'token {github_token}'} if github_token else {}

    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30)
    if response.status_code != 200:
        return None

    tags = response.json()
    tag_names = []
    for tag in tags:
        ref = tag['ref']
        if ref.startswith('refs/tags/v0.0.'):
            tag_name = ref.replace('refs/tags/', '')
            try:
                version_num = int(tag_name.split('.')[-1])
                tag_names.append((version_num, tag_name))
            except (ValueError, IndexError):
                continue

    if not tag_names:
        return None

    # Sort by version number (descending) and check recent tags
    tag_names.sort(reverse=True)
    target = f"leanprover/lean4:{version}"
    for _, tag_name in tag_names[:20]:
        # Fetch lean-toolchain for this tag
        api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}"
        resp = requests.get(api_url, headers=headers, timeout=30)
        if resp.status_code != 200:
            continue
        content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip()
        if content == target:
            return tag_name

    return None

def setup_downstream_releases_dir():
    """Create the downstream_releases directory if it doesn't exist."""
    downstream_dir = Path("downstream_releases")
    if not downstream_dir.exists():
        print(blue(f"Creating {downstream_dir} directory..."))
        downstream_dir.mkdir()
        print(green(f"Created {downstream_dir} directory"))
    return downstream_dir

def clone_or_update_repo(repo_url, repo_dir, downstream_dir):
    """Clone the repository if it doesn't exist, or update it if it does."""
    repo_path = downstream_dir / repo_dir
    
    if repo_path.exists():
        print(blue(f"Repository {repo_dir} already exists, updating..."))
        run_command("git fetch", cwd=repo_path)
        print(green(f"Updated repository {repo_dir}"))
    else:
        print(blue(f"Cloning {repo_url} to {repo_path}..."))
        run_command(f"git clone {repo_url}", cwd=downstream_dir)
        print(green(f"Cloned repository {repo_dir}"))
    
    return repo_path

def get_remotes_for_repo(repo_name):
    """Get the appropriate remotes for bump and nightly-testing branches based on repository."""
    if repo_name == "mathlib4":
        return "nightly-testing", "nightly-testing"
    else:
        return "origin", "origin"

def check_and_abort_merge(repo_path):
    """Check if repository is in the middle of a merge and abort it if so."""
    merge_head_file = repo_path / ".git" / "MERGE_HEAD"
    
    if merge_head_file.exists():
        print(yellow(f"Repository {repo_path.name} is in the middle of a merge. Aborting merge..."))
        run_command("git merge --abort", cwd=repo_path)
        print(green("Merge aborted successfully"))
        return True
    
    # Also check git status for other merge-related states
    try:
        result = run_command("git status --porcelain=v1", cwd=repo_path, check=False)
        if result.returncode == 0:
            # Check for unmerged paths (indicated by 'UU', 'AA', etc. in git status)
            for line in result.stdout.splitlines():
                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
                    print(yellow(f"Repository {repo_path.name} has unmerged paths. Aborting merge..."))
                    run_command("git merge --abort", cwd=repo_path)
                    print(green("Merge aborted successfully"))
                    return True
    except subprocess.CalledProcessError:
        # If git status fails, we'll let the main process handle it
        pass
    
    return False

def execute_release_steps(repo, version, config):
    repo_config = find_repo(repo, config)
    repo_name = repo_config['name']
    repo_url = repo_config['url']
    # Extract the last component of the URL, removing the .git extension if present
    repo_dir = repo_url.split('/')[-1].replace('.git', '')
    default_branch = repo_config.get("branch", "main")
    dependencies = repo_config.get("dependencies", [])
    requires_tagging = repo_config.get("toolchain-tag", True)
    has_stable_branch = repo_config.get("stable-branch", True)

    # Setup downstream releases directory
    downstream_dir = setup_downstream_releases_dir()
    
    # Clone or update the repository
    repo_path = clone_or_update_repo(repo_url, repo_dir, downstream_dir)
    
    # Special remote setup for mathlib4
    if repo_name == "mathlib4":
        print(blue("Setting up special remotes for mathlib4..."))
        try:
            # Check if nightly-testing remote already exists
            result = run_command("git remote get-url nightly-testing", cwd=repo_path, check=False)
            if result.returncode != 0:
                # Add the nightly-testing remote
                run_command("git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git", cwd=repo_path)
                print(green("Added nightly-testing remote"))
            else:
                print(green("nightly-testing remote already exists"))
            
            # Fetch from the nightly-testing remote
            run_command("git fetch nightly-testing", cwd=repo_path)
            print(green("Fetched from nightly-testing remote"))
        except subprocess.CalledProcessError as e:
            print(red(f"Error setting up mathlib4 remotes: {e}"))
            print(yellow("Continuing with default remote setup..."))
    
    print(blue(f"\n=== Executing release steps for {repo_name} ==="))
    
    # Check if repository is in the middle of a merge and abort it if necessary
    check_and_abort_merge(repo_path)
    
    # Execute the release steps
    run_command(f"git checkout {default_branch} && git pull", cwd=repo_path)
    
    # Special rc1 safety check for batteries and mathlib4 (before creating any branches)
    if repo_name in ["batteries", "mathlib4"] and version.endswith('-rc1'):
        print(blue("This repo has nightly-testing infrastructure"))
        print(blue(f"Checking if nightly-testing can be safely merged into bump/{version.split('-rc')[0]}..."))
        
        # Get the base version (e.g., v4.6.0 from v4.6.0-rc1)
        base_version = version.split('-rc')[0]
        bump_branch = f"bump/{base_version}"
        
        # Determine which remote to use for bump and nightly-testing branches
        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
        
        try:
            # Fetch latest changes from the appropriate remote
            run_command(f"git fetch {bump_remote}", cwd=repo_path)
            
            # Check if the bump branch exists
            result = run_command(f"git show-ref --verify --quiet refs/remotes/{bump_remote}/{bump_branch}", cwd=repo_path, check=False)
            if result.returncode != 0:
                print(red(f"Bump branch {bump_remote}/{bump_branch} does not exist. Cannot perform safety check."))
                print(yellow("Please ensure the bump branch exists before proceeding."))
                return
            
            # Create a temporary branch for testing the merge
            temp_branch = f"temp-merge-test-{base_version}"
            
            # Clean up any existing temp branch from previous runs
            result = run_command(f"git show-ref --verify --quiet refs/heads/{temp_branch}", cwd=repo_path, check=False)
            if result.returncode == 0:
                print(blue(f"Cleaning up existing temp branch {temp_branch}..."))
                # Make sure we're not on the temp branch before deleting it
                run_command(f"git checkout {default_branch}", cwd=repo_path)
                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
                print(green(f"Deleted existing temp branch {temp_branch}"))
            
            run_command(f"git checkout -b {temp_branch} {bump_remote}/{bump_branch}", cwd=repo_path)
            
            # Try to merge nightly-testing
            try:
                run_command(f"git merge {nightly_remote}/nightly-testing", cwd=repo_path)
                
                # Check what files have changed compared to the bump branch
                changed_files = run_command(f"git diff --name-only {bump_remote}/{bump_branch}..HEAD", cwd=repo_path)
                
                # Filter out allowed changes
                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
                problematic_files = []
                
                for file in changed_files.stdout.strip().split('\n'):
                    if file.strip():  # Skip empty lines
                        is_allowed = any(pattern in file for pattern in allowed_patterns)
                        if not is_allowed:
                            problematic_files.append(file)
                
                # Clean up temporary branch and return to default branch
                run_command(f"git checkout {default_branch}", cwd=repo_path)
                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
                
                if problematic_files:
                    print(red("❌ Safety check failed!"))
                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
                    for file in problematic_files:
                        print(red(f"  - {file}"))
                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
                    return
                else:
                    print(green("✅ Safety check passed - only lean-toolchain and/or lake-manifest.json would change"))
                    
            except subprocess.CalledProcessError:
                # Merge failed due to conflicts - check which files are conflicted
                print(blue("Merge failed, checking which files are affected..."))
                
                # Get all changed files using git status
                status_result = run_command("git status --porcelain", cwd=repo_path)
                changed_files = []
                
                for line in status_result.stdout.splitlines():
                    if line.strip():  # Skip empty lines
                        # Extract filename (skip the first 3 characters which are status codes)
                        changed_files.append(line[3:])
                
                # Filter out allowed files
                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
                problematic_files = []
                
                for file in changed_files:
                    is_allowed = any(pattern in file for pattern in allowed_patterns)
                    if not is_allowed:
                        problematic_files.append(file)
                
                if problematic_files:
                    # There are changes in non-allowed files - fail the safety check
                    # First abort the merge to clean up the conflicted state
                    run_command("git merge --abort", cwd=repo_path)
                    run_command(f"git checkout {default_branch}", cwd=repo_path)
                    run_command(f"git branch -D {temp_branch}", cwd=repo_path)
                    print(red("❌ Safety check failed!"))
                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
                    for file in problematic_files:
                        print(red(f"  - {file}"))
                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
                    return
                else:
                    # Only allowed files are changed - resolve them and continue
                    print(green(f"✅ Only allowed files changed: {', '.join(changed_files)}"))
                    print(blue("Resolving conflicts by taking nightly-testing version..."))
                    
                    # For each changed allowed file, take the nightly-testing version
                    for file in changed_files:
                        run_command(f"git checkout --theirs {file}", cwd=repo_path)
                    
                    # Complete the merge
                    run_command("git add .", cwd=repo_path)
                    run_command("git commit --no-edit", cwd=repo_path)
                    
                    print(green("✅ Safety check passed - changes only in allowed files"))
                
                # Clean up temporary branch and return to default branch
                run_command(f"git checkout {default_branch}", cwd=repo_path)
                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
                
        except subprocess.CalledProcessError as e:
            # Ensure we're back on the default branch even if setup failed
            try:
                run_command(f"git checkout {default_branch}", cwd=repo_path)
            except subprocess.CalledProcessError:
                print(red(f"Cannot return to {default_branch} branch. Repository is in an inconsistent state."))
                print(red("Please manually check the repository state and fix any issues."))
                return
            print(red(f"Error during safety check: {e}"))
            print(yellow("Skipping safety check and proceeding with normal merge..."))
    
    # Check if the branch already exists
    branch_name = f"bump_to_{version}"
    try:
        # Check if branch exists locally
        result = run_command(f"git show-ref --verify --quiet refs/heads/{branch_name}", cwd=repo_path, check=False)
        if result.returncode == 0:
            print(blue(f"Branch {branch_name} already exists, checking it out..."))
            run_command(f"git checkout {branch_name}", cwd=repo_path)
            print(green(f"Checked out existing branch {branch_name}"))
        else:
            print(blue(f"Creating new branch {branch_name}..."))
            run_command(f"git checkout -b {branch_name}", cwd=repo_path)
            print(green(f"Created new branch {branch_name}"))
    except subprocess.CalledProcessError:
        print(blue(f"Creating new branch {branch_name}..."))
        run_command(f"git checkout -b {branch_name}", cwd=repo_path)
        print(green(f"Created new branch {branch_name}"))
    
    # Update lean-toolchain
    print(blue("Updating lean-toolchain file..."))
    toolchain_file = repo_path / "lean-toolchain"
    with open(toolchain_file, "w") as f:
        f.write(f"leanprover/lean4:{version}\n")
    print(green(f"Updated lean-toolchain to leanprover/lean4:{version}"))

    # Special cases for specific repositories
    if repo_name == "repl":
        run_command("lake update", cwd=repo_path, stream_output=True)
        mathlib_test_dir = repo_path / "test" / "Mathlib"
        run_command(f'perl -pi -e \'s/rev = "v\\d+\\.\\d+\\.\\d+(-rc\\d+)?"/rev = "{version}"/g\' lakefile.toml', cwd=mathlib_test_dir)
        
        # Update lean-toolchain in test/Mathlib
        print(blue("Updating test/Mathlib/lean-toolchain..."))
        mathlib_toolchain = mathlib_test_dir / "lean-toolchain"
        with open(mathlib_toolchain, "w") as f:
            f.write(f"leanprover/lean4:{version}\n")
        print(green(f"Updated test/Mathlib/lean-toolchain to leanprover/lean4:{version}"))
        
        run_command("lake update", cwd=mathlib_test_dir, stream_output=True)
        try:
            result = run_command("./test.sh", cwd=repo_path, stream_output=True, check=False)
            if result.returncode == 0:
                print(green("Tests completed successfully"))
            else:
                print(red("Tests failed, but continuing with PR creation..."))
                print(red(f"Test exit code: {result.returncode}"))
        except subprocess.CalledProcessError as e:
            print(red("Tests failed, but continuing with PR creation..."))
            print(red(f"Test error: {e}"))
    elif repo_name == "lean-fro.org":
        # Update lean-toolchain in examples/hero
        print(blue("Updating examples/hero/lean-toolchain..."))
        docs_toolchain = repo_path / "examples" / "hero" / "lean-toolchain"
        with open(docs_toolchain, "w") as f:
            f.write(f"leanprover/lean4:{version}\n")
        print(green(f"Updated examples/hero/lean-toolchain to leanprover/lean4:{version}"))

        print(blue("Running `lake update`..."))
        run_command("lake update", cwd=repo_path, stream_output=True)
        print(blue("Running `lake update` in examples/hero..."))
        run_command("lake update", cwd=repo_path / "examples" / "hero", stream_output=True)

        # Run scripts/update.sh to regenerate content
        print(blue("Running `scripts/update.sh` to regenerate content..."))
        run_command("scripts/update.sh", cwd=repo_path, stream_output=True)
        print(green("Content regenerated successfully"))
    elif repo_name == "cslib":
        print(blue("Updating lakefile.toml..."))
        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
        run_command("lake update", cwd=repo_path, stream_output=True)
    elif repo_name == "verso":
        # verso has nested Lake projects in test-projects/ that each have their own
        # lake-manifest.json with a subverso pin. After updating the root manifest via
        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
        run_command("lake update", cwd=repo_path, stream_output=True)
        print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
        sync_script = (
            'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
            'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
            'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
            'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do '
            'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; '
            'done'
        )
        run_command(sync_script, cwd=repo_path)
        print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
    elif dependencies:
        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
        run_command("lake update", cwd=repo_path, stream_output=True)

    # For reference-manual, update the release notes title to match the target version.
    # e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
    # e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
    if repo_name == "reference-manual":
        base_version = version.lstrip('v').split('-')[0]  # "4.28.0"
        file_name = f"v{base_version.replace('.', '_')}.lean"
        release_notes_file = repo_path / "Manual" / "Releases" / file_name

        if release_notes_file.exists():
            is_rc = "-rc" in version
            if is_rc:
                # For RC releases, update to the exact RC version
                display_version = version.lstrip('v')  # "4.28.0-rc2"
            else:
                # For stable releases, strip any RC suffix
                display_version = base_version  # "4.28.0"

            print(blue(f"Updating release notes title in {file_name}..."))
            content = release_notes_file.read_text()
            # Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
            new_content = re.sub(
                r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
                rf'\g<1>{display_version}\3',
                content
            )
            if new_content != content:
                release_notes_file.write_text(new_content)
                print(green(f"Updated release notes title to Lean {display_version}"))
            else:
                print(green("Release notes title already correct"))
        else:
            print(yellow(f"Release notes file {file_name} not found, skipping title update"))

    # For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
    if repo_name == "mathlib4":
        print(blue("Checking ProofWidgets4 version pin..."))
        pw_tag = find_proofwidgets_tag(version)
        if pw_tag:
            print(blue(f"Updating ProofWidgets4 pin to {pw_tag}..."))
            for lakefile in repo_path.glob("lakefile.*"):
                content = lakefile.read_text()
                # Only update the ProofWidgets4 dependency line, not other v0.0.X pins
                new_content = re.sub(
                    r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")',
                    rf'\g<1>{pw_tag.removeprefix("v")}\2',
                    content
                )
                if new_content != content:
                    lakefile.write_text(new_content)
                    print(green(f"Updated ProofWidgets4 pin in {lakefile.name}"))
            run_command("lake update proofwidgets", cwd=repo_path, stream_output=True)
            print(green(f"Updated ProofWidgets4 to {pw_tag}"))
        else:
            print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}"))
            print(yellow("You may need to update the ProofWidgets4 pin manually"))

    # Commit changes (only if there are changes)
    print(blue("Checking for changes to commit..."))
    try:
        # Check if there are any changes to commit (staged or unstaged)
        result = run_command("git status --porcelain", cwd=repo_path, check=False)
        if result.stdout.strip():  # There are changes
            print(blue("Committing changes..."))
            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
            print(green(f"Committed changes: chore: bump toolchain to {version}"))
        else:
            print(green("No changes to commit - toolchain already up to date"))
    except subprocess.CalledProcessError:
        print(yellow("Failed to check for changes, attempting commit anyway..."))
        try:
            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
        except subprocess.CalledProcessError as e:
            if "nothing to commit" in e.stderr:
                print(green("No changes to commit - toolchain already up to date"))
            else:
                raise

    # Handle special merging cases
    if version.endswith('-rc1') and repo_name in ["batteries", "mathlib4"]:
        print(blue("This repo uses `bump/v4.X.0` branches for reviewed content from nightly-testing."))
        
        # Determine which remote to use for bump branches
        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
        
        # Fetch latest changes to ensure we have the most up-to-date bump branch
        print(blue(f"Fetching latest changes from {bump_remote}..."))
        run_command(f"git fetch {bump_remote}", cwd=repo_path)
        
        try:
            print(blue(f"Merging {bump_remote}/bump/{version.split('-rc')[0]}..."))
            run_command(f"git merge {bump_remote}/bump/{version.split('-rc')[0]}", cwd=repo_path)
            print(green("Merge completed successfully"))
        except subprocess.CalledProcessError:
            # Merge failed due to conflicts - check which files are conflicted
            print(blue("Merge conflicts detected, checking which files are affected..."))
            
            # Get conflicted files using git status
            status_result = run_command("git status --porcelain", cwd=repo_path)
            conflicted_files = []
            
            for line in status_result.stdout.splitlines():
                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
                    # Extract filename (skip the first 3 characters which are status codes)
                    conflicted_files.append(line[3:])
            
            # Filter out allowed files
            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
            problematic_files = []
            
            for file in conflicted_files:
                is_allowed = any(pattern in file for pattern in allowed_patterns)
                if not is_allowed:
                    problematic_files.append(file)
            
            if problematic_files:
                # There are conflicts in non-allowed files - fail
                print(red("❌ Merge failed!"))
                print(red(f"Merging {bump_remote}/bump/{version.split('-rc')[0]} resulted in conflicts in:"))
                for file in problematic_files:
                    print(red(f"  - {file}"))
                print(red("Please resolve these conflicts manually."))
                return
            else:
                # Only allowed files are conflicted - resolve them automatically
                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
                print(blue("Resolving conflicts automatically..."))
                
                # Overwrite lean-toolchain with our target version
                if 'lean-toolchain' in conflicted_files:
                    print(blue(f"Overwriting lean-toolchain with target version {version}"))
                    toolchain_file = repo_path / "lean-toolchain"
                    with open(toolchain_file, "w") as f:
                        f.write(f"leanprover/lean4:{version}\n")
                
                # For other allowed files, take our version (since we want our changes)
                for file in conflicted_files:
                    if file != 'lean-toolchain':
                        run_command(f"git checkout --ours {file}", cwd=repo_path)
                
                # Run lake update to rebuild lake-manifest.json
                print(blue("Running lake update to rebuild lake-manifest.json..."))
                run_command("lake update", cwd=repo_path, stream_output=True)
                
                # Complete the merge
                run_command("git add .", cwd=repo_path)
                run_command("git commit --no-edit", cwd=repo_path)
                
                print(green("✅ Merge completed successfully with automatic conflict resolution"))
    
    elif version.endswith('-rc1'):
        # For all other repos with rc versions, merge nightly-testing
        if repo_name in ["verso", "reference-manual"]:
            print(yellow("This repo does development on nightly-testing: remember to rebase merge the PR."))
        
        # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
        print(blue("Fetching latest changes from origin..."))
        run_command("git fetch origin", cwd=repo_path)
        
        try:
            print(blue("Merging origin/nightly-testing..."))
            run_command("git merge origin/nightly-testing", cwd=repo_path)
            print(green("Merge completed successfully"))
        except subprocess.CalledProcessError:
            # Merge failed due to conflicts - check which files are conflicted
            print(blue("Merge conflicts detected, checking which files are affected..."))
            
            # Get conflicted files using git status
            status_result = run_command("git status --porcelain", cwd=repo_path)
            conflicted_files = []
            
            for line in status_result.stdout.splitlines():
                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
                    # Extract filename (skip the first 3 characters which are status codes)
                    conflicted_files.append(line[3:])
            
            # Filter out allowed files
            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
            problematic_files = []
            
            for file in conflicted_files:
                is_allowed = any(pattern in file for pattern in allowed_patterns)
                if not is_allowed:
                    problematic_files.append(file)
            
            if problematic_files:
                # There are conflicts in non-allowed files - fail
                print(red("❌ Merge failed!"))
                print(red(f"Merging nightly-testing resulted in conflicts in:"))
                for file in problematic_files:
                    print(red(f"  - {file}"))
                print(red("Please resolve these conflicts manually."))
                return
            else:
                # Only allowed files are conflicted - resolve them automatically
                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
                print(blue("Resolving conflicts automatically..."))
                
                # For lean-toolchain and lake-manifest.json, keep our versions
                for file in conflicted_files:
                    print(blue(f"Keeping our version of {file}"))
                    run_command(f"git checkout --ours {file}", cwd=repo_path)
                
                # Complete the merge
                run_command("git add .", cwd=repo_path)
                run_command("git commit --no-edit", cwd=repo_path)
                
                print(green("✅ Merge completed successfully with automatic conflict resolution"))

    # Build and test (skip for Mathlib)
    if repo_name not in ["mathlib4"]:
        print(blue("Building project..."))
        
        # Clean lake cache for a fresh build
        print(blue("Cleaning lake cache..."))
        run_command("lake clean", cwd=repo_path)

        # Check if downstream of Mathlib and get cache if so
        mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib"
        if mathlib_package_dir.exists():
            print(blue("Project is downstream of Mathlib, fetching cache..."))
            try:
                run_command("lake exe cache get", cwd=repo_path, stream_output=True)
                print(green("Cache fetched successfully"))
            except subprocess.CalledProcessError as e:
                print(yellow("Failed to fetch cache, continuing anyway..."))
                print(yellow(f"Cache fetch error: {e}"))

        try:
            run_command("lake build", cwd=repo_path, stream_output=True)
            print(green("Build completed successfully"))
        except subprocess.CalledProcessError as e:
            print(red("Build failed, but continuing with PR creation..."))
            print(red(f"Build error: {e}"))
        
        # Check if lake check-test exists before running tests
        print(blue("Running tests..."))
        check_test_result = run_command("lake check-test", cwd=repo_path, check=False)
        if check_test_result.returncode == 0:
            try:
                run_command("lake test", cwd=repo_path, stream_output=True)
                print(green("Tests completed successfully"))
            except subprocess.CalledProcessError as e:
                print(red("Tests failed, but continuing with PR creation..."))
                print(red(f"Test error: {e}"))
        else:
            print(yellow("lake check-test reports that there is no test suite"))

    # Push the branch to remote before creating PR
    print(blue("Checking remote branch status..."))
    try:
        # Check if branch exists on remote
        result = run_command(f"git ls-remote --heads origin {branch_name}", cwd=repo_path, check=False)
        if not result.stdout.strip():
            print(blue(f"Pushing branch {branch_name} to remote..."))
            run_command(f"git push -u origin {branch_name}", cwd=repo_path)
            print(green(f"Successfully pushed branch {branch_name} to remote"))
        else:
            print(blue(f"Branch {branch_name} already exists on remote, pushing any new commits..."))
            run_command(f"git push", cwd=repo_path)
            print(green("Successfully pushed commits to remote"))
    except subprocess.CalledProcessError:
        print(red("Failed to push branch to remote. Please check your permissions and network connection."))
        print(yellow(f"You may need to run: git push -u origin {branch_name}"))
        return

    # Create pull request (only if one doesn't already exist)
    print(blue("Checking for existing pull request..."))
    try:
        # Check if PR already exists for this branch
        result = run_command(f'gh pr list --head {branch_name} --json number', cwd=repo_path, check=False)
        if result.returncode == 0 and result.stdout.strip() != "[]":
            print(green(f"Pull request already exists for branch {branch_name}"))
            # Get the PR URL
            pr_result = run_command(f'gh pr view {branch_name} --json url', cwd=repo_path, check=False)
            if pr_result.returncode == 0:
                pr_data = json.loads(pr_result.stdout)
                print(green(f"PR URL: {pr_data.get('url', 'N/A')}"))
        else:
            # Create new PR
            print(blue("Creating new pull request..."))
            run_command(f'gh pr create --title "chore: bump toolchain to {version}" --body ""', cwd=repo_path)
            print(green("Pull request created successfully!"))
    except subprocess.CalledProcessError:
        print(red("Failed to check for existing PR or create new PR."))
        print(yellow("This could be due to:"))
        print(yellow("1. GitHub CLI not authenticated"))
        print(yellow("2. No push permissions to the repository"))
        print(yellow("3. Network issues"))
        print(f"Branch: {branch_name}")
        print(f"Title: chore: bump toolchain to {version}")
        print(yellow("Please create the PR manually if needed."))

def main():
    parser = argparse.ArgumentParser(
        description="Execute release steps for Lean4 repositories.",
        formatter_class=argparse.RawDescriptionHelpFormatter,
        epilog="""
Examples:
  %(prog)s v4.6.0 mathlib4   Execute steps for updating Mathlib to v4.6.0
  %(prog)s v4.6.0 batteries  Execute steps for updating Batteries to v4.6.0
  
The script will:
1. Create a downstream_releases/ directory
2. Clone or update the target repository
3. Update the lean-toolchain file
4. Create appropriate branches and commits
5. Build and test the project
6. Create pull requests

(Note that the steps of creating toolchain version tags, and merging these into `stable` branches,
are handled by `script/release_checklist.py`.)
"""
    )
    parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
    parser.add_argument("repo", help="The repository name as specified in release_repos.yml")
    args = parser.parse_args()

    config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
    config = load_repos_config(config_path)

    execute_release_steps(args.repo, args.version, config)

if __name__ == "__main__":
    main()