chore: lake: cleanup tests (#4056)

Various tweaks and fixes to the Lake tests to make them cleaner and more
standardized.

src/lake/examples/ffi/app/lakefile.lean

@@ -6,8 +6,7 @@ package app
 require ffi from ".."/"lib"
 
 @[default_target]
-lean_exe app {
+lean_exe app where
   root := `Main
-}
 
 lean_lib Test

src/lake/examples/hello/lakefile.lean

@@ -6,6 +6,5 @@ package hello
 lean_lib Hello
 
 @[default_target]
-lean_exe hello {
+lean_exe hello where
   root := `Main
-}

src/lake/examples/targets/test.sh

@@ -20,7 +20,7 @@ fi
 ./clean.sh
 
 # Test error on nonexistent facet
-$LAKE build targets:noexistent && false || true
+$LAKE build targets:noexistent && exit 1 || true
 
 # Test custom targets and package, library, and module facets
 $LAKE build bark | awk '/bark/,/Bark!/' | wc -l | grep -q 2

src/lake/tests/badImport/test.sh

@@ -10,5 +10,5 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/2569
 # https://github.com/leanprover/lean4/issues/2415
 
-($LAKE build +X 2>&1 && exit 1 || true) | grep -F "X.lean"
-($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep -F "Lib.B"
+($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean"
+($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep --color -F "Lib.B"

src/lake/tests/clone/test.sh

@@ -30,7 +30,7 @@ HELLO_MAP="{\"hello\" : \"file://$(pwd)/hello\"}"
 cd test
 
 # test that `LAKE_PKG_URL_MAP` properly overwrites the config-specified Git URL
-LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep "file://"
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep --color "file://"
 # test that a second `lake update` is a no-op (with URLs)
 # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
 LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | diff - /dev/null
@@ -45,15 +45,15 @@ $LAKE update 2>&1 | diff - /dev/null
 test -d .lake/packages/hello
 # test that Lake produces no warnings
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
-./.lake/build/bin/test | grep "Hello, world"
+./.lake/build/bin/test | grep --color "Hello, world"
 
 # Test that Lake produces a warning if local changes are made to a dependency
 # See https://github.com/leanprover/lake/issues/167
 
 sed_i "s/world/changes/" .lake/packages/hello/Hello/Basic.lean
-git -C .lake/packages/hello diff --exit-code && false || true
-$LAKE build 3>&1 1>&2 2>&3 | grep "has local changes"
-./.lake/build/bin/test | grep "Hello, changes"
+git -C .lake/packages/hello diff --exit-code && exit 1 || true
+$LAKE build 3>&1 1>&2 2>&3 | grep --color "has local changes"
+./.lake/build/bin/test | grep --color "Hello, changes"
 git -C .lake/packages/hello reset --hard
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
 

src/lake/tests/clone/test/lakefile.lean

@@ -7,6 +7,5 @@ package test
 require hello from git "../hello"
 
 @[default_target]
-lean_exe test {
+lean_exe test where
   root := `Main
-}

src/lake/tests/depTree/test.sh

@@ -38,7 +38,7 @@ cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
 EOF
 $LAKE update -v
-grep "\"a\"" lake-manifest.json
+grep --color "\"a\"" lake-manifest.json
 git add .
 git config user.name test
 git config user.email [email protected]
@@ -59,7 +59,7 @@ cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
 EOF
 $LAKE update -v
-grep "\"a\"" lake-manifest.json
+grep --color "\"a\"" lake-manifest.json
 git add .
 git config user.name test
 git config user.email [email protected]
@@ -75,7 +75,7 @@ require b from git "../b" @ "master"
 require c from git "../c" @ "master"
 EOF
 # make sure we pick up the version from b's manifest (a@1)
-$LAKE update -v 2>&1 | grep 'first commit in a'
+$LAKE update -v 2>&1 | grep --color 'first commit in a'
 git add .
 git config user.name test
 git config user.email [email protected]
@@ -90,10 +90,10 @@ pushd b
 # b: a@1/init -> a@2
 $LAKE update -v
 # test 84: `lake update` does update
-git diff | grep -m1 manifest
+git diff | grep --color manifest
 sed_i 's/master/init/g' lakefile.lean
 # test 85: warn when manifest and configuration differ
-$LAKE resolve-deps -v 2>&1 | grep 'manifest out of date'
+$LAKE resolve-deps -v 2>&1 | grep --color 'manifest out of date'
 # b: a@1
 git reset --hard
 popd
@@ -109,7 +109,7 @@ popd
 pushd d
 $LAKE update -v
 # test 70: we do not update transitive depednecies
-! grep 'third commit in a' .lake/packages/a/A.lean
+grep --color 'third commit in a' .lake/packages/a/A.lean && exit 1 || true
 git diff --exit-code
 popd
 
@@ -133,10 +133,10 @@ pushd d
 # d: b@1 -> b@2 => a@1 -> a@3
 $LAKE update b -v
 # test 119: pickup a@3 and not a@4
-grep 'third commit in a' .lake/packages/a/A.lean
+grep --color 'third commit in a' .lake/packages/a/A.lean
 # test the removal of `c` from the manifest
-grep "\"c\"" lake-manifest.json
+grep --color "\"c\"" lake-manifest.json
 sed_i '/require c/d' lakefile.lean
 $LAKE update c -v
-grep "\"c\"" lake-manifest.json && false || true
+grep --color "\"c\"" lake-manifest.json && exit 1 || true
 popd

src/lake/tests/env/test.sh

@@ -15,12 +15,12 @@ $LAKE env printenv LAKE
 $LAKE env printenv LAKE_HOME
 $LAKE env printenv LEAN_GITHASH
 $LAKE env printenv LEAN_SYSROOT
-$LAKE env printenv LEAN_AR | grep ar
+$LAKE env printenv LEAN_AR | grep --color ar
 $LAKE env printenv LEAN_PATH
-$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep examples/hello
-$LAKE env printenv LEAN_SRC_PATH | grep lake
-$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep examples/hello
-$LAKE -d ../../examples/hello env printenv PATH | grep examples/hello
+$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep --color examples/hello
+$LAKE env printenv LEAN_SRC_PATH | grep --color lake
+$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep --color examples/hello
+$LAKE -d ../../examples/hello env printenv PATH | grep --color examples/hello
 
 # Test that `env` preserves the input environment for certain variables
 test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
@@ -30,8 +30,8 @@ test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo
 
 # Test `LAKE_PKG_URL_MAP` setting and errors
 test "`LAKE_PKG_URL_MAP='{"a":"a"}' $LAKE env printenv LAKE_PKG_URL_MAP`" = '{"a":"a"}'
-(LAKE_PKG_URL_MAP=foo $LAKE env 2>&1 || true) | grep invalid
-(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep invalid
+(LAKE_PKG_URL_MAP=foo $LAKE env 2>&1 || true) | grep --color invalid
+(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep --color invalid
 
 # Test that the platform-specific shared library search path is set
 if [ "$OS" = Windows_NT ]; then
@@ -40,9 +40,9 @@ elif [ "`uname`" = Darwin ]; then
 # MacOS's System Integrity Protection does not permit
 # us to spawn a `printenv` process with `DYLD_LIBRARY_PATH` set
 # https://apple.stackexchange.com/questions/212945/unable-to-set-dyld-fallback-library-path-in-shell-on-osx-10-11-1
-$LAKE env | grep DYLD_LIBRARY_PATH | grep lib/lean
-$LAKE -d ../../examples/hello env | grep DYLD_LIBRARY_PATH | grep examples/hello
+$LAKE env | grep DYLD_LIBRARY_PATH | grep --color lib/lean
+$LAKE -d ../../examples/hello env | grep DYLD_LIBRARY_PATH | grep --color examples/hello
 else
-$LAKE env printenv LD_LIBRARY_PATH  | grep lib/lean
-$LAKE -d ../../examples/hello env printenv LD_LIBRARY_PATH | grep examples/hello
+$LAKE env printenv LD_LIBRARY_PATH  | grep --color lib/lean
+$LAKE -d ../../examples/hello env printenv LD_LIBRARY_PATH | grep --color examples/hello
 fi

src/lake/tests/init/test.sh

@@ -15,25 +15,25 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 # Test `new` and `init` with bad template/langauge (should error)
 
-($LAKE new foo bar 2>&1 && false || true) | grep "unknown package template"
-($LAKE new foo .baz 2>&1 && false || true) | grep "unknown configuration language"
-($LAKE init foo bar 2>&1 && false || true) | grep "unknown package template"
-($LAKE init foo std.baz 2>&1 && false || true) | grep "unknown configuration language"
+($LAKE new foo bar 2>&1 && exit 1 || true) | grep --color "unknown package template"
+($LAKE new foo .baz 2>&1 && exit 1 || true) | grep --color "unknown configuration language"
+($LAKE init foo bar 2>&1 && exit 1 || true) | grep --color "unknown package template"
+($LAKE init foo std.baz 2>&1 && exit 1 || true) | grep --color "unknown configuration language"
 
 # Test package name validation (should error)
 # https://github.com/leanprover/lean4/issues/2637
 
-($LAKE new  .    2>&1 && false || true) | grep "illegal package name"
+($LAKE new  .    2>&1 && exit 1 || true) | grep --color "illegal package name"
 for cmd in new init; do
-($LAKE $cmd ..   2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd .... 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd '  ' 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd a/bc 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd a\\b 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd init 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd Lean 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd Lake 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd main 2>&1 && false || true) | grep "reserved package name"
+($LAKE $cmd ..   2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd .... 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd '  ' 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd a/bc 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd a\\b 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd init 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd Lean 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd Lake 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd main 2>&1 && exit 1 || true) | grep --color "reserved package name"
 done
 
 # Test default (std) template
@@ -142,4 +142,4 @@ popd
 
 # Test bare `init` on existing package (should error)
 
-($LAKE -d hello_world init 2>&1 && false || true) | grep "package already initialized"
+($LAKE -d hello_world init 2>&1 && exit 1 || true) | grep --color "package already initialized"

src/lake/tests/llvm-bitcode-gen/test.sh

@@ -12,15 +12,15 @@ if [[ ! $(lean --features) =~ LLVM ]]; then
 fi
 
 $LAKE update
-$LAKE build -v | grep "Main.bc.o" # check that we build using the bitcode object file.
+$LAKE build -v | grep --color "Main.bc.o" # check that we build using the bitcode object file.
 
 # If we have the LLVM backend, check that the `lakefile.lean` is aware of this.
-lake script run llvm-bitcode-gen/hasLLVMBackend | grep "true"
+lake script run llvm-bitcode-gen/hasLLVMBackend | grep --color true
 
 # If we have the LLVM backend in the Lean toolchain, then we expect this to
 # print `true`, as this queries the same flag that Lake queries to check the presence
 # of the LLVM toolchian.
-./.lake/build/bin/llvm-bitcode-gen | grep 'true'
+./.lake/build/bin/llvm-bitcode-gen | grep --color true
 
 # If we have the LLVM backend, check that lake builds bitcode artefacts.
 test -f .lake/build/ir/LlvmBitcodeGen.bc

src/lake/tests/lock/test.sh

@@ -22,7 +22,7 @@ test1_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test1.log)
 test -f .lake/build/lake.lock
 kill $test1_pid
-! wait $test1_pid
+wait $test1_pid  && exit 1 || true
 
 # Test build waits when lock file present
 touch test2.log
@@ -37,7 +37,7 @@ wait $test2_pid
 test ! -f .lake/build/lake.lock
 
 # Test build error still deletes lock file
-! $LAKE build Error
+$LAKE build Error && exit 1 || true
 test ! -f .lake/build/lake.lock
 
 # Test that removing the lock during build does not cause it to fail
@@ -47,4 +47,4 @@ test3_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test3.log)
 rm .lake/build/lake.lock
 wait $test3_pid
-cat test3.log | grep "deleted before the lock"
+cat test3.log | grep --color "deleted before the lock"

src/lake/tests/manifest/lake-manifest-v6.json

@@ -10,4 +10,4 @@
     "name": "bar",
     "inputRev?": null,
     "inherited": false}}],
- "name": "test"}
+ "name": "«foo-bar»"}

src/lake/tests/manifest/lake-manifest-v7.json

@@ -16,5 +16,5 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"}],
- "name": "test",
+ "name": "«foo-bar»",
  "lakeDir": ".lake"}

src/lake/tests/manifest/lakefile.lean

@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-package test
+package «foo-bar»
 
 require foo from "foo"
 require bar from git "bar"

src/lake/tests/manifest/test.sh

@@ -25,45 +25,43 @@ git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd
 
+LATEST_VER=v7
 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
 
+# Test an update produces the expected manifest of the latest version
+test_update() {
+  $LAKE update
+  sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
+  diff --strip-trailing-cr lake-manifest-$LATEST_VER.json lake-manifest.json
+}
+
 # ---
 # Test manifest manually upgrades from unsupported versions
 # ---
 
 # Test loading of a V4 manifest fails
 cp lake-manifest-v4.json lake-manifest.json
-($LAKE resolve-deps 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+($LAKE resolve-deps 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
 
 # Test package update fails as well
-($LAKE update bar 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+($LAKE update bar 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
 
-# Test bare update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+# Test bare update works
+test_update
 rm -rf .lake
 
 # ---
 # Test manifest automatically upgrades from supported versions
 # ---
 
-# Test successful loading of a V5 manifest
-cp lake-manifest-v5.json lake-manifest.json
-sed_i "s/253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f/$GIT_REV/g" lake-manifest.json
-$LAKE resolve-deps
-
-# Test update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
-
-# Test successful loading of a V6 manifest
-cp lake-manifest-v6.json lake-manifest.json
-sed_i "s/dab525a78710d185f3d23622b143bdd837e44ab0/$GIT_REV/g" lake-manifest.json
-$LAKE resolve-deps
+# Test successful load & update of a supported manifest version
+test_manifest() {
+  cp lake-manifest-$1.json lake-manifest.json
+  sed_i "s/$2/$GIT_REV/g" lake-manifest.json
+  $LAKE resolve-deps
+  test_update
+}
 
-# Test update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+test_manifest v5 253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f
+test_manifest v6 dab525a78710d185f3d23622b143bdd837e44ab0
+test_manifest v7 0538596b94a0510f55dc820cabd3bde41ad93c3e

src/lake/tests/meta/test.sh

@@ -10,18 +10,18 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # ---
 
 # Test `run_io`
-$LAKE resolve-deps -R 2>&1 | grep impure
-$LAKE resolve-deps 2>&1 | (grep impure && false || true)
+$LAKE resolve-deps -R 2>&1 | grep --color impure
+$LAKE resolve-deps 2>&1 | (grep --color impure && exit 1 || true)
 
 # Test `meta if` and command `do`
-$LAKE resolve-deps -R 2>&1 | (grep -E "foo|bar|baz|1|2" && false || true)
-$LAKE resolve-deps -R -Kbaz 2>&1 | grep baz
-$LAKE resolve-deps -R -Kenv=foo 2>&1 | grep foo
-$LAKE run print_env 2>&1 | grep foo
-$LAKE resolve-deps -R -Kenv=bar 2>&1 | grep bar
-$LAKE run print_env 2>&1 | grep bar
+$LAKE resolve-deps -R 2>&1 | (grep --color -E "foo|bar|baz|1|2" && exit 1 || true)
+$LAKE resolve-deps -R -Kbaz 2>&1 | grep --color baz
+$LAKE resolve-deps -R -Kenv=foo 2>&1 | grep --color foo
+$LAKE run print_env 2>&1 | grep --color foo
+$LAKE resolve-deps -R -Kenv=bar 2>&1 | grep --color bar
+$LAKE run print_env 2>&1 | grep --color bar
 
 # Test environment extension filtering
 # https://github.com/leanprover/lean4/issues/2632
 
-$LAKE run print_elab 2>&1 | grep elabbed-string
+$LAKE run print_elab 2>&1 | grep --color elabbed-string