test: clean up tests writing to tracked files, prevent future violations

.github/workflows/build-template.yml

@@ -308,12 +308,31 @@ jobs:
         run: |
           build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
+      # Tests must not write into the checked-in source tree; scratch output belongs in an
+      # ignored path. Making tracked files read-only catches a test that edits one even if it
+      # restores the file afterwards, which the tree comparison below cannot see.
+      - name: Protect Source Tree
+        run: |
+          git status --porcelain -unormal | sort > "$RUNNER_TEMP/tree-before"
+          git ls-files -z | xargs -0 chmod a-w
+        if: matrix.test
       - name: Test
         id: test
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: matrix.test
+      # restore write access before any later step (stage 2, benchmarks, `update-stage0`) runs
+      - name: Unprotect Source Tree
+        run: git ls-files -z | xargs -0 chmod u+w
+        if: always() && matrix.test
+      - name: Check Source Tree Clean
+        run: |
+          git status --porcelain -unormal | sort > "$RUNNER_TEMP/tree-after"
+          diff -u "$RUNNER_TEMP/tree-before" "$RUNNER_TEMP/tree-after" && exit 0
+          echo "::error::the test suite left files in the checked-in source tree; write them to an ignored path instead"
+          exit 1
+        if: matrix.test && steps.test.conclusion != 'skipped'
       # copy failed tests' output into the `<failure>` elements shown by the test summary
       - name: Embed Test Output
         run: |

tests/README.md

@@ -145,6 +145,22 @@ Otherwise, create a new test directory or pile:
    by updating the directory structure section above.
 5. Optionally update [`lint.py`](lint.py) if it makes sense.
 
+### Keep the source tree clean
+
+A test may not write into the checked-in source tree. CI enforces this by making tracked files
+read-only for the duration of the test run and by comparing `git status` before and after, so a
+test that violates it fails even if it tidies up afterwards.
+
+In practice this means:
+
+* Scratch output must land in an ignored path. Follow the pile's convention where there is one:
+  the `_tmp_` prefix in [`compile`](compile/.gitignore) and [`compile_bench`](compile_bench/.gitignore),
+  `produced.*` under [`lake`](lake/.gitignore) and [`pkg`](pkg/.gitignore). Otherwise add a
+  `.gitignore` entry next to the test.
+* A test that needs to edit its own inputs, or to initialize a Git repository, must work on a
+  copy. Lake tests have `copy_to_work` in [`lake/tests/common.sh`](lake/tests/common.sh) for this;
+  it copies into the ignored `work/` directory and `cd`s there.
+
 ## How to write a benchmark?
 
 When writing a benchmark, consider that most benchmarks are also executed as tests.

tests/bench/size/.gitignore

@@ -0,0 +1 @@
+/install/

tests/compile/compact_closure.lean

