fix: sync lean-toolchain for test projects that build against Verso

.github/workflows/consistent-pr-comment.yml

@@ -63,17 +63,36 @@ 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 }}
               run: gh pr checkout ${{ github.event.issue.number }}
 
             - 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"

.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)"

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

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