diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 331e37458d..bd2c569714 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 53bdbe3be9..b0777e3bdf 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/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 diff --git a/src/lake/test/116/test.sh b/src/lake/test/116/test.sh index 7b20c45d2b..93b61d831d 100755 --- a/src/lake/test/116/test.sh +++ b/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" diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 93453b8a59..3a870b1772 100644 --- a/src/shell/CMakeLists.txt +++ b/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}"