test: lake: give issue tests meaningful names

src/lake/tests/75/foo/lakefile.lean

@@ -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
-}

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

src/lake/tests/rebuild/clean.sh

@@ -0,0 +1,2 @@
+rm -rf build lakefile.olean
+rm -rf Foo

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

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

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"

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}"