diff --git a/.github/workflows/consistent-pr-comment.yml b/.github/workflows/consistent-pr-comment.yml index 43ae1c48..b09f94dd 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 9ecaa425..ae13b2bb 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 00000000..01239aa0 --- /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 3dad9ffc..802f3070 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