diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index d11cce5468..bedfe44fe6 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -214,6 +214,7 @@ file( GLOB_RECURSE LEANLAKETESTS #"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh" "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh" + "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh" ) foreach(T ${LEANLAKETESTS}) if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*") diff --git a/tests/lake/tests/shake/input/lean-toolchain b/tests/lake/tests/shake/input/lean-toolchain new file mode 100644 index 0000000000..dcca6df980 --- /dev/null +++ b/tests/lake/tests/shake/input/lean-toolchain @@ -0,0 +1 @@ +lean4 diff --git a/tests/lake/tests/shake/test.sh b/tests/lake/tests/shake/test.sh index 570e782a4b..4dd1007848 100755 --- a/tests/lake/tests/shake/test.sh +++ b/tests/lake/tests/shake/test.sh @@ -21,6 +21,7 @@ match_pat 'remove.*Lib.B' produced.out cp -r input/* . test_run build test_run shake --fix Main +test_run build # Verify Main.lean matches expected check_diff expected/Main.lean Main.lean