sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: use de-modulized subverso rev for verso test-project sub-manifests

Browse Source 
The test-projects use leanprover/lean4:v4.21.0 which doesn't support
module/prelude syntax. Sync the de-modulized subverso rev (tagged
no-modules/<root-rev>) rather than the root rev so the sub-projects
build correctly with their old toolchain.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
2026-03-04 12:06:45 +00:00
parent 51cdf26936
commit 1c61ba6420
1 changed files with 9 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
script/release_steps.py
View File

@@ -482,17 +482,21 @@ def execute_release_steps(repo, version, config):
elif repo_name == "verso":
# verso has nested Lake projects in test-projects/ that each have their own
# lake-manifest.json with a subverso pin. After updating the root manifest via
# `lake update`, sync the subverso rev into all sub-manifests so the
# "SubVerso version consistency" CI check passes.
# `lake update`, sync the de-modulized subverso rev into all sub-manifests.
# The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
# syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
# The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
run_command("lake update", cwd=repo_path, stream_output=True)
print(blue("Syncing subverso rev from root manifest to test-project sub-manifests..."))
print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
sync_script = (
'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
'find test-projects -name lake-manifest.json -print0 | '
'xargs -0 -I{} sh -c \'jq --arg rev "$ROOT_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "{}" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "{}"\''
'xargs -0 -I{} sh -c \'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "{}" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "{}"\''
)
run_command(sync_script, cwd=repo_path)
print(green("Synced subverso rev to all test-project sub-manifests"))
print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
elif dependencies:
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
run_command("lake update", cwd=repo_path, stream_output=True)