test: lake: make 116 deterministic & related tweaks

.github/workflows/ci.yml

@@ -58,7 +58,7 @@ jobs:
             prepare-llvm: ../script/prepare-llvm-linux.sh lean-llvm*
             binary-check: ldd -v
             # foreign code may be linked against more recent glibc
-            CTEST_OPTIONS: -E 'foreign|leanlaketest_git'
+            CTEST_OPTIONS: -E 'foreign'
           - name: Linux
             os: ubuntu-latest
             check-stage3: true

src/lake/Lake/CLI/Serve.lean

@@ -58,7 +58,7 @@ def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
       let ctx := mkLakeContext ws
       pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
     else
-      IO.eprint "warning: package configuration has errors, falling back to plain `lean --server`"
+      IO.eprintln "warning: package configuration has errors, falling back to plain `lean --server`"
       pure (config.env.installVars.push (invalidConfigEnvVar, log), #[])
   (← IO.Process.spawn {
     cmd := config.env.lean.lean.toString

src/lake/test/116/test.sh

@@ -1,20 +1,26 @@
 #!/usr/bin/env bash
-set -eu
+set -exuo pipefail
 
 LAKE=${LAKE:-../../build/bin/lake}
 
+if [ "`uname`" = Darwin ]; then
+  TAIL=gtail
+else
+  TAIL=tail
+fi
+
 # Test environmnt variable
 
-LAKE_INVALID_CONFIG=$'foo\n' $LAKE print-paths 2>&1 | grep -m1 foo
+(LAKE_INVALID_CONFIG=$'foo\n' $LAKE print-paths 2>&1 || true) |  grep -m1 foo
 
 # Test watchdog
 
+set +x
+
 INIT_REQ=$'Content-Length: 46\r\n\r\n{"jsonrpc":"2.0","method":"initialize","id":1}'
 INITD_NOT=$'Content-Length: 40\r\n\r\n{"jsonrpc":"2.0","method":"initialized"}'
 OPEN_REQ=$'Content-Length: 145\r\n\r\n{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file://Test.lean","languageId":"lean4","version":0,"text":""}}}'
 MSGS="$INIT_REQ$INITD_NOT$OPEN_REQ"
 
-(echo -n "$MSGS"; sleep 5) | $LAKE serve 2>&1 > lake.out || true
-
-echo
-grep -m1 Lake lake.out
+grep -q "Invalid Lake configuration" < <(set +e; (echo -n "$MSGS" && $TAIL --pid=$$ -f /dev/null) | $LAKE serve)
+echo "done"

src/shell/CMakeLists.txt

@@ -177,12 +177,14 @@ FOREACH(T ${LEANTESTS})
   endif()
 ENDFOREACH(T)
 
-# Create a lake test for each subdirectory of `lake` which contains a `test.sh` file.
+# 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
-# 116: non-deterministic (`sleep`)
-file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/test.sh")
+file(GLOB_RECURSE LEANLAKETESTS
+  "${LEAN_SOURCE_DIR}/lake/test/test.sh"
+  "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
-  if(NOT T MATCHES ".*(lake-packages|bootstrap|116).*")
+  if(NOT T MATCHES ".*(lake-packages|bootstrap).*")
     GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
     GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
     add_test(NAME "leanlaketest_${DIR_NAME}"