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

fix: remove obsolete docs directory handling for cslib in release_steps.py (#11649)

Browse source 
This PR updates the release checklist script. The cslib repository no
longer has a docs subdirectory, so the release script was failing when
trying to update lakefile.toml and lean-toolchain in that nonexistent
directory.
This commit is contained in:
Kim Morrison 2025-12-14 16:15:38 +11:00 • committed by GitHub
parent 983d64395a
commit b7e6862163
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
script/release_steps.py
View file

@ -421,17 +421,6 @@ def execute_release_steps(repo, version, config):
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)
print(blue("Updating docs/lakefile.toml..."))
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path / "docs")
# Update lean-toolchain in docs
print(blue("Updating docs/lean-toolchain..."))
docs_toolchain = repo_path / "docs" / "lean-toolchain"
with open(docs_toolchain, "w") as f:
f.write(f"leanprover/lean4:{version}\n")
print(green(f"Updated docs/lean-toolchain to leanprover/lean4:{version}"))
run_command("lake update", cwd=repo_path, stream_output=True)
elif dependencies:
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)