@@ -7,7 +7,7 @@ Tests `CompactedRegion.save`/`read` with `allowClosures := true`: closures (with
 are serialized in the `v3` olean format and round-trip within the same process.
 -/
 unsafe def main : IO Unit := do
-  let tmpFile : System.FilePath := "./_compact_closure_test.olean"
+  let tmpFile : System.FilePath := "./_tmp_compact_closure_test.olean"
 
   -- Simple closure with captured string
   let captured := "hello"

tests/compile/compact_closure_cross.lean

@@ -8,7 +8,7 @@ loads and runs correctly in a *separate* process: the `v3` lib relocation table
 closure's fn pointer to the loader process's address space.
 -/
 unsafe def main (args : List String) : IO UInt32 := do
-  let tmpFile : System.FilePath := "./_compact_closure_cross_test.olean"
+  let tmpFile : System.FilePath := "./_tmp_compact_closure_cross_test.olean"
 
   match args with
   | ["save"] =>

tests/lake/tests/clone/.gitignore

@@ -1 +1,2 @@
 /hello
+/lean-toolchain

tests/lake/tests/common.sh

@@ -46,6 +46,17 @@ else
 fi
 norm_dirname() { norm_path "$(dirname -- "$1")";  }
 
+# Copy the given paths into the ignored `work/` directory and `cd` into it, so that tests
+# which mutate their inputs or initialize a Git repository leave the checked-in source tree
+# untouched. The copies are made writable because `cp` propagates the source mode and CI
+# runs the suite with tracked files read-only.
+copy_to_work() {
+  mkdir -p work
+  cp -r "$@" work/
+  chmod -R u+w work
+  cd work
+}
+
 init_git() {
   echo "# initialize test repository"
   set -x

tests/lake/tests/init/.gitignore

@@ -9,3 +9,4 @@
 /meta
 /qed-lax
 /qed
+/mathlib_standards

tests/lake/tests/manifest/.gitignore

@@ -0,0 +1 @@
+/lake-packages/

tests/lake/tests/manifest/test.sh

@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r bar foo lakefile.lean lake-manifest-*.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work bar foo lakefile.lean lake-manifest-*.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the bar repository on each test. This requires updating the

tests/lake/tests/noRelease/test.sh

@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r dep lakefile.lean Test.lean "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work dep lakefile.lean Test.lean
 
 NO_BUILD_CODE=3
 

tests/lake/tests/packageOverrides/test.sh

@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r bar1 bar2 foo lakefile.lean packages.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work bar1 bar2 foo lakefile.lean packages.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the `bar1` repository on each test.

tests/lake/tests/rebuild/.gitignore

@@ -1,2 +1,2 @@
+/Foo/
 /Foo.lean
-/Foo/Test.lean

tests/lake/tests/reservoirConfig/test.sh

@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r lakefile.lean expected.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work lakefile.lean expected.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the repository on each test.

tests/lake/tests/shake/clean.sh

@@ -1,4 +1,3 @@
 #!/usr/bin/env bash
-rm -rf .lake lake-manifest.json lake-packages
-rm -f lakefile.toml Main.lean
-rm -rf Lib
+rm -rf work
+rm -f produced.out

tests/lake/tests/shake/test.sh

@@ -5,8 +5,8 @@ source ../common.sh
 
 # Test the `lake shake` command
 
-# Copy input project to working directory
-cp -r input/* .
+# `shake --fix` rewrites the sources it is given, so work on a copy
+copy_to_work input/*
 
 # Build the project first (shake needs .olean files)
 test_run build
@@ -20,11 +20,12 @@ match_pat 'remove.*Lib.B' produced.out
 lake_out shake --only DepMain
 
 # Test --fix mode: apply the fixes and verify the result
+cd ..
 ./clean.sh
-cp -r input/* .
+copy_to_work input/*
 test_run build
 test_run shake --fix Main
 test_run build
 
 # Verify Main.lean matches expected
-check_diff expected/Main.lean Main.lean
+check_diff ../expected/Main.lean Main.lean

tests/lake/tests/srcHash/test.sh

@@ -15,10 +15,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r dep lakefile.toml "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work dep lakefile.toml
 
 # Initialize the dependency
 echo "# SETUP: Create v1"

tests/lake/tests/toml/.gitignore

@@ -0,0 +1 @@
+/toml-test/

tests/lake/tests/updateUnknown/clean.sh

@@ -1,3 +1,2 @@
-rm -rf .lake dep/.lake
-rm -f lake-manifest.json dep/lake-manifest.json
+rm -rf work
 rm -f produced.out

tests/lake/tests/updateUnknown/test.sh

@@ -2,6 +2,9 @@
 source ../common.sh
 ./clean.sh
 
+# The manifest edit below rewrites `lakefile.toml`, so work on a copy
+copy_to_work lakefile.toml dep
+
 # Test that `lake update <pkg>` errors on unknown package names (typos and
 # case mismatches). Names that are current root requires or already in the
 # manifest are accepted (so selective update can still drop a removed require).
@@ -28,6 +31,3 @@ test_run update dep --keep-toolchain
 mv lakefile.toml.bak lakefile.toml
 
 test_run update --keep-toolchain
-
-# Cleanup
-./clean.sh

tests/lake/tests/versionTags/test.sh

@@ -4,10 +4,7 @@ source ./clean.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r lakefile.lean "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work lakefile.lean
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the repository on each test.

tests/pkg/.gitignore

@@ -1 +1,2 @@
 lake-manifest.json
+produced.*

tests/pkg/ver_clash/DiamondExample-D/.gitignore

@@ -1,2 +1 @@
 .lake
-produced.out