fix: workaround nightly issue

Author: david-christiansen

.github/workflows/ci.yml

@@ -139,7 +139,16 @@ jobs:
             - name: Verify tutorial project zip files build
               if: github.event_name != 'release'
               run: |
-                  scripts/check-tutorial-zips.sh
+                  # On Linux, some nightly toolchains currently report a version string that
+                  # the zips turn into a toolchain name that elan rejects, so build the
+                  # projects with this repository's toolchain instead. Releases and release
+                  # candidates are unaffected and build with the toolchain from the zip.
+                  # See https://github.com/leanprover/lean4/issues/14702
+                  if grep -q nightly lean-toolchain; then
+                      scripts/check-tutorial-zips.sh "$(cat lean-toolchain)"
+                  else
+                      scripts/check-tutorial-zips.sh
+                  fi
 
             - name: Generate proofreading HTML
               if: github.event_name == 'pull_request'

scripts/check-tutorial-zips.sh

@@ -1,6 +1,16 @@
 #!/usr/bin/env bash
 
 # Verify that tutorial project zip files can be unpacked and built with lake
+#
+# Usage: check-tutorial-zips.sh [TOOLCHAIN]
+#
+# When TOOLCHAIN is given, it replaces the `lean-toolchain` file of each
+# unpacked project. On Linux, some nightly toolchains currently report a version
+# string that the zips turn into a toolchain name that elan rejects, so CI passes
+# this repository's toolchain when building from a nightly. Releases and release
+# candidates are unaffected and build with the toolchain from the zip.
+# See https://github.com/leanprover/lean4/issues/14702
+toolchain="${1:-}"
 
 # First check that we actually found some zip files
 zip_count=$(find _out/site/tutorials -name "*.zip" 2>/dev/null | wc -l)
@@ -25,6 +35,10 @@ while IFS= read -r zip; do
         echo "Warning: No lakefile found in $zip"
         ((failures++))
     else
+        if [ -n "$toolchain" ]; then
+            echo "Using toolchain: $toolchain"
+            echo "$toolchain" > "$project_dir/lean-toolchain"
+        fi
         pushd "$project_dir" > /dev/null
         if lake build 2>&1; then
             echo "Build succeeded"