diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 1528f2fd9c..00acc55848 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -137,7 +137,7 @@ rec { ln -sf ${lean-all}/* . ''; buildPhase = '' - ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES + ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)|laketest' -j$NIX_BUILD_CORES ''; installPhase = '' touch $out diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 005f20f323..b6ad916c5c 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -202,3 +202,10 @@ add_test(NAME leanpkgtest_user_attr_app export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr") + +add_test(NAME laketest + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/lake/examples" + COMMAND bash -c " + set -eu + export PATH=${LEAN_BIN}:$PATH + make LAKE=lake test")