From 293d1dfd5759c1f0bea8da2121343de16abc3e32 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 1 Jul 2025 12:39:10 +1000 Subject: [PATCH] chore: improvements to release automation (#9119) --- script/release_checklist.py | 81 +++++++++++++++++++++++++++++++++---- 1 file changed, 74 insertions(+), 7 deletions(-) diff --git a/script/release_checklist.py b/script/release_checklist.py index 70559d6a69..25b6c5a968 100755 --- a/script/release_checklist.py +++ b/script/release_checklist.py @@ -231,6 +231,43 @@ def get_next_version(version): # Next version is always .0 return f"v{major}.{minor + 1}.0" +def get_latest_nightly_tag(github_token): + """Get the most recent nightly tag from leanprover/lean4-nightly.""" + api_url = "https://api.github.com/repos/leanprover/lean4-nightly/tags" + headers = {'Authorization': f'token {github_token}'} if github_token else {} + response = requests.get(api_url, headers=headers) + if response.status_code != 200: + return None + tags = response.json() + if not tags: + return None + # Return the most recent tag name + return tags[0]['name'] + +def update_lean_toolchain_in_branch(org_repo, branch, toolchain_content, github_token): + """Update the lean-toolchain file in a specific branch.""" + api_url = f"https://api.github.com/repos/{org_repo}/contents/lean-toolchain" + headers = {'Authorization': f'token {github_token}'} if github_token else {} + + # First get the current file to get its SHA + response = requests.get(f"{api_url}?ref={branch}", headers=headers) + if response.status_code != 200: + return False + + current_file = response.json() + file_sha = current_file['sha'] + + # Update the file + update_data = { + "message": f"chore: update lean-toolchain to {toolchain_content}", + "content": base64.b64encode(toolchain_content.encode('utf-8')).decode('utf-8'), + "sha": file_sha, + "branch": branch + } + + response = requests.put(api_url, json=update_data, headers=headers) + return response.status_code in [200, 201] + def check_bump_branch_toolchain(url, bump_branch, github_token): """Check if the lean-toolchain file in bump branch starts with either 'leanprover/lean4:nightly-' or the next version.""" content = get_branch_content(url, bump_branch, "lean-toolchain", github_token) @@ -455,7 +492,7 @@ def main(): repo_status[name] = False continue else: - print(f" … Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...") + 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]) @@ -478,7 +515,7 @@ def main(): repo_status[name] = False continue else: - print(f" … Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...") + print(f" ⮕ Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...") # Run the script to merge the tag subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain]) @@ -495,19 +532,49 @@ def main(): if check_bump: next_version = get_next_version(toolchain) bump_branch = f"bump/{next_version}" - if not branch_exists(url, bump_branch, github_token): + + # For mathlib4, use the nightly-testing fork for bump branches + bump_org_repo = org_repo + bump_url = url + if name == "mathlib4": + bump_org_repo = "leanprover-community/mathlib4-nightly-testing" + bump_url = "https://github.com/leanprover-community/mathlib4-nightly-testing" + + branch_created = False + if not branch_exists(bump_url, bump_branch, github_token): 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.") + latest_nightly = get_latest_nightly_tag(github_token) + nightly_note = f" (will set lean-toolchain to {latest_nightly})" if name in ["batteries", "mathlib4"] and latest_nightly else "" + print(f" ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{bump_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{nightly_note}.") 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) + print(f" ⮕ Bump branch {bump_branch} does not exist. Creating it...") + result = run_command(f"gh api -X POST /repos/{bump_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 + branch_created = True + print(f" ✅ Bump branch {bump_branch} exists") - if not check_bump_branch_toolchain(url, bump_branch, github_token): + + # For batteries and mathlib4, update the lean-toolchain to the latest nightly + if branch_created and name in ["batteries", "mathlib4"]: + latest_nightly = get_latest_nightly_tag(github_token) + if latest_nightly: + nightly_toolchain = f"leanprover/lean4:{latest_nightly}" + print(f" ⮕ Updating lean-toolchain to {nightly_toolchain}...") + if update_lean_toolchain_in_branch(bump_org_repo, bump_branch, nightly_toolchain, github_token): + print(f" ✅ Updated lean-toolchain to {nightly_toolchain}") + else: + print(f" ❌ Failed to update lean-toolchain to {nightly_toolchain}") + repo_status[name] = False + continue + else: + print(f" ❌ Could not fetch latest nightly tag") + repo_status[name] = False + continue + if not check_bump_branch_toolchain(bump_url, bump_branch, github_token): repo_status[name] = False continue