diff --git a/script/merge_remote.py b/script/merge_remote.py new file mode 100755 index 0000000000..44032f73d8 --- /dev/null +++ b/script/merge_remote.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 + +""" +Merge a tag into a branch on a GitHub repository. + +This script checks if a specified tag can be merged cleanly into a branch and performs +the merge if possible. If the merge cannot be done cleanly, it prints a helpful message. + +Usage: + python3 merge_remote.py + +Arguments: + org/repo: GitHub repository in the format 'organization/repository' + branch: The target branch to merge into + tag: The tag to merge from + +Example: + python3 merge_remote.py leanprover/mathlib4 stable v4.6.0 + +The script uses the GitHub CLI (`gh`), so make sure it's installed and authenticated. +""" + +import argparse +import subprocess +import sys +import tempfile +import os +import shutil + + +def run_command(command, check=True, capture_output=True): + """Run a shell command and return the result.""" + try: + result = subprocess.run( + command, + check=check, + shell=True, + text=True, + capture_output=capture_output + ) + return result + except subprocess.CalledProcessError as e: + if capture_output: + print(f"Command failed: {command}") + print(f"Error: {e.stderr}") + return e + + +def clone_repo(repo, temp_dir): + """Clone the repository to a temporary directory using shallow clone.""" + print(f"Shallow cloning {repo}...") + # Use --depth=1 for shallow clone + clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False) + if clone_result.returncode != 0: + print(f"Failed to clone repository {repo}.") + print(f"Error: {clone_result.stderr}") + return False + return True + + +def check_and_merge(repo, branch, tag, temp_dir): + """Check if tag can be merged into branch and perform the merge if possible.""" + # Change to the temporary directory + os.chdir(temp_dir) + + # Fetch only the specific branch and tag we need + print(f"Fetching branch '{branch}' and tag '{tag}'...") + fetch_branch = run_command(f"git fetch origin {branch}") + if fetch_branch.returncode != 0: + print(f"Error: Failed to fetch branch '{branch}'.") + return False + + fetch_tag = run_command(f"git fetch origin tag {tag}") + if fetch_tag.returncode != 0: + print(f"Error: Failed to fetch tag '{tag}'.") + return False + + # Check if branch exists + branch_check = run_command(f"git branch -r | grep origin/{branch}") + if branch_check.returncode != 0: + print(f"Error: Branch '{branch}' does not exist in repository.") + return False + + # Check if tag exists + tag_check = run_command(f"git tag -l {tag}") + if tag_check.returncode != 0 or not tag_check.stdout.strip(): + print(f"Error: Tag '{tag}' does not exist in repository.") + return False + + # Checkout the branch + print(f"Checking out branch '{branch}'...") + checkout_result = run_command(f"git checkout -b {branch} origin/{branch}") + if checkout_result.returncode != 0: + return False + + # Try merging the tag in a dry-run to check if it can be merged cleanly + print(f"Checking if {tag} can be merged cleanly into {branch}...") + merge_check = run_command(f"git merge --no-commit --no-ff {tag}", check=False) + + if merge_check.returncode != 0: + print(f"Cannot merge {tag} cleanly into {branch}.") + print("Merge conflicts would occur. Aborting merge.") + run_command("git merge --abort") + return False + + # Abort the test merge + run_command("git reset --hard HEAD") + + # Now perform the actual merge and push to remote + print(f"Merging {tag} into {branch}...") + merge_result = run_command(f"git merge {tag} --no-edit") + if merge_result.returncode != 0: + print(f"Failed to merge {tag} into {branch}.") + return False + + print(f"Pushing changes to remote...") + push_result = run_command(f"git push origin {branch}") + if push_result.returncode != 0: + print(f"Failed to push changes to remote.") + return False + + print(f"Successfully merged {tag} into {branch} and pushed to remote.") + return True + + +def main(): + parser = argparse.ArgumentParser( + description="Merge a tag into a branch on a GitHub repository.", + formatter_class=argparse.RawDescriptionHelpFormatter, + epilog=""" +Examples: + %(prog)s leanprover/mathlib4 stable v4.6.0 Merge tag v4.6.0 into stable branch + +The script will: +1. Clone the repository +2. Check if the tag and branch exist +3. Check if the tag can be merged cleanly into the branch +4. Perform the merge and push to remote if possible + """ + ) + parser.add_argument("repo", help="GitHub repository in the format 'organization/repository'") + parser.add_argument("branch", help="The target branch to merge into") + parser.add_argument("tag", help="The tag to merge from") + + args = parser.parse_args() + + # Create a temporary directory for the repository + temp_dir = tempfile.mkdtemp() + try: + # Clone the repository + if not clone_repo(args.repo, temp_dir): + sys.exit(1) + + # Check if the tag can be merged and perform the merge + if not check_and_merge(args.repo, args.branch, args.tag, temp_dir): + sys.exit(1) + + finally: + # Clean up the temporary directory + print(f"Cleaning up temporary files...") + shutil.rmtree(temp_dir) + + +if __name__ == "__main__": + main() \ No newline at end of file diff --git a/script/release_checklist.py b/script/release_checklist.py index 4cfb937cb3..3e8c4acd81 100755 --- a/script/release_checklist.py +++ b/script/release_checklist.py @@ -8,6 +8,11 @@ import subprocess import sys import os +def debug(verbose, message): + """Print debug message if verbose mode is enabled.""" + if verbose: + print(f" [DEBUG] {message}") + def parse_repos_config(file_path): with open(file_path, "r") as f: return yaml.safe_load(f)["repositories"] @@ -90,7 +95,7 @@ def is_version_gte(version1, version2): return False return parse_version(version1) >= parse_version(version2) -def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token): +def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token, verbose=False): # 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 {} @@ -98,6 +103,7 @@ def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token): # 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: + debug(verbose, f"Could not fetch tag {tag_name}, status code: {tag_response.status_code}") return False # Handle both single object and array responses @@ -106,22 +112,48 @@ def is_merged_into_stable(repo_url, tag_name, stable_branch, github_token): # Find the exact matching tag in the list matching_tags = [tag for tag in tag_data if tag['ref'] == f'refs/tags/{tag_name}'] if not matching_tags: + debug(verbose, f"No matching tag found for {tag_name} in response list") return False tag_sha = matching_tags[0]['object']['sha'] else: tag_sha = tag_data['object']['sha'] - + + # Check if the tag is an annotated tag and get the actual commit SHA + if tag_data.get('object', {}).get('type') == 'tag' or ( + isinstance(tag_data, list) and + matching_tags and + matching_tags[0].get('object', {}).get('type') == 'tag'): + + # Get the commit that this tag points to + tag_obj_response = requests.get(f"{api_base}/git/tags/{tag_sha}", headers=headers) + if tag_obj_response.status_code == 200: + tag_obj = tag_obj_response.json() + if 'object' in tag_obj and tag_obj['object']['type'] == 'commit': + commit_sha = tag_obj['object']['sha'] + debug(verbose, f"Tag is annotated. Resolved commit SHA: {commit_sha}") + tag_sha = commit_sha # Use the actual commit 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: + debug(verbose, f"Could not fetch commits for branch {stable_branch}, status code: {commits_response.status_code}") 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 + + is_merged = tag_sha in stable_commits + + debug(verbose, f"Tag SHA: {tag_sha}") + debug(verbose, f"First 5 stable commits: {stable_commits[:5]}") + debug(verbose, f"Total stable commits fetched: {len(stable_commits)}") + if not is_merged: + debug(verbose, f"Tag SHA not found in first {len(stable_commits)} commits of stable branch") + + return is_merged def is_release_candidate(version): return "-rc" in version @@ -195,13 +227,15 @@ def pr_exists_with_title(repo_url, title, github_token): return None def main(): + parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories") + parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)") + parser.add_argument("--verbose", "-v", action="store_true", help="Enable verbose debugging output") + args = parser.parse_args() + github_token = get_github_token() - - if len(sys.argv) != 2: - print("Usage: python3 release_checklist.py ") - sys.exit(1) - - toolchain = sys.argv[1] + toolchain = args.toolchain + verbose = args.verbose + stripped_toolchain = strip_rc_suffix(toolchain) lean_repo_url = "https://github.com/leanprover/lean4" @@ -291,6 +325,7 @@ def main(): print(f" ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})") else: print(f" ❌ PR with title '{pr_title}' does not exist") + print(f" Run `script/release_steps.py {toolchain} {name}` to create it") repo_status[name] = False continue print(f" ✅ On compatible toolchain (>= {toolchain})") @@ -303,8 +338,10 @@ def main(): print(f" ✅ Tag {toolchain} exists") if check_stable and not is_release_candidate(toolchain): - if not is_merged_into_stable(url, toolchain, "stable", github_token): + if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose): + org_repo = extract_org_repo_from_url(url) print(f" ❌ Tag {toolchain} is not merged into stable") + print(f" Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it") repo_status[name] = False continue print(f" ✅ Tag {toolchain} is merged into stable") diff --git a/script/release_repos.yml b/script/release_repos.yml index e59f05e449..3dad36ca39 100644 --- a/script/release_repos.yml +++ b/script/release_repos.yml @@ -85,6 +85,7 @@ repositories: - Batteries - doc-gen4 - import-graph + - plausible - name: REPL url: https://github.com/leanprover-community/repl diff --git a/script/release_steps.py b/script/release_steps.py index 74ff3e7bcb..118eb7f282 100755 --- a/script/release_steps.py +++ b/script/release_steps.py @@ -51,15 +51,18 @@ def find_repo(repo_substring, config): def generate_script(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) script_lines = [ - f"cd {repo_name}", + f"cd {repo_dir}", "git fetch", - f"git checkout {default_branch}", + f"git checkout {default_branch} && git pull", f"git checkout -b bump_to_{version}", f"echo leanprover/lean4:{version} > lean-toolchain", ] @@ -67,19 +70,21 @@ def generate_script(repo, version, config): # Special cases for specific repositories if repo_name == "REPL": script_lines.extend([ - "cd test/Mathlib", - f"echo leanprover/lean4:{version} > lean-toolchain", - 'echo "Please update the dependencies in lakefile.{lean,toml}"', "lake update", - "cd ../.." + "cd test/Mathlib", + f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml", + f"echo leanprover/lean4:{version} > lean-toolchain", + "lake update", + "cd ../..", + "./test.sh" ]) elif dependencies: script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"') + script_lines.append("lake update") - script_lines.append("lake update") script_lines.append("") - if not re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]: + if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]: script_lines.extend([ "echo 'This repo has nightly-testing infrastructure'", f"git merge bump/{version}", @@ -98,13 +103,13 @@ def generate_script(repo, version, config): if repo_name == "ProofWidgets4": script_lines.append(f"echo 'Note: Follow the version convention of the repository for tagging.'") elif requires_tagging: - script_lines.append(f"git tag -a {version} -m 'Release {version}'") - script_lines.append("git push origin --tags") + script_lines.append(f"git checkout {default_branch} && git pull") + script_lines.append(f'[ "$(cat lean-toolchain)" = "leanprover/lean4:{version}" ] && git tag -a {version} -m \'Release {version}\' && git push origin --tags || echo "Error: lean-toolchain does not contain expected version {version}"') if has_stable_branch: script_lines.extend([ - "git checkout stable", - f"git merge {version}", + "git checkout stable && git pull", + f"git merge {version} --no-edit", "git push origin stable" ])