diff --git a/src/lake/tests/75/foo/lakefile.lean b/src/lake/tests/75/foo/lakefile.lean deleted file mode 100644 index bc5ee700db..0000000000 --- a/src/lake/tests/75/foo/lakefile.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Lake -open Lake DSL - -package foo { - -- add package configuration options here -} - -lean_lib Foo { - -- add library configuration options here -} - -@[default_target] -lean_exe foo { - root := `Main -} diff --git a/src/lake/tests/44/.gitignore b/src/lake/tests/old/.gitignore similarity index 100% rename from src/lake/tests/44/.gitignore rename to src/lake/tests/old/.gitignore diff --git a/src/lake/tests/44/clean.sh b/src/lake/tests/old/clean.sh similarity index 100% rename from src/lake/tests/44/clean.sh rename to src/lake/tests/old/clean.sh diff --git a/src/lake/tests/44/expected.out b/src/lake/tests/old/expected.out similarity index 100% rename from src/lake/tests/44/expected.out rename to src/lake/tests/old/expected.out diff --git a/src/lake/tests/44/test.sh b/src/lake/tests/old/test.sh similarity index 86% rename from src/lake/tests/44/test.sh rename to src/lake/tests/old/test.sh index 2714dbc5c3..295af7d095 100755 --- a/src/lake/tests/44/test.sh +++ b/src/lake/tests/old/test.sh @@ -5,6 +5,9 @@ LAKE=${LAKE:-../../build/bin/lake} ./clean.sh +# Tests the `--old` option for using outdate oleans +# See https://github.com/leanprover/lake/issues/44 + $LAKE new hello $LAKE -d hello build sleep 0.5 # for some reason, delay needed for `--old` rebuild consistency diff --git a/src/lake/tests/75/foo/.gitignore b/src/lake/tests/rebuild/.gitignore similarity index 100% rename from src/lake/tests/75/foo/.gitignore rename to src/lake/tests/rebuild/.gitignore diff --git a/src/lake/tests/75/foo/Main.lean b/src/lake/tests/rebuild/Main.lean similarity index 100% rename from src/lake/tests/75/foo/Main.lean rename to src/lake/tests/rebuild/Main.lean diff --git a/src/lake/tests/rebuild/clean.sh b/src/lake/tests/rebuild/clean.sh new file mode 100755 index 0000000000..c6a4b305f0 --- /dev/null +++ b/src/lake/tests/rebuild/clean.sh @@ -0,0 +1,2 @@ +rm -rf build lakefile.olean +rm -rf Foo diff --git a/src/lake/tests/rebuild/lakefile.lean b/src/lake/tests/rebuild/lakefile.lean new file mode 100644 index 0000000000..65a4412d94 --- /dev/null +++ b/src/lake/tests/rebuild/lakefile.lean @@ -0,0 +1,10 @@ +import Lake +open Lake DSL + +package foo + +lean_lib Foo + +@[default_target] +lean_exe foo where + root := `Main diff --git a/src/lake/tests/75/test.sh b/src/lake/tests/rebuild/test.sh similarity index 51% rename from src/lake/tests/75/test.sh rename to src/lake/tests/rebuild/test.sh index 00109b6d08..50cbab1d3b 100755 --- a/src/lake/tests/75/test.sh +++ b/src/lake/tests/rebuild/test.sh @@ -1,10 +1,16 @@ #!/usr/bin/env bash set -euxo pipefail -LAKE=${LAKE:-../../../build/bin/lake} +LAKE=${LAKE:-../../build/bin/lake} + +./clean.sh + +# Tests that Lake rebulds C files and relinks executables on changes +# See https://github.com/leanprover/lake/issues/75 + +# The exact issue is no longer applicable as Lake now always rebuilds C files +# with the other `lean` artifacts but the test is still nice to have -cd foo -rm -rf build lakefile.olean mkdir -p Foo echo $'def a := "a"' > Foo/Test.lean echo $'import Foo.Test def hello := a' > Foo.lean diff --git a/src/lake/tests/62/.gitignore b/src/lake/tests/toolchain/.gitignore similarity index 100% rename from src/lake/tests/62/.gitignore rename to src/lake/tests/toolchain/.gitignore diff --git a/src/lake/tests/62/clean.sh b/src/lake/tests/toolchain/clean.sh similarity index 100% rename from src/lake/tests/62/clean.sh rename to src/lake/tests/toolchain/clean.sh diff --git a/src/lake/tests/62/test.sh b/src/lake/tests/toolchain/test.sh similarity index 79% rename from src/lake/tests/62/test.sh rename to src/lake/tests/toolchain/test.sh index bf68fa6083..c421c78bf1 100755 --- a/src/lake/tests/62/test.sh +++ b/src/lake/tests/toolchain/test.sh @@ -1,6 +1,10 @@ #!/usr/bin/env bash set -euxo pipefail +# Tests that Lake rebuilds when toolchain changes +# See https://github.com/leanprover/lake/issues/62 +# Requires Elan to download a toolchain + # skip if no elan found if ! command -v elan > /dev/null; then echo "elan not found; skipping test" diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 62be3e37bf..389bfca006 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -173,12 +173,12 @@ ENDFOREACH(T) # Create a lake test for each test and examples subdirectory of `lake` # which contains a `test.sh` file, excluding the following test(s): # bootstrap: too slow -# 62: requires elan to download toolchain +# toolchain: requires elan to download toolchain file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/tests/test.sh" "${LEAN_SOURCE_DIR}/lake/examples/test.sh") FOREACH(T ${LEANLAKETESTS}) - if(NOT T MATCHES ".*(lake-packages|bootstrap|62).*") + if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain).*") GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY) GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME) add_test(NAME "leanlaketest_${DIR_NAME}"