max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: release_steps runs lake exe cache get when needed (#10882)

Browse source
This commit is contained in:
Kim Morrison 2025-10-22 09:49:38 +11:00 • committed by GitHub
parent bd05f87d01
commit 11eabdb000
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
script/release_steps.py
View file

@ -589,8 +589,19 @@ def execute_release_steps(repo, version, config):
# Clean lake cache for a fresh build
print(blue("Cleaning lake cache..."))
run_command("rm -rf .lake", cwd=repo_path)
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"))