diff --git a/tests/pkg/ver_clash/.gitignore b/tests/pkg/ver_clash/.gitignore new file mode 100644 index 0000000000..76b5fe4428 --- /dev/null +++ b/tests/pkg/ver_clash/.gitignore @@ -0,0 +1 @@ +/work/ diff --git a/tests/pkg/ver_clash/clean.sh b/tests/pkg/ver_clash/clean.sh index 0c5790af33..b734e1d511 100755 --- a/tests/pkg/ver_clash/clean.sh +++ b/tests/pkg/ver_clash/clean.sh @@ -1,3 +1 @@ -rm -rf DiamondExample-*/.git -rm -rf DiamondExample-*/.lake DiamondExample-*/lake-manifest.json -rm -f DiamondExample-D/produced.out +rm -rf work diff --git a/tests/pkg/ver_clash/run_test.sh b/tests/pkg/ver_clash/run_test.sh index 7b22adf8e7..ee7b1ef6a4 100644 --- a/tests/pkg/ver_clash/run_test.sh +++ b/tests/pkg/ver_clash/run_test.sh @@ -18,6 +18,16 @@ # Setup # --- +./clean.sh + +# Copy test data to a working directory to avoid initializing Git repositories +# inside the checked-in source tree. Cleaned at the start so artifacts from a +# failed run remain available for inspection. +WORK_DIR="$PWD/work" +mkdir -p "$WORK_DIR" +cp -r DiamondExample-A DiamondExample-B DiamondExample-C DiamondExample-D lean-toolchain "$WORK_DIR/" +cd "$WORK_DIR" + # Since committing a Git repository to a Git repository is not well-supported, # We reinitialize the repositories on each test. @@ -42,8 +52,6 @@ init_git() { set +x } -./clean.sh - pushd DiamondExample-A sed_i s/add_left_comm/poorly_named_lemma/ DiamondExampleA/Ring/Lemmas.lean lake update @@ -107,7 +115,3 @@ capture_fail lake build check_out_contains 'could not disambiguate the module `DiamondExampleA.Ring.Lemmas`' popd - -# Cleanup -rm -rf DiamondExample-*/.git -rm -rf DiamondExample-*/.lake