chore: more verbose tests & related fixes (#8183)

This PR makes Lake tests much more verbose in output. It also fixes some bugs that had been missed due to disabled tests. Most significantly, the target specifier `@pkg` (e.g., in `lake build`) is now always interpreted as a package. It was previously ambiguously interpreted due to changes in #7909.
2025-04-30 21:20:50 -04:00 · 2025-04-30 21:20:50 -04:00 · 05153d66b1
commit 05153d66b1
parent ae5fe802ce
66 changed files with 917 additions and 617 deletions
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@ -74,7 +74,7 @@ def Package.maybeFetchBuildCache (self : Package) : FetchM (Job Bool) := do
@[inline]
 private def Package.optFacetDetails (self : Package) (facet : Name) : JobM String := do
  if (← getIsVerbose) then
-    return s!" (see '{self.name}:{facet}' for details)"
+    return s!" (see '{self.name}:{Name.eraseHead facet}' for details)"
  else
    return " (run with '-v' for details)"

@ -161,7 +161,7 @@ private def Package.mkOptBuildArchiveFacetConfig
  (getUrl : Package → JobM String) (headers : Array String := #[])
  [FamilyDef FacetOut facet Bool]
 : PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
-  withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
+  withRegisterJob s!"{pkg.name}:{Name.eraseHead facet}" (optional := true) <| Job.async do
  try
    let url ← getUrl pkg
    pkg.fetchBuildArchive url (archiveFile pkg) headers
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@ -170,12 +170,14 @@ def resolveTargetInWorkspace
    throw <| CliError.unknownTarget target

 private def resolveTargetLikeSpec
-  (ws : Workspace) (spec : String) (facet : Name) (isMaybePath := false)
+  (ws : Workspace) (spec : String) (facet : Name) (isMaybePath explicit := false)
 : Except CliError (Array BuildSpec) := do
  match spec.splitOn "/" with
  | [spec] =>
    if spec.isEmpty then
      resolvePackageTarget ws ws.root facet
+    else if explicit then
+      resolvePackageTarget ws (← parsePackageSpec ws spec) facet
    else
      resolveTargetInWorkspace ws (stringToLegalOrSimpleName spec) facet
  | [pkgSpec, targetSpec] =>
@ -201,7 +203,7 @@ def resolveTargetBaseSpec
 : EIO CliError (Array BuildSpec) := do
  if spec.startsWith "@" then
    let spec := spec.drop 1
-    resolveTargetLikeSpec ws spec facet
+    resolveTargetLikeSpec ws spec facet (explicit := true)
  else if spec.startsWith "+" then
    let mod := spec.drop 1 |>.toName
    if let some mod := ws.findTargetModule? mod then
--- a/src/lake/Makefile
+++ b/src/lake/Makefile
@ -4,7 +4,7 @@ LAKE ?= ./.lake/build/bin/lake
 # Suite Targets
 #-------------------------------------------------------------------------------

-TESTS := $(addprefix tests/, $(shell ls tests))
+TESTS := $(addprefix tests/, $(filter-out common.sh, $(shell ls tests)))
 EXAMPLES := $(addprefix examples/, $(filter-out bootstrap, $(shell ls examples)))

 default: build
--- a/src/lake/tests/api/keys.lean
+++ b/src/lake/tests/api/keys.lean
@ -23,23 +23,23 @@ open Lake DSL
 /-- info: Lake.BuildKey.facet (Lake.BuildKey.package `pkg) `facet -/
 #guard_msgs in #eval `@pkg:facet

-/-- info: Lake.BuildKey.packageTarget `pkg `target -/
-#guard_msgs in #eval `@pkg/target
+/-- info: Lake.BuildKey.packageTarget `pkg `tgt -/
+#guard_msgs in #eval `@pkg/tgt

-/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target) `facet -/
-#guard_msgs in #eval `@pkg/target:facet
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `tgt) `facet -/
+#guard_msgs in #eval `@pkg/tgt:facet

-/-- info: Lake.BuildKey.packageTarget `pkg `target.«_+» -/
-#guard_msgs in #eval `@pkg/+target
+/-- info: Lake.BuildKey.packageTarget `pkg `tgt.«_+» -/
+#guard_msgs in #eval `@pkg/+tgt

-/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target.«_+») `facet -/
-#guard_msgs in #eval `@pkg/+target:facet
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `tgt.«_+») `facet -/
+#guard_msgs in #eval `@pkg/+tgt:facet

-/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `target -/
-#guard_msgs in #eval `@/target
+/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `tgt -/
+#guard_msgs in #eval `@/tgt

-/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `target) `facet -/
-#guard_msgs in #eval `@/target:facet
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `tgt) `facet -/
+#guard_msgs in #eval `@/tgt:facet

 /-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `mod.«_+» -/
 #guard_msgs in #eval `@/+mod
@ -53,4 +53,4 @@ open Lake DSL
 def stx  := (`@pkg : PartialBuildKey)

 -- Test coercion to a target
-def coe : Array (Target Dynlib) := #[`@pkg/target:facet]
+def coe : Array (Target Dynlib) := #[`@pkg/tgt:facet]
--- a/src/lake/tests/api/test.sh
+++ b/src/lake/tests/api/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LEAN=${LEAN:-lean}
+source ../common.sh

 # Run Lean tests
-$LEAN keys.lean
+test_run env lean keys.lean
--- a/src/lake/tests/badImport/test.sh
+++ b/src/lake/tests/badImport/test.sh
@ -25,12 +25,10 @@ test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
 test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
 test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
 # Test a vanishing import within the workspace (lean4#3551)
-echo "[Test: Vanishing Import]"
-set -x
-touch Lib/Bogus.lean
-$LAKE build +Lib.B
-rm Lib/Bogus.lean
-set +x
+echo "# TEST: Vanishing Import"
+test_cmd touch Lib/Bogus.lean
+test_run build +Lib.B
+test_cmd rm Lib/Bogus.lean
 test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
 test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
 test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
@ -45,5 +43,5 @@ test_err "X.lean: bad import 'Lib.Bogus'" build X
 # Test an executable which imports a module containing a bad import
 test_err "B.lean: bad import 'Lib.Bogus'" build X1

-# cleanup
+# Cleanup
 rm -f produced.out
--- a/src/lake/tests/buildArgs/test.sh
+++ b/src/lake/tests/buildArgs/test.sh
@ -36,5 +36,5 @@ test_run build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib  --no-build
 test_run build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib  --no-build
 test_run build hello -R -KweakLinkArgs=-L.lake/build/lib  --no-build

-# cleanup
+# Cleanup
 rm -f produced.out
--- a/src/lake/tests/clone/clean.sh
+++ b/src/lake/tests/clone/clean.sh
@ -1,2 +1,3 @@
 rm -rf hello
 rm -rf test/.lake test/lake-manifest.json
+rm -f produced.out
--- a/src/lake/tests/clone/test.sh
+++ b/src/lake/tests/clone/test.sh
@ -1,19 +1,12 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-../../../.lake/build/bin/lake}
-
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
+source ../common.sh

 ./clean.sh

 # Test Lake's management of a single Git-cloned dependency.

+echo "# SETUP"
+set -x
 mkdir hello
 pushd hello
 $LAKE init hello
@ -26,42 +19,51 @@ git config user.email test@example.com
 git add --all
 git commit -m "initial commit"
 popd
+set +x

 HELLO_MAP="{\"hello\" : \"file://$(pwd)/hello\"}"

 cd test

+echo "# TESTS"
+
 # test that `LAKE_PKG_URL_MAP` properly overwrites the config-specified Git URL
-LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep --color "file://"
+LAKE_PKG_URL_MAP=$HELLO_MAP test_out "file://" update
 # 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 --keep-toolchain 2>&1 | diff - /dev/null
+LAKE_PKG_URL_MAP=$HELLO_MAP test_no_out update --keep-toolchain
 rm -rf .lake/packages

 # Test that Lake produces no warnings on a `lake build` after a `lake update`
 # See https://github.com/leanprover/lean4/issues/2427

-$LAKE update
+echo "# TEST: lake build after update"
+
+test_run update
 # test that a second `lake update` is a no-op (with file paths)
-$LAKE update --keep-toolchain 2>&1 | diff - /dev/null
+test_no_out update --keep-toolchain
 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 --color "Hello, world"
+test_no_warn build
+test_cmd_eq "Hello, world!" ./.lake/build/bin/test

 # Test that Lake produces a warning if local changes are made to a dependency
 # See https://github.com/leanprover/lake/issues/167

+echo "# TEST: Local changes"
+
 sed_i "s/world/changes/" .lake/packages/hello/Hello/Basic.lean
-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
+test_cmd_fails git -C .lake/packages/hello diff --exit-code
+test_out "has local changes" build
+test_cmd_eq "Hello, changes!" ./.lake/build/bin/test
+test_cmd git -C .lake/packages/hello reset --hard
+test_no_warn build

 # Test no `git fetch` on a `lake build` if already on the proper revision
 # See https://github.com/leanprover/lake/issues/104

+echo "# TEST: No fetch"
+
 TEST_URL=https://example.com/hello.git
 TEST_MAP="{\"hello\" : \"$TEST_URL\"}"

@ -69,4 +71,7 @@ TEST_MAP="{\"hello\" : \"$TEST_URL\"}"
 git -C .lake/packages/hello remote set-url origin $TEST_URL
 # build should succeed (do nothing) despite the invalid remote because
 # the remote should not be fetched; Lake should also not produce any warnings
-LAKE_PKG_URL_MAP=$TEST_MAP $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
+LAKE_PKG_URL_MAP=$TEST_MAP test_no_warn build
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/common.sh
+++ b/src/lake/tests/common.sh
@ -1,11 +1,22 @@
 set -euo pipefail

+# Lake configuration
+
 LAKE=${LAKE:-lake}
+echo "LAKE=$LAKE"
+
+# Platform-specific configuration
+
+OS="${OS:-}"
+echo "OS=$OS"
+
+UNAME="`uname`"
+echo "UNAME=$UNAME"

 if [ "${OS:-}" = Windows_NT ]; then
 LIB_PREFIX=
 SHARED_LIB_EXT=dll
-elif [ "`uname`" = Darwin ]; then
+elif [ "$UNAME" = Darwin ]; then
 LIB_PREFIX=lib
 SHARED_LIB_EXT=dylib
 else
@ -13,63 +24,160 @@ LIB_PREFIX=lib
 SHARED_LIB_EXT=so
 fi

-test_run() {
-  echo "[COMMAND]"
-  echo "$>" "$LAKE" "$@"
-  if "$LAKE" "$@" >produced.out 2>&1; then
-    rc=$?
-  else
-    rc=$?
-  fi
-  echo "Lake exited with code $rc"
-  echo "[OUTPUT]"
-  cat produced.out
-  return $rc
-}
+if [ "$UNAME" = Darwin ] || [ "$UNAME" = FreeBSD ]; then
+  sed_i() { sed -i '' "$@"; }
+  TAIL=gtail
+else
+  sed_i() { sed -i "$@"; }
+  TAIL=tail
+fi

