Compare commits

...

8 Commits

Author SHA1 Message Date
Kim Morrison
69f8d761a6 feat: further release checklist automation 2025-04-02 21:28:49 +11:00
Kim Morrison
0c718ad3c3 merge master 2025-04-02 19:06:05 +11:00
Kim Morrison
a9ba387a35 . 2025-04-02 19:04:50 +11:00
Kim Morrison
79ead2db55 fix REPL steps 2025-04-01 17:29:03 +11:00
Kim Morrison
9e99fb4958 shallow clone 2025-04-01 17:16:27 +11:00
Johan Commelin
9d9f4737c6 refactor: abstract debug printing in release_checklist.py 2025-04-01 07:56:43 +02:00
Kim Morrison
5f07ede94c feat: upgrades to release automation 2025-04-01 16:44:24 +11:00
Kim Morrison
c371a5ca75 feat: upgrades to release automation 2025-04-01 16:44:20 +11:00
4 changed files with 58 additions and 18 deletions

View File

@@ -49,7 +49,7 @@ def run_command(command, check=True, capture_output=True):
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
# Keep the shallow clone for efficiency
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}.")
@@ -63,19 +63,21 @@ def check_and_merge(repo, branch, tag, temp_dir):
# 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}")
# First fetch the specific remote branch with its history
print(f"Fetching branch '{branch}'...")
fetch_branch = run_command(f"git fetch origin {branch}:refs/remotes/origin/{branch} --update-head-ok")
if fetch_branch.returncode != 0:
print(f"Error: Failed to fetch branch '{branch}'.")
return False
# Then fetch the specific tag
print(f"Fetching tag '{tag}'...")
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
# Check if branch exists now that we've fetched it
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.")

View File

@@ -7,6 +7,8 @@ import base64
import subprocess
import sys
import os
# Import run_command from merge_remote.py
from merge_remote import run_command
def debug(verbose, message):
"""Print debug message if verbose mode is enabled."""
@@ -230,11 +232,13 @@ 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")
parser.add_argument("--dry-run", action="store_true", help="Dry run mode (no actions taken)")
args = parser.parse_args()
github_token = get_github_token()
toolchain = args.toolchain
verbose = args.verbose
# dry_run = args.dry_run # Not used yet but available for future implementation
stripped_toolchain = strip_rc_suffix(toolchain)
lean_repo_url = "https://github.com/leanprover/lean4"
@@ -290,6 +294,7 @@ def main():
for repo in repos:
name = repo["name"]
url = repo["url"]
org_repo = extract_org_repo_from_url(url)
branch = repo["branch"]
check_stable = repo["stable-branch"]
check_tag = repo.get("toolchain-tag", True)
@@ -331,10 +336,25 @@ def main():
print(f" ✅ On compatible toolchain (>= {toolchain})")
if check_tag:
if not tag_exists(url, toolchain, github_token):
print(f" ❌ Tag {toolchain} does not exist. Run `script/push_repo_release_tag.py {extract_org_repo_from_url(url)} {branch} {toolchain}`.")
repo_status[name] = False
continue
tag_exists_initially = tag_exists(url, toolchain, github_token)
if not tag_exists_initially:
if args.dry_run:
print(f" ❌ Tag {toolchain} does not exist. Run `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`.")
repo_status[name] = False
continue
else:
print(f" … Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
# Run the script to create the tag
subprocess.run(["script/push_repo_release_tag.py", org_repo, branch, toolchain])
# Check again if the tag exists now
if not tag_exists(url, toolchain, github_token):
print(f" ❌ Manual intervention required.")
repo_status[name] = False
continue
# This will print in all successful cases - whether tag existed initially or was created successfully
print(f" ✅ Tag {toolchain} exists")
if check_stable and not is_release_candidate(toolchain):
@@ -350,9 +370,16 @@ def main():
next_version = get_next_version(toolchain)
bump_branch = f"bump/{next_version}"
if not branch_exists(url, bump_branch, github_token):
print(f" ❌ Bump branch {bump_branch} does not exist")
repo_status[name] = False
continue
if args.dry_run:
print(f" ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it.")
repo_status[name] = False
continue
print(f" … Bump branch {bump_branch} does not exist. Creating it...")
result = run_command(f"gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
if result.returncode != 0:
print(f" ❌ Failed to create bump branch {bump_branch}")
repo_status[name] = False
continue
print(f" ✅ Bump branch {bump_branch} exists")
if not check_bump_branch_toolchain(url, bump_branch, github_token):
repo_status[name] = False

View File

@@ -63,7 +63,9 @@ repositories:
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
dependencies:
- Cli
- Batteries
- name: plausible
url: https://github.com/leanprover-community/plausible

View File

@@ -84,17 +84,26 @@ def generate_script(repo, version, config):
script_lines.append("")
script_lines.extend([
f'git commit -am "chore: bump toolchain to {version}"',
""
])
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}",
f"git merge origin/bump/{version.split('-rc')[0]}",
"echo 'Please resolve any conflicts.'",
""
])
if repo_name != "Mathlib":
script_lines.extend([
"lake build && if lake check-test; then lake test; fi",
""
])
script_lines.extend([
f'git commit -am "chore: bump toolchain to {version}"',
"gh pr create",
'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
"echo 'Please review the PR and merge it.'",
""
])