From 359101e06b374f7f13da63459749dca7e9b26e55 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Aug 2026 14:05:11 +0000 Subject: [PATCH] fix: sync lean-toolchain for test projects that build against Verso `update-subverso.sh` iterated over `lake-manifest.json` files, so it never reached `literate-config` and `literate-multi-root`, which require Verso by path and therefore have no manifest. Their toolchains were left behind on every bump, failing the consistency check. List those projects in `test-projects/root-toolchain-projects.txt` and read it from the updater, the check, and the `!consistent` fixer, so the three cannot drift apart. The fixer resolves the list before checking out the pull request, since it runs with write access and must not take instructions from PR content. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_0188amTRAvgJg9gKTzsC6KWF --- .github/workflows/consistent-pr-comment.yml | 32 +++++++++++++++---- .../consistent-subverso-manifests.yml | 11 +++++-- test-projects/root-toolchain-projects.txt | 12 +++++++ update-subverso.sh | 32 +++++++++++++++++-- 4 files changed, 75 insertions(+), 12 deletions(-) create mode 100644 test-projects/root-toolchain-projects.txt diff --git a/.github/workflows/consistent-pr-comment.yml b/.github/workflows/consistent-pr-comment.yml index 43ae1c487..b09f94dd2 100644 --- a/.github/workflows/consistent-pr-comment.yml +++ b/.github/workflows/consistent-pr-comment.yml @@ -63,6 +63,28 @@ jobs: with: token: ${{ secrets.GITHUB_TOKEN }} + - name: Resolve toolchain sync targets + # Read the list from the default-branch checkout, before the pull + # request's own code is on disk. This job can write to the + # repository, so it must not take instructions from the PR. + run: | + list=test-projects/root-toolchain-projects.txt + mapfile -t names < <(grep -vE '^[[:space:]]*(#|$)' "$list") + if [ "${#names[@]}" -eq 0 ]; then + echo "Error: no projects listed in $list" >&2 + exit 1 + fi + for name in "${names[@]}"; do + case "$name" in + */* | . | ..) + echo "Error: $list must list bare directory names, got '$name'" >&2 + exit 1 + ;; + esac + echo "test-projects/$name/lean-toolchain" + done > "$RUNNER_TEMP/toolchain-targets" + cat "$RUNNER_TEMP/toolchain-targets" + - name: Checkout PR branch env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} @@ -70,10 +92,7 @@ jobs: - name: Sync test-project lean-toolchains run: | - targets=( - test-projects/literate-config/lean-toolchain - test-projects/literate-multi-root/lean-toolchain - ) + mapfile -t targets < "$RUNNER_TEMP/toolchain-targets" for t in "${targets[@]}"; do if [ -L "$t" ]; then echo "Refusing to write through symlink: $t" @@ -89,9 +108,8 @@ jobs: run: | git config user.name "github-actions[bot]" git config user.email "github-actions[bot]@users.noreply.github.com" - git add -- \ - test-projects/literate-config/lean-toolchain \ - test-projects/literate-multi-root/lean-toolchain + mapfile -t targets < "$RUNNER_TEMP/toolchain-targets" + git add -- "${targets[@]}" if git diff --cached --quiet; then echo "No consistency fixes needed" echo "changes=false" >> "$GITHUB_OUTPUT" diff --git a/.github/workflows/consistent-subverso-manifests.yml b/.github/workflows/consistent-subverso-manifests.yml index 9ecaa4256..ae13b2bb9 100644 --- a/.github/workflows/consistent-subverso-manifests.yml +++ b/.github/workflows/consistent-subverso-manifests.yml @@ -50,12 +50,19 @@ jobs: xargs -0 jq -e --arg root "$ROOT_REV" --arg demod "$DEMOD_REV" \ 'all(.packages[] | select(.name == "subverso") | .rev; . == $root or . == $demod)' - - name: Check that literate test projects match root lean-toolchain + - name: Check that root-toolchain test projects match root lean-toolchain run: | ROOT_TC=$(cat lean-toolchain) echo "Root lean-toolchain: $ROOT_TC" + mapfile -t PROJECTS < <(grep -vE '^[[:space:]]*(#|$)' test-projects/root-toolchain-projects.txt) + # An unreadable list would otherwise check nothing and pass. + if [ "${#PROJECTS[@]}" -eq 0 ]; then + echo "Error: no projects listed in test-projects/root-toolchain-projects.txt" + exit 1 + fi FAILED=0 - for proj in test-projects/literate-config test-projects/literate-multi-root; do + for name in "${PROJECTS[@]}"; do + proj="test-projects/$name" PROJ_TC=$(cat "$proj/lean-toolchain") if [ "$PROJ_TC" != "$ROOT_TC" ]; then echo "MISMATCH: $proj/lean-toolchain ($PROJ_TC) does not match root ($ROOT_TC)" diff --git a/test-projects/root-toolchain-projects.txt b/test-projects/root-toolchain-projects.txt new file mode 100644 index 000000000..01239aa05 --- /dev/null +++ b/test-projects/root-toolchain-projects.txt @@ -0,0 +1,12 @@ +# Test projects that build against Verso's own source, via a path dependency. +# They inherit Verso's module status, so they must use the root toolchain, and +# `update-subverso.sh` keeps their `lean-toolchain` in step with the root one. +# +# Every other test project depends on SubVerso from Git and is independent of +# the root toolchain. Several are deliberately pinned to older releases to check +# that those keep working, so they must not be listed here. +# +# One project directory name per line; blank lines and `#` comments are ignored. + +literate-config +literate-multi-root diff --git a/update-subverso.sh b/update-subverso.sh index 3dad9ffc2..802f30701 100755 --- a/update-subverso.sh +++ b/update-subverso.sh @@ -72,9 +72,6 @@ find test-projects -name "lake-manifest.json" -not -path "$ROOT_MANIFEST" | grep if jq -e '.packages[] | select(.name == "verso" and .type == "path")' "$manifest_file" > /dev/null 2>&1; then TARGET_REV="$SUBVERSO_REV" echo " Uses Verso path dependency → modulized rev" - # Keep toolchain in sync with root - cp lean-toolchain "$project_dir/lean-toolchain" - echo " Copied lean-toolchain to $project_dir/" else TARGET_REV="$SUBVERSO_NOMODULE_REV" echo " Standalone project → de-modulized rev" @@ -97,3 +94,32 @@ find test-projects -name "lake-manifest.json" -not -path "$ROOT_MANIFEST" | grep done echo "All manifests processed successfully" + +# Projects listed in root-toolchain-projects.txt build against Verso's source and +# must track the root toolchain. They are handled here rather than in the loop +# above, which only reaches projects that have a lake-manifest.json. +PROJECT_LIST="test-projects/root-toolchain-projects.txt" +mapfile -t ROOT_TOOLCHAIN_PROJECTS < <(grep -vE '^[[:space:]]*(#|$)' "$PROJECT_LIST") + +# An unreadable list would otherwise leave the array empty and sync nothing. +if [ "${#ROOT_TOOLCHAIN_PROJECTS[@]}" -eq 0 ]; then + echo "Error: no projects listed in $PROJECT_LIST" + exit 1 +fi + +for name in "${ROOT_TOOLCHAIN_PROJECTS[@]}"; do + case "$name" in + */* | . | ..) + echo "Error: $PROJECT_LIST must list bare directory names, got '$name'" + exit 1 + ;; + esac + + target="test-projects/$name/lean-toolchain" + if [ -L "$target" ]; then + echo "Refusing to write through symlink: $target" + exit 1 + fi + cp lean-toolchain "$target" + echo "Copied lean-toolchain to test-projects/$name/" +done