-match_out() {
-  expected=$1; shift
-  echo "[MATCH \"$expected\"]"
-  if grep --color -F -- "$expected" produced.out; then
+# Test functions
+
+test_cmd() {
+  echo '$' "$@"
+  if "$@" 2>&1; then
    return 0
  else
-    echo "No match found."
+    rc=$?
+    echo "Program exited with code $rc"
+    return $rc
+  fi
+}
+
+test_exp() {
+  echo '$' test "$@"
+  test "$@"
+}
+
+test_cmd_fails() {
+  if test_cmd "$@"; then
+    echo "FAILURE: Program unexpectedly succeeded"
    return 1
+  else
+    return 0
+  fi
+}
+
+test_run() {
+  echo '$' lake "$@"
+  if "$LAKE" "$@" 2>&1; then
+    return 0
+  else
+    rc=$?
+    echo "Lake exited with code $rc"
+    return $rc
+  fi
+}
+
+test_fails() {
+  if test_run "$@"; then
+    echo "FAILURE: Lake unexpectedly succeeded"
+    return 1
+  else
+    return 0
+  fi
+}
+
+test_status() {
+  expected=$1; shift
+  if test_run "$@"; then rc=$?; else rc=$?; fi
+  if [ $rc = $expected ]; then
+    return 0
+  else
+    echo "FAILURE: Expected Lake to exit with code $expected."
+    return 1
+  fi
+}
+
+program_out() {
+  echo '$' "$@"
+  if "$@" >produced.out 2>&1; then
+    cat produced.out
+    return 0
+  else
+    rc=$?
+    cat produced.out
+    echo "Program exited with code $rc"
+    return $rc
+  fi
+}
+
+lake_out() {
+  echo '$' lake "$@"
+  if "$LAKE" "$@" >produced.out 2>&1; then
+    cat produced.out
+    return 0
+  else
+    rc=$?
+    cat produced.out
+    echo "Lake exited with code $rc"
+    return $rc
+  fi
+}
+
+match_text() {
+  echo "? grep -F \"$1\""
+  if grep --color -F -- "$1" $2; then
+    return 0
+  else
+    echo "No match found"
+    return 1
+  fi
+}
+
+no_match_text() {
+  echo "! grep -F \"$1\""
+  if grep --color -F -- "$1" $2; then
+    return 1
+  else
+    return 0
+  fi
+}
+
+no_match_pat() {
+  echo "! grep -E \"$1\""
+  if grep --color -E -- "$1" $2; then
+    return 1
+  else
+    return 0
  fi
 }

 test_out() {
  expected=$1; shift
-  if test_run "$@"; then rc=$?; else rc=$?; fi
-  match_out "$expected"
+  if lake_out "$@"; then rc=$?; else rc=$?; fi
+  match_text "$expected" produced.out
  return $rc
 }

-no_match_out() {
+test_cmd_out() {
  expected=$1; shift
-  echo "[NO MATCH \"$expected\"]"
-  if grep --color -F -- "$expected" produced.out; then
-    return 1
-  else
-    echo "No match found."
-    return 0
-  fi
+  if program_out "$@"; then rc=$?; else rc=$?; fi
+  match_text "$expected" produced.out
+  return $rc
 }

 test_not_out() {
  expected=$1; shift
-  if test_run "$@"; then rc=$?; else rc=$?; fi
-  no_match_out "$expected"
+  if lake_out "$@"; then rc=$?; else rc=$?; fi
+  no_match_text "$expected" produced.out
+  return $rc
+}
+
+test_not_pat() {
+  expected=$1; shift
+  if lake_out "$@"; then rc=$?; else rc=$?; fi
+  no_match_pat "$expected" produced.out
  return $rc
 }

 test_err() {
  expected=$1; shift
-  if test_run "$@"; then rc=$?; else rc=$?; fi
-  if match_out "$expected"; then
+  if lake_out "$@"; then rc=$?; else rc=$?; fi
+  if match_text "$expected" produced.out; then
    if [ $rc != 1 ]; then
-      echo "[OUTCOME]"
-      echo "Lake unexpectedly succeeded."
+      echo "FAILURE: Lake unexpectedly succeeded"
      return 1
    fi
  else
@ -79,7 +187,105 @@ test_err() {

 test_maybe_err() {
  expected=$1; shift
-  test_run "$@" || true
-  match_out "$expected"
+  lake_out "$@" || true
+  match_text "$expected" produced.out
 }

+check_diff() {
+  expected=$1; actual=$2
+  if diff -u --strip-trailing-cr "$expected" "$actual"; then
+    cat "$actual"
+    echo "Output matched expectations"
+    return 9
+  else
+    return 1
+  fi
+}
+
+test_out_diff() {
+  expected=$1; shift
+  echo '$' lake "$@"
+  if "$LAKE" "$@" >produced.out 2>&1; then rc=$?; else rc=$?; fi
+  if check_diff "$expected" produced.out; then
+    if [ $rc != 0 ]; then
+      echo "FAILURE: Program exited with code $rc"
+      return 1
+    fi
+  else
+    if [ $rc != 0 ]; then
+      echo "Program exited with code $rc"
+    fi
+  fi
+}
+
+test_err_diff() {
+  expected=$1; shift
+  echo '$' lake "$@"
+  if "$LAKE" "$@" >produced.out 2>&1; then rc=$?; else rc=$?; fi
+  if check_diff "$expected" produced.out; then
+    if [ $rc != 1 ]; then
+      echo "FAILURE: Lake unexpectedly succeeded"
+      return 1
+    fi
+  else
+    if [ $rc != 1 ]; then
+      echo "Lake exited with code $rc."
+    fi
+    return 0
+  fi
+}
+
+
+test_no_out() {
+  if lake_out "$@"; then rc=$?; else rc=$?; fi
+  diff produced.out /dev/null
+  return $rc
+}
+
+test_no_warn() {
+  echo '$' lake "$@"
+  if "$LAKE" "$@" 2>produced.out; then
+    diff produced.out /dev/null
+  else
+    rc=$?
+    cat produced.out
+    echo "FAILURE: Lake exited with code $rc"
+    return 1
+  fi
+}
+
+test_cmd_eq() {
+  expected=$1; shift
+  echo '$' "$@"
+  if "$@" >produced.out; then
+    echo "? output \"`cat produced.out`\" = \"$expected\""
+    if test "`cat produced.out`" = "$expected"; then
+      return 0
+    else
+      return 1
+    fi
+  else
+    rc=$?
+    cat produced.out
+    echo "FAILURE: Program exited with code $rc"
+    return 1
+  fi
+}
+
+test_eq() {
+  expected=$1; shift
+  echo '$' lake "$@"
+  if "$LAKE" "$@" >produced.out; then
+    echo "? output \"`cat produced.out`\" = \"$expected\""
+    if test "`cat produced.out`" = "$expected"; then
+      return 0
+    else
+      return 1
+    fi
+  else
+    rc=$?
+    cat produced.out
+    echo "FAILURE: Lake exited with code $rc"
+    return 1
+  fi
+}
--- a/src/lake/tests/depTree/test.sh
+++ b/src/lake/tests/depTree/test.sh
@ -1,14 +1,6 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-$PWD/../../.lake/build/bin/lake}
-
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
+source ../common.sh
+set -x

 ./clean.sh

--- a/src/lake/tests/driver/clean.sh
+++ b/src/lake/tests/driver/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/driver/test.sh
+++ b/src/lake/tests/driver/test.sh
@ -1,92 +1,101 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

 # Script driver
-$LAKE -f script.lean test | grep --color -F "script: []"
-$LAKE -f script.lean lint | grep --color -F "script: []"
-$LAKE -f script.lean test -- hello | grep --color "hello"
-$LAKE -f script.lean lint -- hello | grep --color "hello"
+echo "# TEST: Script driver"
+test_out "script: []" -f script.lean test
+test_out "script: []" -f script.lean lint
+test_out "hello" -f script.lean test -- hello
+test_out "hello" -f script.lean lint -- hello

 # Executable driver
-$LAKE -f exe.lean test | grep --color -F "exe: []"
-$LAKE -f exe.toml test | grep --color -F "exe: []"
-$LAKE -f exe.lean lint | grep --color -F "exe: []"
-$LAKE -f exe.toml lint | grep --color -F "exe: []"
-$LAKE -f exe.lean test -- hello | grep --color "hello"
-$LAKE -f exe.toml test -- hello | grep --color "hello"
-$LAKE -f exe.lean lint -- hello | grep --color "hello"
-$LAKE -f exe.toml lint -- hello | grep --color "hello"
+echo "# TEST: Excutable driver"
+test_out "exe: []" -f exe.lean test
+test_out "exe: []" -f exe.toml test
+test_out "exe: []" -f exe.lean lint
+test_out "exe: []" -f exe.toml lint
+test_out "hello" -f exe.lean test -- hello
+test_out "hello" -f exe.toml test -- hello
+test_out "hello" -f exe.lean lint -- hello
+test_out "hello" -f exe.toml lint -- hello

 # Library test driver
+echo "# TEST: Library test driver"
 rm -f .lake/build/lib/lean/Test.olean
-$LAKE -f lib.lean test | grep --color -F "Built Test"
+test_out "Built Test" -f lib.lean test
 rm -f .lake/build/lib/lean/Test.olean
-$LAKE -f lib.toml test | grep --color -F "Built Test"
-($LAKE -f lib.lean test -- hello 2>&1 && exit 1 || true) | grep --color "arguments cannot be passed"
-($LAKE -f lib.toml test -- hello 2>&1 && exit 1 || true) | grep --color "arguments cannot be passed"
+test_out "Built Test" -f lib.toml test
+test_err "arguments cannot be passed" -f lib.lean test -- hello
+test_err "arguments cannot be passed" -f lib.toml test -- hello

 # Upstream driver
+echo "# TEST: Driver from dependency"
 rm -f lake-manifest.json
-$LAKE -f dep.lean test | grep --color -F "dep: []"
-$LAKE -f dep.toml test | grep --color -F "dep: []"
-$LAKE -f dep.lean lint | grep --color -F "dep: []"
-$LAKE -f dep.toml lint | grep --color -F "dep: []"
-$LAKE -f dep.lean test -- hello | grep --color "hello"
-$LAKE -f dep.toml test -- hello | grep --color "hello"
-$LAKE -f dep.lean lint -- hello | grep --color "hello"
-$LAKE -f dep.toml lint -- hello | grep --color "hello"
+test_out "dep: []" -f dep.lean test
+test_out "dep: []" -f dep.toml test
+test_out "dep: []" -f dep.lean lint
+test_out "dep: []" -f dep.toml lint
+test_out "hello" -f dep.lean test -- hello
+test_out "hello" -f dep.toml test -- hello
+test_out "hello" -f dep.lean lint -- hello
+test_out "hello" -f dep.toml lint -- hello

 # Test runner
-$LAKE -f runner.lean test 2>&1 | grep --color -F " @[test_runner] has been deprecated"
-$LAKE -f runner.toml test
-$LAKE -f runner.lean check-test
-$LAKE -f runner.toml check-test
+echo "# TEST: Test runner"
+test_out " @[test_runner] has been deprecated" -f runner.lean test
+test_run -f runner.toml test
+test_run -f runner.lean check-test
+test_run -f runner.toml check-test

 # Driver validation
-($LAKE -f two.lean test 2>&1 && exit 1 || true) | grep --color "only one"
-($LAKE -f none.lean test 2>&1 && exit 1 || true) | grep --color "no test driver"
-($LAKE -f none.toml test 2>&1 && exit 1 || true) | grep --color "no test driver"
-($LAKE -f unknown.lean test 2>&1 && exit 1 || true) | grep --color "invalid test driver: unknown"
-($LAKE -f unknown.toml test 2>&1 && exit 1 || true) | grep --color "invalid test driver: unknown"
-($LAKE -f dep-unknown.lean test 2>&1 && exit 1 || true) | grep --color "unknown test driver package"
-($LAKE -f dep-unknown.toml test 2>&1 && exit 1 || true) | grep --color "unknown test driver package"
-($LAKE -f dep-invalid.lean test 2>&1 && exit 1 || true) | grep --color "invalid test driver"
-($LAKE -f dep-invalid.toml test 2>&1 && exit 1 || true) | grep --color "invalid test driver"
-($LAKE -f two.lean lint 2>&1 && exit 1 || true) | grep --color "only one"
-($LAKE -f none.lean lint 2>&1 && exit 1 || true) | grep --color "no lint driver"
-($LAKE -f none.toml lint 2>&1 && exit 1 || true) | grep --color "no lint driver"
-($LAKE -f unknown.lean lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver: unknown"
-($LAKE -f unknown.toml lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver: unknown"
-($LAKE -f dep-unknown.lean lint 2>&1 && exit 1 || true) | grep --color "unknown lint driver package"
-($LAKE -f dep-unknown.toml lint 2>&1 && exit 1 || true) | grep --color "unknown lint driver package"
-($LAKE -f dep-invalid.lean lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver"
-($LAKE -f dep-invalid.toml lint 2>&1 && exit 1 || true) | grep --color "invalid lint driver"
+echo "# TEST: Driver validation"
+test_err "only one" -f two.lean test
+test_err "no test driver" -f none.lean test
+test_err "no test driver" -f none.toml test
+test_err "invalid test driver: unknown" -f unknown.lean test
+test_err "invalid test driver: unknown" -f unknown.toml test
+test_err "unknown test driver package" -f dep-unknown.lean test
+test_err "unknown test driver package" -f dep-unknown.toml test
+test_err "invalid test driver" -f dep-invalid.lean test
+test_err "invalid test driver" -f dep-invalid.toml test
+test_err "only one" -f two.lean lint
+test_err "no lint driver" -f none.lean lint
+test_err "no lint driver" -f none.toml lint
+test_err "invalid lint driver: unknown" -f unknown.lean lint
+test_err "invalid lint driver: unknown" -f unknown.toml lint
+test_err "unknown lint driver package" -f dep-unknown.lean lint
+test_err "unknown lint driver package" -f dep-unknown.toml lint
+test_err "invalid lint driver" -f dep-invalid.lean lint
+test_err "invalid lint driver" -f dep-invalid.toml lint

 # Driver checker
-$LAKE -f exe.lean check-test
-$LAKE -f exe.toml check-test
-$LAKE -f exe.lean check-lint
-$LAKE -f exe.toml check-lint
-$LAKE -f dep.lean check-test
-$LAKE -f dep.toml check-test
-$LAKE -f dep.lean check-lint
-$LAKE -f dep.toml check-lint
-$LAKE -f script.lean check-test
-$LAKE -f script.lean check-lint
-$LAKE -f lib.lean check-test
-$LAKE -f two.lean check-test && exit 1 || true
-$LAKE -f two.lean check-lint && exit 1 || true
-$LAKE -f none.lean check-test && exit 1 || true
-$LAKE -f none.toml check-test && exit 1 || true
-$LAKE -f none.lean check-lint && exit 1 || true
-$LAKE -f none.toml check-lint && exit 1 || true
+echo "# TEST: Check driver"
+test_run -f exe.lean check-test
+test_run -f exe.toml check-test
+test_run -f exe.lean check-lint
+test_run -f exe.toml check-lint
+test_run -f dep.lean check-test
+test_run -f dep.toml check-test
+test_run -f dep.lean check-lint
+test_run -f dep.toml check-lint
+test_run -f script.lean check-test
+test_run -f script.lean check-lint
+test_run -f lib.lean check-test
+test_fails -f two.lean check-test
+test_fails -f two.lean check-lint
+test_fails -f none.lean check-test
+test_fails -f none.toml check-test
+test_fails -f none.lean check-lint
+test_fails -f none.toml check-lint

 # Build checker
-$LAKE -f build.lean check-build
-$LAKE -f build.toml check-build
-$LAKE -f none.lean check-build && exit 1 || true
-$LAKE -f none.toml check-build && exit 1 || true
+echo "# TEST: Check build"
+test_run -f build.lean check-build
+test_run -f build.toml check-build
+test_fails -f none.lean check-build
+test_fails -f none.toml check-build
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/env/clean.sh
+++ b/src/lake/tests/env/clean.sh
@ -0,0 +1 @@
+rm -f produced.out
--- a/src/lake/tests/env/test.sh
+++ b/src/lake/tests/env/test.sh
@ -1,49 +1,59 @@
 #!/usr/bin/env bash
-set -exo pipefail
+source ../common.sh

-LAKE=${LAKE:-../../.lake/build/bin/lake}
+./clean.sh

 # Test the functionality of `lake env`
 # Also test https://github.com/leanprover/lake/issues/179

 # Test `env` with no command
+echo "# TEST: Bare lake env"
 $LAKE env | grep ".*=.*"

+echo "# TEST: Variables in lake env"
 # Test installation variables are set
 # NOTE: `printenv` exits with code 1 if the variable is not set
-$LAKE env printenv LAKE
-$LAKE env printenv LAKE_HOME
-$LAKE env printenv LEAN
-$LAKE env printenv LEAN_GITHASH
-$LAKE env printenv LEAN_SYSROOT
-$LAKE env printenv LEAN_AR | grep --color ar
-$LAKE env printenv LEAN_PATH
-$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep --color hello
-$LAKE env printenv LEAN_SRC_PATH | grep --color lake
-$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep --color hello
-$LAKE -d ../../examples/hello env printenv PATH | grep --color hello
+test_out "lake" env printenv LAKE
+test_run env printenv LAKE_HOME
+test_out "lean" env printenv LEAN
+test_run env printenv LEAN_GITHASH
+test_run env printenv LEAN_SYSROOT
+test_out "ar" env printenv LEAN_AR
+test_run env printenv LEAN_PATH
+test_out "hello" -d ../../examples/hello env printenv LEAN_PATH
+test_out "lake" env printenv LEAN_SRC_PATH
+test_out "hello" -d ../../examples/hello env printenv LEAN_SRC_PATH
+test_out "hello" -d ../../examples/hello env printenv PATH

 # Test that `env` preserves the input environment for certain variables
-test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
-test "`LEAN_GITHASH=foo $LAKE env printenv LEAN_GITHASH`" = foo
-test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo
-test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo
+echo "# TEST: Setting variables for lake env"
+test_eq "foo" env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN
+LEAN_GITHASH=foo test_eq "foo" env printenv LEAN_GITHASH
+LEAN_AR=foo test_eq "foo" env printenv LEAN_AR
+LEAN_CC=foo test_eq "foo" env printenv LEAN_CC

 # 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 --color invalid
-(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep --color invalid
+echo "# TEST: LAKE_PKG_URL_MAP"
+LAKE_PKG_URL_MAP='{"a":"a"}' test_eq '{"a":"a"}' env printenv LAKE_PKG_URL_MAP
+LAKE_PKG_URL_MAP=foo test_err "invalid" env
+LAKE_PKG_URL_MAP=0 test_err "invalid" env

 # Test that the platform-specific shared library search path is set
+echo "# TEST: Platform-specific shared library search path"
 if [ "$OS" = Windows_NT ]; then
-$LAKE env which libleanshared.dll # DLL in `bin` directory is in `PATH`
-elif [ "`uname`" = Darwin ]; then
+test_run env which libleanshared.dll # DLL in `bin` directory is in `PATH`
+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
+set -x
 $LAKE env | grep DYLD_LIBRARY_PATH | grep --color lib/lean
 $LAKE -d ../../examples/hello env | grep DYLD_LIBRARY_PATH | grep --color examples/hello
+set +x
 else
-$LAKE env printenv LD_LIBRARY_PATH  | grep --color lib/lean
-$LAKE -d ../../examples/hello env printenv LD_LIBRARY_PATH | grep --color examples/hello
+test_out "lib/lean" env printenv LD_LIBRARY_PATH
+test_out "examples/hello" -d ../../examples/hello env printenv LD_LIBRARY_PATH
 fi
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/externLib/test.sh
+++ b/src/lake/tests/externLib/test.sh
@ -14,8 +14,8 @@ test_run -v exe test

 # Tests that a non-precompiled build does not load anything as a dynlib/plugin
 # https://github.com/leanprover/lean4/issues/4565
-$LAKE -v build test | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
-$LAKE -v -d ffi build test | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
+test_not_pat 'load-dynlib|plugin' -v build test
+test_not_pat 'load-dynlib|plugin' -v -d ffi build test

 # Cleanup
 rm -f produced.out
--- a/src/lake/tests/globs/test.sh
+++ b/src/lake/tests/globs/test.sh
@ -1,22 +1,20 @@
 #!/usr/bin/env bash
-set -euxo pipefail
+source ../common.sh

 ./clean.sh

-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
 # test that directory information is preserved during glob recursion
 # see https://github.com/leanprover/lake/issues/102

-$LAKE build TBA
-test -f .lake/build/lib/lean/TBA.olean
-test -f .lake/build/lib/lean/TBA/Eulerian.olean
-test -f .lake/build/lib/lean/TBA/Eulerian/A.olean
+test_run build TBA
+test_exp -f .lake/build/lib/lean/TBA.olean
+test_exp -f .lake/build/lib/lean/TBA/Eulerian.olean
+test_exp -f .lake/build/lib/lean/TBA/Eulerian/A.olean
 rm -rf .lake
-$LAKE -f lakefile.toml build TBA
-test -f .lake/build/lib/lean/TBA.olean
-test -f .lake/build/lib/lean/TBA/Eulerian.olean
-test -f .lake/build/lib/lean/TBA/Eulerian/A.olean
+test_run -f lakefile.toml build TBA
+test_exp -f .lake/build/lib/lean/TBA.olean
+test_exp -f .lake/build/lib/lean/TBA/Eulerian.olean
+test_exp -f .lake/build/lib/lean/TBA/Eulerian/A.olean

 # test that globs capture modules with non-Lean names
 # see https://github.com/leanprover/lake/issues/174
@ -24,10 +22,10 @@ test -f .lake/build/lib/lean/TBA/Eulerian/A.olean
 # also test that globs capture files in directories without a corresponding `.lean` file
 # see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20build.20all/near/370788618

-$LAKE build Test
-test -f .lake/build/lib/lean/Test/1.olean
-test -f .lake/build/lib/lean/Test/Subtest/1.olean
+test_run build Test
+test_exp -f .lake/build/lib/lean/Test/1.olean
+test_exp -f .lake/build/lib/lean/Test/Subtest/1.olean
 rm -rf .lake
-$LAKE -f lakefile.toml build Test
-test -f .lake/build/lib/lean/Test/1.olean
-test -f .lake/build/lib/lean/Test/Subtest/1.olean
+test_run -f lakefile.toml build Test
+test_exp -f .lake/build/lib/lean/Test/1.olean
+test_exp -f .lake/build/lib/lean/Test/Subtest/1.olean
--- a/src/lake/tests/init/clean.sh
+++ b/src/lake/tests/init/clean.sh
@ -1,3 +1,4 @@
+rm -f produced.out
 rm -rf hello
 rm -rf HelloWorld
 rm -rf hello-world
--- a/src/lake/tests/init/test.sh
+++ b/src/lake/tests/init/test.sh
@ -1,146 +1,154 @@
 #!/usr/bin/env bash
-set -euxo pipefail
+source ../common.sh

 ./clean.sh

-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
-
-LAKE1=${LAKE:-../../../.lake/build/bin/lake}
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
 # Test `new` and `init` with bad template/language (should error)

-($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"
+echo "# TEST: Template validation"
+test_err "unknown package template" new foo bar
+test_err "unknown configuration language" new foo .baz
+test_err "unknown package template" init foo bar
+test_err "unknown configuration language" init foo std.baz

 # Test package name validation (should error)
 # https://github.com/leanprover/lean4/issues/2637

-($LAKE new  .    2>&1 && exit 1 || true) | grep --color "illegal package name"
+echo "# TEST: Package name validation"
+test_err "illegal package name" new  .
 for cmd in new init; do
-($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"
+test_err "illegal package name" $cmd ..
+test_err "illegal package name" $cmd ....
+test_err "illegal package name" $cmd '  '
+test_err "illegal package name" $cmd a/bc
+test_err "illegal package name" $cmd a\\b
+test_err "reserved package name" $cmd init
+test_err "reserved package name" $cmd Lean
+test_err "reserved package name" $cmd Lake
+test_err "reserved package name" $cmd main
 done

 # Test default (std) template

-$LAKE new hello .lean
-$LAKE -d hello exe hello
+echo "# TEST: default template"
+test_run new hello .lean
+test_run -d hello exe hello
 test -f hello/.lake/build/lib/lean/Hello.olean
 rm -rf hello
-$LAKE new hello .toml
-$LAKE -d hello exe hello
+test_run new hello .toml
+test_run -d hello exe hello
 test -f hello/.lake/build/lib/lean/Hello.olean
 rm -rf hello

 # Test exe template

-$LAKE new hello exe.lean
+echo "# TEST: exe template"
+test_run new hello exe.lean
 test -f hello/Main.lean
-$LAKE -d hello exe hello
+test_run -d hello exe hello
 rm -rf hello
-$LAKE new hello exe.toml
+test_run new hello exe.toml
 test -f hello/Main.lean
-$LAKE -d hello exe hello
+test_run -d hello exe hello
 rm -rf hello

 # Test lib template

-$LAKE new hello lib.lean
-$LAKE -d hello build Hello
+echo "# TEST: lib template"
+test_run new hello lib.lean
+test_run -d hello build Hello
 test -f hello/.lake/build/lib/lean/Hello.olean
 rm -rf hello
-$LAKE new hello lib.toml
-$LAKE -d hello build Hello
+test_run new hello lib.toml
+test_run -d hello build Hello
 test -f hello/.lake/build/lib/lean/Hello.olean
 rm -rf hello

 # Test math template

-$LAKE new qed math.lean || true # ignore toolchain download errors
+echo "# TEST: math template"
+test_run new qed math.lean || true # ignore toolchain download errors
 # Remove the require, since we do not wish to download mathlib during tests
 sed_i '/^require.*/{N;d;}' qed/lakefile.lean
-$LAKE -d qed build Qed
+test_run -d qed build Qed
 test -f qed/.lake/build/lib/lean/Qed.olean
 rm -rf qed
-$LAKE new qed math.toml || true # ignore toolchain download errors
+test_run new qed math.toml || true # ignore toolchain download errors
 # Remove the require, since we do not wish to download mathlib during tests
 sed_i '/^\[\[require\]\]/{N;N;N;d;}' qed/lakefile.toml
-$LAKE -d qed build Qed
+test_run -d qed build Qed
 test -f qed/.lake/build/lib/lean/Qed.olean

 # Test `init .`

+echo "# TEST: init ."
 mkdir hello
 pushd hello
-$LAKE1 init .
-$LAKE1 exe hello
+test_run init .
+test_run exe hello
 popd

 # Test creating packages with uppercase names
 # https://github.com/leanprover/lean4/issues/2540

-$LAKE new HelloWorld
-$LAKE -d HelloWorld exe helloworld
+echo "# TEST: Uppercase package names"
+test_run new HelloWorld
+test_run -d HelloWorld exe helloworld

 # Test creating multi-level packages with a `.`

-$LAKE new hello.world
-$LAKE -d hello-world exe hello-world
+echo "# TEST: Packages with a `.`"
+test_run new hello.world
+test_run -d hello-world exe hello-world
 test -f hello-world/Hello/World/Basic.lean

-$LAKE new hello.exe exe
-$LAKE -d hello-exe exe hello-exe
+test_run new hello.exe exe
+test_run -d hello-exe exe hello-exe

 # Test creating packages with a `-` (i.e., a non-identifier package name)
 # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20new.20lean-data

-$LAKE new lean-data
-$LAKE -d lean-data exe lean-data
+echo "# TEST: Non-identifier package names"
+test_run new lean-data
+test_run -d lean-data exe lean-data

 # Test creating packages starting with digits (i.e., a non-identifier library name)
 # https://github.com/leanprover/lean4/issues/2865

-$LAKE new 123-hello
-$LAKE -d 123-hello exe 123-hello
+echo "# TEST: Non-identifier library names"
+test_run new 123-hello
+test_run -d 123-hello exe 123-hello

 # Test creating packages with components that contain `.`s
 # https://github.com/leanprover/lean4/issues/2999

 # the unicode name is improperly encoded on windows for non-Lake reasons
 if [ "$OSTYPE" != "cygwin" -a "$OSTYPE" != "msys" ]; then
-  $LAKE new «A.B».«C.D»
-  $LAKE -d A-B-C-D exe a-b-c-d
+  echo "# TEST: Escaped names"
+  test_run new «A.B».«C.D»
+  test_run -d A-B-C-D exe a-b-c-d
 fi

 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128

-$LAKE new meta
-$LAKE -d meta exe meta
+echo "# TEST: Keyword names"
+test_run new meta
+test_run -d meta exe meta

 # Test `init` with name

+echo "# TEST: init <name>"
 mkdir hello_world
 pushd hello_world
-$LAKE1 init hello_world exe
-$LAKE1 exe hello_world
+test_run init hello_world exe
+test_run exe hello_world
 popd

 # Test bare `init` on existing package (should error)

-($LAKE -d hello_world init 2>&1 && exit 1 || true) | grep --color "package already initialized"
+echo "# TEST: init existing"
+test_err "package already initialized" -d hello_world init
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/inputFile/clean.sh
+++ b/src/lake/tests/inputFile/clean.sh
@ -1,2 +1,2 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
 rm -rf inputs lakefile.produced.lean lakefileAlt.produced.toml
--- a/src/lake/tests/inputFile/test.sh
+++ b/src/lake/tests/inputFile/test.sh
@ -1,61 +1,69 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

+# Setup directory structure
+echo "# SETUP"
 ./setup.sh

-# Validate configuration
-$LAKE -q resolve-deps 2>&1 | diff - /dev/null
+# Valdiate configuration
+echo "# TEST: Configuration"
+test_no_out -q resolve-deps

-# Test initial directory structure
-$LAKE exe test | diff -u --strip-trailing-cr <(cat << 'EOF'
+# Validate initial directory structure
+echo "# TEST: Directory structure"
+test_out_diff <(cat << 'EOF'
 foo
 bar
 baz
 untraced
 untraced
 EOF
-) -
+) exe test

-# Validate Lean configuration
-$LAKE -f lakefileAlt.lean translate-config toml lakefileAlt.produced.toml 2>&1 | diff - /dev/null
-diff -u --strip-trailing-cr lakefileAlt.expected.toml lakefileAlt.produced.toml
-$LAKE -f lakefileAlt.lean -q build --no-build 2>&1 | diff - /dev/null
+# Test Lean<->TOML equivalence
+echo "# TEST: Lean->TOML translation"
+test_no_out -f lakefileAlt.lean translate-config toml lakefileAlt.produced.toml
+test_cmd diff -u --strip-trailing-cr lakefileAlt.expected.toml lakefileAlt.produced.toml
+test_no_out -f lakefileAlt.lean -q build --no-build
+echo "# TEST: TOML->Lean translation"
+test_no_out translate-config lean lakefile.produced.lean
+test_cmd diff -u --strip-trailing-cr lakefile.expected.lean lakefile.produced.lean
+test_no_out -f lakefile.expected.lean -q build --no-build

-# Validate TOML->Lean translation
-$LAKE translate-config lean lakefile.produced.lean 2>&1 | diff - /dev/null
-diff -u --strip-trailing-cr lakefile.expected.lean lakefile.produced.lean
-$LAKE -f lakefile.expected.lean -q build --no-build 2>&1 | diff - /dev/null
-
-# Test input file target
-cat "`$LAKE query foo`" | diff -u --strip-trailing-cr <(echo foo) -
-
-# Test input directory target
+# Test input targets
+echo "# TEST: input_file target"
+test_run query foo
+test_cmd diff -u --strip-trailing-cr <(echo foo) "`$LAKE query foo`"
+echo "# TEST: input_dir target"
+test_run query barz
 cat `$LAKE query barz` | diff -u --strip-trailing-cr <(cat << 'EOF'
 bar
 baz
 EOF
 ) -

-# Test input file dependency
+# Test input dependencies
+echo "# TEST: input_file dependency"
 echo traced > inputs/foo.txt
-$LAKE exe test foo | diff -u --strip-trailing-cr <(echo traced) -
-
-# Test input directory dependency
+test_eq "traced" exe test foo
+echo "# TEST: input_dir dependency"
 echo traced > inputs/barz/bar.txt
-$LAKE exe test bar | diff -u --strip-trailing-cr <(echo traced) -
+test_eq "traced" exe test bar
 echo traced > inputs/barz/baz.txt
-$LAKE exe test baz | diff -u --strip-trailing-cr <(echo traced) -
+test_eq "traced" exe test baz

 # Test untraced dependencies
+echo "# TEST: Untraced dependencies"
 echo traced > inputs/untraced.txt
 echo traced > inputs/barz/untraced.txt
-$LAKE exe test | diff -u --strip-trailing-cr <(cat << 'EOF'
+test_out_diff <(cat << 'EOF'
 traced
 traced
 traced
 untraced
 untraced
 EOF
-) -
+) exe test
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/kinds/test.sh
+++ b/src/lake/tests/kinds/test.sh
@ -1,21 +1,22 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
+source ../common.sh
 ./clean.sh

 # setup directory structure
+echo "# SETUP"
+set -x
 mkdir -p files
 touch files/Lib.lean
 echo "def main : IO Unit := pure ()" > files/exe.lean
 touch files/test.txt
+set +x

 # Test that targets have their expected data kinds
-$LAKE query-kind exe | diff -u --strip-trailing-cr <(echo filepath) -
-$LAKE query-kind Lib:static | diff -u --strip-trailing-cr <(echo filepath) -
-$LAKE query-kind Lib:shared | diff -u --strip-trailing-cr <(echo dynlib) -
-$LAKE query-kind inFile | diff -u --strip-trailing-cr <(echo filepath) -
-$LAKE query-kind inDir | diff -u --strip-trailing-cr <(echo [anonymous]) -
-$LAKE query-kind pathTarget | diff -u --strip-trailing-cr <(echo filepath) -
-$LAKE query-kind dynlibTarget | diff -u --strip-trailing-cr <(echo dynlib) -
+echo "# TEST: Target query kinds"
+test_eq "filepath" query-kind exe
+test_eq "filepath" query-kind Lib:static
+test_eq "dynlib" query-kind Lib:shared
+test_eq "filepath" query-kind inFile
+test_eq "[anonymous]" query-kind inDir
+test_eq "filepath" query-kind pathTarget
+test_eq "dynlib" query-kind dynlibTarget
--- a/src/lake/tests/lean/clean.sh
+++ b/src/lake/tests/lean/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/lean/test.sh
+++ b/src/lake/tests/lean/test.sh
@ -5,10 +5,7 @@ source ../common.sh

 # Test running a Lean file works and builds its imports
 test_out 'Hello from the library foo!' lean Test.lean
-
-set -x
-test -f .lake/build/lib/lean/Lib.olean
-set +x
+test_exp -f .lake/build/lib/lean/Lib.olean

 # Test running a main function of a Lean file
 test_out 'Hello Bob!' lean Test.lean -- --run Test.lean Bob
@ -16,3 +13,6 @@ test_out 'Hello Bob!' lean Test.lean -- --run Test.lean Bob
 # Test that Lake uses module-specific configuration
 # if the source file is a module in the workspace
 test_out '-Dweak.foo="bar"' -v lean Lib/Basic.lean
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/llvm-bitcode-gen/clean.sh
+++ b/src/lake/tests/llvm-bitcode-gen/clean.sh
@ -1 +1 @@
-rm -rf .lake
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/llvm-bitcode-gen/test.sh
+++ b/src/lake/tests/llvm-bitcode-gen/test.sh
@ -1,27 +1,31 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../build/bin/lake}
+source ../common.sh

 ./clean.sh

+test_run update
+
 # Skip test if we don't have LLVM backend in the Lean toolchain
-if [[ ! $(lean --features) =~ LLVM ]]; then
+echo "# Check if LLVM enabled"
+if [[ ! $($LAKE env lean --features) =~ LLVM ]]; then
  echo "Skipping test: 'lean' does not have LLVM backend enabled"
  exit 0
 fi

-$LAKE update
-$LAKE build -v | grep --color "Main.bc.o" # check that we build using the bitcode object file.
+echo "# TESTS"
+test_out "Main.bc.o" build -v  # 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 --color true
+test_out "true" script run llvm-bitcode-gen/hasLLVMBackend

 # 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 --color true
+test_out -q exe 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
 test -f .lake/build/ir/Main.bc
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/logLevel/clean.sh
+++ b/src/lake/tests/logLevel/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/logLevel/test.sh
+++ b/src/lake/tests/logLevel/test.sh
@ -1,18 +1,15 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-exit 0  # TODO: flaky test disabled
-
-# test disabled 
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

 # Test failure log level

+echo "# TEST: Failure log level"
+
 log_fail_target() {
-  ($LAKE build "$@" && exit 1 || true) | grep --color foo
-  ($LAKE build "$@" && exit 1 || true) | grep --color foo # test replay
+  test_err "foo" build "$@"
+  test_err "foo" build "$@" # test replay
 }

 log_fail_target topTrace --fail-level=trace
@ -31,12 +28,14 @@ log_fail Error

 # Test output log level

+echo "# TEST: Output log level"
+
 log_empty() {
  lv=$1; shift
  rm -f .lake/build/art$lv
-  $LAKE build art$lv "$@" | grep --color foo && exit 1 || true
-  $LAKE build art$lv -v # test whole log was saved
-  $LAKE build art$lv "$@" | grep --color foo && exit 1 || true # test replay
+  test_not_out "foo" build art$lv "$@"
+  test_run build art$lv -v # test whole log was saved
+  test_not_out "foo" build art$lv "$@" # test replay
 }

 log_empty Info -q
@ -49,9 +48,8 @@ log_empty Trace

 # Test configuration-time output log level

-$LAKE resolve-deps -R -Klog=info 2>&1 | grep --color "info:"
-$LAKE resolve-deps -R -Klog=info -q 2>&1 |
-  grep --color "info:"  && exit 1 || true
-$LAKE resolve-deps -R -Klog=warning 2>&1 | grep --color "warning:"
-$LAKE resolve-deps -R -Klog=warning --log-level=error 2>&1 |
-  grep --color "warning:" && exit 1 || true
+echo "# TEST: Configuration log level"
+test_out "info:" resolve-deps -R -Klog=info
+test_not_out "info:" resolve-deps -R -Klog=info -q
+test_out "warning:" resolve-deps -R -Klog=warning
+test_not_out "warning:" resolve-deps -R -Klog=warning --log-level=error
--- a/src/lake/tests/manifest/clean.sh
+++ b/src/lake/tests/manifest/clean.sh
@ -1 +1 @@
-rm -rf .lake foo/.lake bar/.git lake-packages lake-manifest.json
+rm -rf .lake foo/.lake bar/.git lake-packages lake-manifest.json produced.out
--- a/src/lake/tests/manifest/test.sh
+++ b/src/lake/tests/manifest/test.sh
@ -1,20 +1,13 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
+source ../common.sh

 ./clean.sh

 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the bar repository on each test. This requires updating the
 # locked manifest to the new hash to ensure things work properly.
+echo "# SETUP"
+set -x
 pushd bar
 git init
 git checkout -b master
@ -24,12 +17,13 @@ git add --all
 git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd
+set +x

 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'

 # Test an update produces the expected manifest of the latest version
 test_update() {
-  $LAKE update
+  test_run update
  sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
  diff --strip-trailing-cr lake-manifest-latest.json lake-manifest.json
 }
@ -40,10 +34,10 @@ test_update() {

 # Test loading of a V4 manifest fails
 cp lake-manifest-v4.json lake-manifest.json
-($LAKE resolve-deps 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '0.4.0'"
+test_err "incompatible manifest version '0.4.0'" resolve-deps

 # Test package update fails as well
-($LAKE update bar 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '0.4.0'"
+test_err "incompatible manifest version '0.4.0'" update bar

 # Test bare update works
 test_update
@ -57,7 +51,7 @@ rm -rf .lake
 test_manifest() {
  cp lake-manifest-$1.json lake-manifest.json
  sed_i "s/$LOCKED_REV/$GIT_REV/g" lake-manifest.json
-  $LAKE resolve-deps
+  test_run resolve-deps
  test_update
 }

@ -66,3 +60,6 @@ test_manifest v6
 test_manifest v7
 test_manifest v1.0.0
 test_manifest v1.1.0
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/meta/clean.sh
+++ b/src/lake/tests/meta/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/meta/test.sh
+++ b/src/lake/tests/meta/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -10,18 +8,23 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # ---

 # Test `run_io`
-$LAKE resolve-deps -R 2>&1 | grep --color impure
-$LAKE resolve-deps 2>&1 | (grep --color impure && exit 1 || true)
+echo "# TEST: run_io"
+test_out "impure" resolve-deps -R
+test_not_out "impure" resolve-deps

 # Test `meta if` and command `do`
-$LAKE resolve-deps -R 2>&1 | (grep --color -E "foo|bar|baz|lorem|ipsum" && 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
+echo "# TEST: meta if"
+test_not_pat "foo|bar|baz|lorem|ipsum"  resolve-deps -R
+test_out "baz" resolve-deps -R -Kbaz
+test_out "foo" resolve-deps -R -Kenv=foo
+test_out "foo" run print_env
+test_out "bar" resolve-deps -R -Kenv=bar
+test_out "bar" run print_env

 # Test environment extension filtering
 # https://github.com/leanprover/lean4/issues/2632

-$LAKE run print_elab 2>&1 | grep --color elabbed-string
+test_out "elabbed-string" run print_elab
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/noBuild/clean.sh
+++ b/src/lake/tests/noBuild/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/noBuild/test.sh
+++ b/src/lake/tests/noBuild/test.sh
@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
+source ../common.sh

 # Tests that Lake properly exits before normal builds occur
 # when `--no-build` is passed on the command line.
@ -7,18 +7,22 @@ set -euxo pipefail
 ./clean.sh

 NO_BUILD_CODE=3
-LAKE=${LAKE:-../../.lake/build/bin/lake}

 # Test `--no-build` for setup-file and module builds (`buildUnlessUpToDate`)
-$LAKE setup-file ./Irrelevant.lean Test --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
+echo "# TEST: --no-build setup-file & modules"
+test_status $NO_BUILD_CODE setup-file bogus Test --no-build
 test ! -f .lake/build/lib/lean/Test.olean
-$LAKE build Test
+test_run build Test
 test -f .lake/build/lib/lean/Test.olean
-$LAKE setup-file ./Irrelevant.lean Test --no-build
+test_run setup-file bogus Test --no-build

 # Test `--no-build` for file builds (`buildFileUnlessUpToDate`)
-$LAKE build +Test:c.o.export --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
+echo "# TEST: --no-build file"
+test_status $NO_BUILD_CODE build +Test:c.o.export --no-build
 test ! -f .lake/build/ir/Test.c.o.export
-$LAKE build +Test:c.o.export
+test_run build +Test:c.o.export
 test -f .lake/build/ir/Test.c.o.export
-$LAKE build +Test:c.o.export --no-build
+test_run build +Test:c.o.export --no-build
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/noRelease/clean.sh
+++ b/src/lake/tests/noRelease/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json dep/.lake dep/.git
+rm -rf produced.out .lake lake-manifest.json dep/.lake dep/.git
--- a/src/lake/tests/noRelease/test.sh
+++ b/src/lake/tests/noRelease/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -12,6 +10,8 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the bar repository on each test. This requires updating the
 # locked manifest to the new hash to ensure things work properly.
+echo "# SETUP"
+set -x
 pushd dep
 git init
 git checkout -b master
@ -28,60 +28,70 @@ popd
 $LAKE update
 # Remove the release tag from the local copy
 git -C .lake/packages/dep tag -d release
+set +x

-# Test that a direct invocation fo `lake build *:release` fails
-($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << EOF
+# Test that a direct invocation of `lake build *:release` fails
+echo "# TEST: Direct fetch"
+test_err_diff <(cat << EOF
 ✖ [2/2] Running dep:release
 error: failed to fetch GitHub release (run with '-v' for details)
 Some required builds logged failures:
 - dep:release
+error: build failed
 EOF
-) -
+) build dep:release

 # Test that an indirect fetch on the release does not cause the build to fail
-$LAKE build Test | diff -u --strip-trailing-cr <(cat << EOF
+echo "# TEST: Indirect fetch"
+test_out_diff <(cat << EOF
 ⚠ [3/6] Ran dep:extraDep
 warning: building from source; failed to fetch GitHub release (run with '-v' for details)
 ✔ [4/6] Built Dep
 ✔ [5/6] Built Test
 Build completed successfully.
 EOF
-) -
+) build Test

 # Test download failure
-$LAKE update # re-fetch release tag
-($LAKE -v build dep:release && exit 1 || true) | grep --color "curl"
+echo "# TEST: Download failure"
+test_run update # re-fetch release tag
+test_err "curl" -v build dep:release

 # Test automatic cloud release unpacking
+echo "# TEST: Automaticcloud release unpacking"
 mkdir -p .lake/packages/dep/.lake/build
-$LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
-test -f .lake/packages/dep/.lake/release.tgz
+test_out "packing" -d .lake/packages/dep pack
+test_exp -f .lake/packages/dep/.lake/release.tgz
 echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
 rm -rf .lake/packages/dep/.lake/build
-$LAKE build dep:release -v | grep --color "tar"
-test -d .lake/packages/dep/.lake/build
+test_out "tar" build dep:release -v
+test_exp -d .lake/packages/dep/.lake/build

 # Test that the job prints nothing if the archive is already fetched and unpacked
-$LAKE build dep:release | diff -u --strip-trailing-cr <(cat << 'EOF'
+echo "# TEST: Quiet if fetched"
+test_out_diff <(cat << 'EOF'
 Build completed successfully.
 EOF
-) -
+) build dep:release

 # Test that releases do not contaminate downstream jobs
-$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
+echo "# TEST: Downstream job contamination"
+test_out_diff <(cat << 'EOF'
 Build completed successfully.
 EOF
-) -
+) build Test

 # Test retagging
-git -C dep tag -d release
-git -C dep tag release
+echo "# TEST: Retagging"
+test_cmd git -C dep tag -d release
+test_cmd git -C dep tag release
 NEW_REV=`git -C dep rev-parse release`
-test ! "$INIT_REV" = "$NEW_REV"
-test `git -C .lake/packages/dep rev-parse HEAD` = "$INIT_REV"
-$LAKE update
-test `git -C .lake/packages/dep rev-parse HEAD` = "$NEW_REV"
-$LAKE build dep:release
+test_exp ! "$INIT_REV" = "$NEW_REV"
+test_cmd_eq "$INIT_REV" git -C .lake/packages/dep rev-parse HEAD
+test_run update
+test_cmd_eq "$NEW_REV" git -C .lake/packages/dep rev-parse HEAD
+test_run build dep:release

-# Cleanup git repo
+# Cleanup
 rm -rf dep/.git
+rm -f prdouced.out
--- a/src/lake/tests/online/clean.sh
+++ b/src/lake/tests/online/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/online/test.sh
+++ b/src/lake/tests/online/test.sh
@ -1,68 +1,70 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 export ELAN_TOOLCHAIN=test

 ./clean.sh
+echo "# TEST: Request Errors"
 # Tests requiring a package not in the index
-($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
-  grep --color "package not found on Reservoir"
+test_err "package not found on Reservoir" -f bogus-dep.toml update
 # Tests a request error
-(RESERVOIR_API_URL=example.com $LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
-  grep --color "server returned invalid JSON"
-(RESERVOIR_API_URL=example.com $LAKE -f bogus-dep.toml update -v 2>&1 && exit 1 || true) |
-  grep --color "Reservoir responded with"
+RESERVOIR_API_URL=example.com \
+  test_err "server returned invalid JSON" -f bogus-dep.toml update
+RESERVOIR_API_URL=example.com \
+  test_err "Reservoir responded with" -f bogus-dep.toml update -v

 ./clean.sh
-$LAKE -f git.toml update --keep-toolchain
+echo "# TEST: Non-Reservoir"
+test_run -f git.toml update --keep-toolchain
 # Test that barrels are not fetched for non-Reservoir dependencies
-$LAKE -v -f git.toml build @Cli:extraDep |
-  grep --color "Cli:optBarrel" && exit 1 || true
+test_not_out "Cli:optBarrel" -v -f git.toml build @Cli:extraDep

 ./clean.sh
-$LAKE -f barrel.lean update --keep-toolchain
+echo "# TEST: Resveroir"
+test_run -f barrel.lean update --keep-toolchain
 # Test that a barrel is not fetched for an unbuilt dependency
-$LAKE -v -f barrel.lean build @test:extraDep |
-  grep --color "Cli:optBarrel" && exit 1 || true
+echo "# TEST: Unbuilt"
+test_not_out "Cli:optBarrel" -v -f barrel.lean build @test:extraDep
 # Test that barrels are not fetched after the build directory is created.
+echo "# TEST: Build directory"
 mkdir -p .lake/packages/Cli/.lake/build
-($LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
+test_not_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep
 rmdir .lake/packages/Cli/.lake/build
 # Test that barrels are not fetched without a toolchain
-(ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-($LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
-  grep --color "toolchain=test"
+echo "# TEST: Toolchain"
+ELAN_TOOLCHAIN= test_not_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep
+test_err "toolchain=test" -v -f barrel.lean build @Cli:barrel
 # Test that fetch failures are only shown in verbose mode
-$LAKE -v -f barrel.lean build @Cli:extraDep |
-  grep --color "Cli:optBarrel"
-$LAKE -f barrel.lean build @Cli:extraDep |
-  grep --color "Cli:optBarrel" && exit 1 || true
+echo "# TEST: Verbosity"
+test_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep
+test_not_out "Cli:optBarrel" -f barrel.lean build @Cli:extraDep
 # Test cache toggle
-(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-($LAKE -v -f barrel.lean build @Cli:extraDep --no-cache) |
-  grep --color "Cli:optBarrel" && exit 1 || true
-(LAKE_NO_CACHE=1 $LAKE -v -f barrel.lean build @Cli:extraDep --try-cache) |
-  grep --color "Cli:optBarrel"
+echo "# TEST: Cache toggle"
+LAKE_NO_CACHE=1 test_not_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep
+test_not_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep --no-cache
+LAKE_NO_CACHE=1 test_out "Cli:optBarrel" -v -f barrel.lean build @Cli:extraDep --try-cache
 # Test barrel download
-(ELAN_TOOLCHAIN= $LAKE -v -f barrel.lean build @Cli:barrel && exit 1 || true) |
-  grep --color "Lean toolchain not known"
+echo "# TEST: Download"
+ELAN_TOOLCHAIN= \
+  test_err "Lean toolchain not known" -v -f barrel.lean build @Cli:barrel
 ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
-  $LAKE -v -f barrel.lean build @Cli:barrel
-ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
-LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
-  $LAKE -f barrel.lean build Cli --no-build
+  test_run -v -f barrel.lean build @Cli:barrel
+# FIXME: Update
+# ELAN_TOOLCHAIN=leanprover/lean4:v4.11.0 \
+# LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \
+#   test_run -f barrel.lean build Cli --no-build

 ./clean.sh
-$LAKE -f require.lean update -v --keep-toolchain
-test -d .lake/packages/doc-gen4
-$LAKE -f require.lean resolve-deps  # validate manifest
+echo "# TEST: Resvoir require (Lean)"
+test_run -f require.lean update -v --keep-toolchain
+test_exp -d .lake/packages/doc-gen4
+test_run -f require.lean resolve-deps  # validate manifest

 ./clean.sh
-$LAKE -f require.toml update -v --keep-toolchain
-test -d .lake/packages/doc-gen4
-$LAKE -f require.toml resolve-deps  # validate manifest
+echo "# TEST: Resvoir require (TOML)"
+test_run -f require.toml update -v --keep-toolchain
+test_exp -d .lake/packages/doc-gen4
+test_run -f require.toml resolve-deps  # validate manifest
+
+# cleanup
+rm -f produced.out
--- a/src/lake/tests/order/clean.sh
+++ b/src/lake/tests/order/clean.sh
@ -1,3 +1,4 @@
+rm -f produced.out
 rm -rf .lake foo/.lake bar/.lake baz/.lake leaf/.lake
 rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json baz/lake-manifest.json leaf/lake-manifest.json
 rm -f lake-manifest-1.json
--- a/src/lake/tests/order/test.sh
+++ b/src/lake/tests/order/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -10,25 +8,28 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Later packages and libraries in the dependency tree shadow earlier ones.
 # https://github.com/leanprover/lean4/issues/2548

-$LAKE update -v
-$LAKE build +A -v | grep --color 222000
-$LAKE build +A.B -v | grep --color 333000
-$LAKE build +A.B.C -v | grep --color 333000
-$LAKE build +X -v | grep --color 888000 # bar
-$LAKE build +Y -v | grep --color 666000 # order
-$LAKE build +Z -v | grep --color 666000 # leaf from order
-$LAKE exe Y | grep --color root
+test_run update -v
+test_out 222000 -v build +A
+test_out 333000 -v build +A.B
+test_out 333000 -v build +A.B.C
+test_out 888000 -v build +X # bar
+test_out 666000 -v build +Y # order
+test_out 666000 -v build +Z # leaf from order
+test_out root exe Y

 # Tests that `lake update` does not reorder packages in the manifest
 # (if there have been no changes to the order in the configuration)
 # https://github.com/leanprover/lean4/issues/2664

-cp lake-manifest.json lake-manifest-1.json
-$LAKE update foo
-diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+test_cmd cp lake-manifest.json lake-manifest-1.json
+test_run update foo
+test_cmd diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json

 # Tests that order does not change in the presence of dep manifests
-$LAKE -d foo update
-$LAKE -d bar update
-$LAKE update
-diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+test_run -d foo update
+test_run -d bar update
+test_run update
+test_cmd diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/packageOverrides/clean.sh
+++ b/src/lake/tests/packageOverrides/clean.sh
@ -1,2 +1,2 @@
 rm -rf bar1/.git bar2/.lake .lake
-rm -f lake-manifest.json
+rm -f lake-manifest.json produced.out
--- a/src/lake/tests/packageOverrides/test.sh
+++ b/src/lake/tests/packageOverrides/test.sh
@ -1,12 +1,12 @@
 #!/usr/bin/env bash
-set -exo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the `bar1` repository on each test.
+echo "# SETUP"
+set -x
 pushd bar1
 git init
 git checkout -b master
@ -15,18 +15,30 @@ git config user.email test@example.com
 git add --all
 git commit -m "initial commit"
 popd
+set +x

-$LAKE resolve-deps -R
-$LAKE exe bar | grep --color "bar1"
+# Test the functionality of package overrides

-$LAKE resolve-deps -R -Kfoo --packages=packages.json
-$LAKE --packages=packages.json exe bar  | grep --color "bar2"
-$LAKE --packages=packages.json exe foo  | grep --color "foo"
+echo "# Tests"

-$LAKE resolve-deps -R
-$LAKE exe bar | grep --color "bar1"
+# Test dependency resolution without overrides
+test_run resolve-deps -R
+test_out "bar1" exe bar

-cp packages.json .lake/package-overrides.json
-$LAKE resolve-deps -R -Kfoo
-$LAKE exe bar | grep --color "bar2"
-$LAKE exe foo | grep --color "foo"
+# Test the `--packages` option
+test_run resolve-deps -R -Kfoo --packages=packages.json
+test_out "bar2" --packages=packages.json exe bar
+test_out "foo" --packages=packages.json exe foo
+
+# Test overrides are properly removed when reconfigured
+test_run resolve-deps -R
+test_out "bar1" exe bar
+
+# Test the use of `.lake/package-overrides.json`
+test_cmd cp packages.json .lake/package-overrides.json
+test_run resolve-deps -R -Kfoo
+test_out "bar2" exe bar
+test_out "foo" exe foo
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/postUpdate/clean.sh
+++ b/src/lake/tests/postUpdate/clean.sh
@ -1,2 +1,3 @@
 rm -rf dep/.lake dep/toolchain dep/lake-manifest.json
 rm -rf .lake lake-manifest.json toolchain
+rm -f produced.out
--- a/src/lake/tests/postUpdate/test.sh
+++ b/src/lake/tests/postUpdate/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -11,6 +9,8 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}

 echo "root" > toolchain
 echo "dep" > dep/toolchain
-$LAKE update | grep --color -F "post-update hello w/ arguments: [get]"
-test "`cat toolchain`" = dep
+test_out "post-update hello w/ arguments: [get]" update
+test_exp "`cat toolchain`" = dep

+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/precompileLink/test.sh
+++ b/src/lake/tests/precompileLink/test.sh
@ -21,7 +21,7 @@ test_maybe_err "-lBogus" build -KlinkArgs=-lBogus
 test_run build -R
 echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
 test_err "Building Foo" build --rehash
-rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+test_cmd rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
 test_run build -R -KplatformIndependent=true
 echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
 test_run build --rehash --no-build
--- a/src/lake/tests/query/clean.sh
+++ b/src/lake/tests/query/clean.sh
@ -1,2 +1 @@
-rm -rf .lake
-rm -f lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/query/test.sh
+++ b/src/lake/tests/query/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -9,19 +7,24 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Test the behavior of `lake query`
 # ---

-# Check that logs are not written to stdout
-$LAKE query | diff - /dev/null
+echo "# COMMON TESTS"

 # Test failure to build a query-only target
-($LAKE build +A:imports 2>&1 && exit 1 || true) | grep --color "not a build target"
+test_err "not a build target" build +A:imports

 # Test querying a custom target
-test "`$LAKE query foo`" = foo
-test "`$LAKE query foo --json`" = '"foo"'
+test_eq "foo" query foo
+test_eq '"foo"' query foo --json

 # Test querying imports
-test "`$LAKE query +A:imports`" = B
-test "`$LAKE query +A:transImports --json`" = '["C","B"]'
+test_eq "B" query +A:imports
+test_eq '["C","B"]' query +A:transImports --json
+
+echo "# UNCOMMON TESTS"
+set -x
+
+# Check that logs are not written to stdout
+$LAKE query | diff - /dev/null

 # Test querying library modules
 $LAKE query lib:modules | sort | diff -u --strip-trailing-cr <(cat << 'EOF'
@ -38,3 +41,8 @@ EOF
 # Test querying multiple targets
 test `$LAKE query foo foo | wc -l` = 2
 test `$LAKE query a b | wc -l` = 2
+
+set +x
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/rebuild/clean.sh
+++ b/src/lake/tests/rebuild/clean.sh
@ -1,2 +1,2 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
 rm -rf Foo Foo.lean
--- a/src/lake/tests/rebuild/test.sh
+++ b/src/lake/tests/rebuild/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -11,13 +9,16 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # 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

-mkdir -p Foo
+test_cmd mkdir -p Foo
 echo $'def a := "a"' > Foo/Test.lean
 echo $'import Foo.Test def hello := a' > Foo.lean
-${LAKE} build
-./.lake/build/bin/foo | grep --color a
+test_run build
+test_cmd_eq "Hello, a!" ./.lake/build/bin/foo
 echo $'def b := "b"' > Foo/Test.lean
 echo $'import Foo.Test def hello := b' > Foo.lean
-${LAKE} build Foo
-${LAKE} build
-./.lake/build/bin/foo | grep --color b
+test_run build Foo
+test_run build
+test_cmd_eq "Hello, b!" ./.lake/build/bin/foo
+
+# Cleanuo
+rm -f produced.out
--- a/src/lake/tests/reservoirConfig/clean.sh
+++ b/src/lake/tests/reservoirConfig/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json .git
+rm -rf .lake lake-manifest.json .git produced.out
--- a/src/lake/tests/reservoirConfig/test.sh
+++ b/src/lake/tests/reservoirConfig/test.sh
@ -1,10 +1,12 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the repository on each test.
+echo "# SETUP"
+set -x
 git init
 git checkout -b master
 git config user.name test
@ -16,8 +18,12 @@ git commit --allow-empty -m "commit 2"
 git tag v2
 git commit --allow-empty -m "commit 3"
 git tag etc
+set +x

-$LAKE reservoir-config | diff -u --strip-trailing-cr expected.json -
+# Test that Lake produces the expected Reservoir configuration.
+echo "# TEST"
+test_out_diff expected.json reservoir-config

-# Cleanup git repo
+# Cleanup
 rm -rf .git
+rm -f produced.out
--- a/src/lake/tests/reversion/clean.sh
+++ b/src/lake/tests/reversion/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json Hello.lean
+rm -rf .lake lake-manifest.json Hello.lean produced.out
--- a/src/lake/tests/reversion/test.sh
+++ b/src/lake/tests/reversion/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -10,11 +8,14 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}

 # Initial state
 echo 'def hello := "foo"' > Hello.lean
-$LAKE -q build
+test_run -q build
 # Introduce error
 echo 'error' > Hello.lean
-$LAKE build && exit 1 || true
+test_fails build
 # Revert
 echo 'def hello := "foo"' > Hello.lean
 # Ensure error is not presevered but the warning in another file is
-$LAKE -q build | grep --color 'Replayed Main'
+test_out "Replayed Main" -q build
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/serve/test.sh
+++ b/src/lake/tests/serve/test.sh
@ -1,14 +1,5 @@
 #!/usr/bin/env bash
-set -euo pipefail
-
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  TAIL=gtail
-else
-  TAIL=tail
-fi
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source  ../common.sh

 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"}'
@ -24,19 +15,23 @@ echo "does not compile" > lakefile.lean
 # See https://github.com/leanprover/lake/issues/49
 # ---

+echo "# TEST 49"
 MSGS="$INIT_REQ$INITD_NOT$SD_REQ$EXIT_NOT"
-echo -n "$MSGS" | ${LAKE:-../../.lake/build/bin/lake} serve > serve.log
-echo "tested 49"
+echo -n "$MSGS" | $LAKE serve > serve.log
+echo "Test passed"

 # ---
 # Test that `lake setup-file` retains the error from `lake serve`
 # See https://github.com/leanprover/lake/issues/116
 # ---

+echo "# TEST 116"
+
 # Test that `lake setup-file` produces the error from `LAKE_INVALID_CONFIG`
 (LAKE_INVALID_CONFIG=$'foo\n' $LAKE setup-file ./Irrelevant.lean 2>&1 && exit 1 || true) | grep --color foo

 # Test that `lake serve` produces the `Failed to configure` message.
 MSGS="$INIT_REQ$INITD_NOT$OPEN_REQ"
 grep -q "Failed to configure the Lake workspace" <(set +e; (echo -n "$MSGS" && $TAIL --pid=$$ -f /dev/null) | timeout 30s $LAKE serve | tee serve.log)
-echo "tested 116"
+
+echo "Test passed"
--- a/src/lake/tests/setupFile/clean.sh
+++ b/src/lake/tests/setupFile/clean.sh
@ -1 +1 @@
-rm -f lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/setupFile/test.sh
+++ b/src/lake/tests/setupFile/test.sh
@ -26,3 +26,6 @@ test_run -f invalid.lean setup-file invalid.lean Lake
 # Test that `setup-file` on a configuration file uses the Lake plugin,
 # even if the file is invalid and/or is not using a `Lake` import.
 test_not_out '"pluginPaths":[]' -f invalid.lean setup-file invalid.lean
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/toml/test.sh
+++ b/src/lake/tests/toml/test.sh
@ -1,5 +1,3 @@
 #!/usr/bin/env bash
-set -euo pipefail
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-$LAKE -d ../.. build Lake.Toml
-$LAKE env lean --run Test.lean
+source ../common.sh
+test_run env lean --run Test.lean
--- a/src/lake/tests/toolchain/test.sh
+++ b/src/lake/tests/toolchain/test.sh
@ -1,30 +1,36 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../../.lake/build/bin/lake}
+source ../common.sh

 # Tests which require Elan to download a toolchain

+ELAN=${ELAN:-elan}
+
 # skip if no elan found
-if ! command -v elan > /dev/null; then
+echo "# Check if elan exists"
+if ! command -v $ELAN > /dev/null; then
   echo "elan not found; skipping test"
   exit 0
 fi

+# Ensure runtime libraries of different Leans are not overridden
+export LD_LIBRARY_PATH=
+
+echo "# TESTS"
+
 # Test that Lake rebuilds when toolchain changes
 # See https://github.com/leanprover/lake/issues/62

 TOOLCHAIN=leanprover/lean4:v4.0.0
 ./clean.sh
-elan run --install $TOOLCHAIN lake new foo
+test_cmd $ELAN run --install $TOOLCHAIN lake new foo
 pushd foo
-elan run $TOOLCHAIN lake build +Foo:olean -v | grep --color Foo.olean
-rm lean-toolchain # switch to Lake under test
-$LAKE build -v | grep --color Foo.olean
+test_cmd_out "Foo.olean" $ELAN run $TOOLCHAIN lake build +Foo:olean -v
+test_cmd rm lean-toolchain # switch to Lake under test
+test_out "Foo.olean" build -v
 popd

 # Test Lake runs under the new toolchain after Lake updates it
 rm -f foo/lake-manifest.json
 echo $TOOLCHAIN > foo/lean-toolchain
-$LAKE update
-grep --color -F '"version": 5' lake-manifest.json
+test_run update
+test_cmd grep --color -F '"version": 5' lake-manifest.json
--- a/src/lake/tests/trace/clean.sh
+++ b/src/lake/tests/trace/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/trace/test.sh
+++ b/src/lake/tests/trace/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

@ -10,26 +8,29 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # ---

 # Tests that a build produces a trace
-test ! -f .lake/build/lib/lean/Foo.trace
-$LAKE build | grep --color "Built Foo"
-test -f .lake/build/lib/lean/Foo.trace
+test_exp ! -f .lake/build/lib/lean/Foo.trace
+test_out "Built Foo" build
+test_exp -f .lake/build/lib/lean/Foo.trace

 # Tests that a proper trace prevents a rebuild
-$LAKE build --no-build
+test_run build --no-build

 # Tests that Lake accepts pure numerical traces
 if command -v jq > /dev/null; then # skip if no jq found
  jq -r '.depHash' .lake/build/lib/lean/Foo.trace > .lake/build/lib/lean/Foo.trace.hash
-  mv .lake/build/lib/lean/Foo.trace.hash .lake/build/lib/lean/Foo.trace
-  $LAKE build --no-build
+  test_cmd mv .lake/build/lib/lean/Foo.trace.hash .lake/build/lib/lean/Foo.trace
+  test_run build --no-build
 fi

 # Tests that removal of the trace does not cause a rebuild
 # (if the modification time of the artifact is still newer than the inputs)
-rm .lake/build/lib/lean/Foo.trace
-$LAKE build --no-build
+test_cmd rm .lake/build/lib/lean/Foo.trace
+test_run build --no-build

 # Tests that an invalid trace does cause a rebuild
-touch .lake/build/lib/lean/Foo.trace
-$LAKE build | grep --color "Built Foo"
-$LAKE build --no-build
+test_cmd touch .lake/build/lib/lean/Foo.trace
+test_out "Built Foo" build
+test_run build --no-build
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/translateConfig/clean.sh
+++ b/src/lake/tests/translateConfig/clean.sh
@ -1,3 +1,4 @@
 rm -rf .lake
+rm -f produced.out
 rm -f *.produced.*
 rm -f lakefile.*
--- a/src/lake/tests/translateConfig/test.sh
+++ b/src/lake/tests/translateConfig/test.sh
@ -1,40 +1,41 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 ./clean.sh

 # Test Lean to TOML translation
-$LAKE translate-config -f source.lean toml out.produced.toml 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.expected.toml out.produced.toml
-rm out.produced.toml
+test_no_out translate-config -f source.lean toml out.produced.toml
+test_cmd diff --strip-trailing-cr out.expected.toml out.produced.toml
+test_cmd rm out.produced.toml

 # Test idempotency of TOML translation
-$LAKE translate-config -f out.expected.toml toml out.produced.toml 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.expected.toml out.produced.toml
+test_no_out translate-config -f out.expected.toml toml out.produced.toml
+test_cmd diff --strip-trailing-cr out.expected.toml out.produced.toml

 # Test TOML to Lean translation
-$LAKE translate-config -f source.toml lean out.produced.lean 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.expected.lean out.produced.lean
-rm out.produced.lean
+test_no_out translate-config -f source.toml lean out.produced.lean
+test_cmd diff --strip-trailing-cr out.expected.lean out.produced.lean
+test_cmd rm out.produced.lean

 # Test idempotency of Lean translation
-$LAKE translate-config -f out.expected.lean lean out.produced.lean 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.expected.lean out.produced.lean
+test_no_out translate-config -f out.expected.lean lean out.produced.lean
+test_cmd diff --strip-trailing-cr out.expected.lean out.produced.lean

 # Test produced TOML round-trips
-$LAKE translate-config -f out.produced.toml lean bridge.produced.lean 2>&1 | diff - /dev/null
-$LAKE translate-config -f bridge.produced.lean toml roundtrip.produced.toml 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.produced.toml roundtrip.produced.toml
+test_no_out translate-config -f out.produced.toml lean bridge.produced.lean
+test_no_out translate-config -f bridge.produced.lean toml roundtrip.produced.toml
+test_cmd diff --strip-trailing-cr out.produced.toml roundtrip.produced.toml

 # Test produced Lean round-trips
-$LAKE translate-config -f out.produced.lean toml bridge.produced.toml 2>&1 | diff - /dev/null
-$LAKE translate-config -f bridge.produced.toml lean roundtrip.produced.lean 2>&1 | diff - /dev/null
-diff --strip-trailing-cr out.produced.lean roundtrip.produced.lean
+test_no_out translate-config -f out.produced.lean toml bridge.produced.toml
+test_no_out translate-config -f bridge.produced.toml lean roundtrip.produced.lean
+test_cmd diff --strip-trailing-cr out.produced.lean roundtrip.produced.lean

 # Test source rename
-cp source.lean lakefile.lean
-$LAKE translate-config toml | diff - /dev/null
-test -f lakefile.lean.bak
-test -f lakefile.toml
+test_cmd cp source.lean lakefile.lean
+test_no_out translate-config toml
+test_exp -f lakefile.lean.bak
+test_exp -f lakefile.toml
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/updateToolchain/clean.sh
+++ b/src/lake/tests/updateToolchain/clean.sh
@ -1 +1 @@
-rm -f lean-toolchain a/lean-toolchain b/lean-toolchain
+rm -f produced.out lean-toolchain a/lean-toolchain b/lean-toolchain
--- a/src/lake/tests/updateToolchain/test.sh
+++ b/src/lake/tests/updateToolchain/test.sh
@ -1,7 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh

 # Ensure Lake thinks there is a elan environment configured
 export ELAN_HOME=
@ -11,16 +9,16 @@ export ELAN_HOME=
 RESTART_CODE=4

 test_update(){
-   ELAN=true $LAKE update 2>&1 | grep --color "updating toolchain to '$1'"
+   ELAN=true test_out "updating toolchain to '$1'" update
   cat lean-toolchain | diff - <(echo -n "$1")
 }

 # Test toolchain version API
-$LAKE lean test.lean
+test_run lean test.lean

 # Test no toolchain information
 ./clean.sh
-$LAKE update 2>&1 | grep --color "toolchain not updated; no toolchain information found"
+test_out "toolchain not updated; no toolchain information found" update

 # Test a single unknown candidate
 ./clean.sh
@ -49,20 +47,23 @@ test_update leanprover/lean4:nightly-2024-10-01
 echo v4.4.0 > a/lean-toolchain
 echo v4.8.0 > b/lean-toolchain
 echo v4.10.0 > lean-toolchain
-$LAKE update 2>&1 | grep --color "toolchain not updated; already up-to-date"
+test_out "toolchain not updated; already up-to-date" update

 # Test multiple candidates
 ./clean.sh
 echo lean-a > a/lean-toolchain
 echo lean-b > b/lean-toolchain
-$LAKE update 2>&1 | grep --color "toolchain not updated; multiple toolchain candidates"
+test_out "toolchain not updated; multiple toolchain candidates" update

 # Test manual restart
 ./clean.sh
 echo lean-a > a/lean-toolchain
-ELAN= $LAKE update 2>&1 && exit 1 || [ $? = $RESTART_CODE ]
+ELAN= test_status $RESTART_CODE update

 # Test elan restart
 ./clean.sh
 echo lean-a > a/lean-toolchain
-ELAN=echo $LAKE update | grep --color "run --install lean-a lake update"
+ELAN=echo test_out "run --install lean-a lake update" update
+
+# Cleanup
+rm -f produced.out
--- a/src/lake/tests/versionTags/clean.sh
+++ b/src/lake/tests/versionTags/clean.sh
@ -1 +1 @@
-rm -rf .lake lake-manifest.json .git
+rm -rf .lake lake-manifest.json .git produced.out
--- a/src/lake/tests/versionTags/test.sh
+++ b/src/lake/tests/versionTags/test.sh
@ -1,27 +1,35 @@
 #!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
-./clean.sh
+source ../common.sh
+source ./clean.sh

+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the repository on each test.
+echo "# SETUP"
+set -x
 git init
 git checkout -b master
 git config user.name test
 git config user.email test@example.com
 git add --all
-git commit -m "commit 1"
+git commit -m "commit v1"
 git tag v1
-git commit --allow-empty -m "commit 2"
+git commit --allow-empty -m "commit v2"
 git tag v2
-git commit --allow-empty -m "commit 3"
+git commit --allow-empty -m "commit venom"
+git tag venom
+git commit --allow-empty -m "commit etc"
 git tag etc
+set +x

-$LAKE version-tags | diff -u --strip-trailing-cr <(cat << 'EOF'
+# Test thae Lake returns the version-like tags
+# (i.e., those matching `v[0-9].*`)
+echo "# TEST"
+test_out_diff <(cat << 'EOF'
 v1
 v2
 EOF
-) -
+) version-tags

-# Cleanup git repo
+# Cleanup
+rm -f produced.out
 rm -rf .git