From 05153d66b1b2ab33b724203cbbc87bc2d7ca0f3f Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 30 Apr 2025 21:20:50 -0400 Subject: [PATCH] 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. --- src/lake/Lake/Build/Package.lean | 4 +- src/lake/Lake/CLI/Build.lean | 6 +- src/lake/Makefile | 2 +- src/lake/tests/api/keys.lean | 26 +-- src/lake/tests/api/test.sh | 6 +- src/lake/tests/badImport/test.sh | 12 +- src/lake/tests/buildArgs/test.sh | 2 +- src/lake/tests/clone/clean.sh | 1 + src/lake/tests/clone/test.sh | 49 ++-- src/lake/tests/common.sh | 280 ++++++++++++++++++++--- src/lake/tests/depTree/test.sh | 12 +- src/lake/tests/driver/clean.sh | 2 +- src/lake/tests/driver/test.sh | 149 ++++++------ src/lake/tests/env/clean.sh | 1 + src/lake/tests/env/test.sh | 58 +++-- src/lake/tests/externLib/test.sh | 4 +- src/lake/tests/globs/test.sh | 32 ++- src/lake/tests/init/clean.sh | 1 + src/lake/tests/init/test.sh | 128 ++++++----- src/lake/tests/inputFile/clean.sh | 2 +- src/lake/tests/inputFile/test.sh | 66 +++--- src/lake/tests/kinds/test.sh | 23 +- src/lake/tests/lean/clean.sh | 2 +- src/lake/tests/lean/test.sh | 8 +- src/lake/tests/llvm-bitcode-gen/clean.sh | 2 +- src/lake/tests/llvm-bitcode-gen/test.sh | 20 +- src/lake/tests/logLevel/clean.sh | 2 +- src/lake/tests/logLevel/test.sh | 32 ++- src/lake/tests/manifest/clean.sh | 2 +- src/lake/tests/manifest/test.sh | 25 +- src/lake/tests/meta/clean.sh | 2 +- src/lake/tests/meta/test.sh | 27 ++- src/lake/tests/noBuild/clean.sh | 2 +- src/lake/tests/noBuild/test.sh | 20 +- src/lake/tests/noRelease/clean.sh | 2 +- src/lake/tests/noRelease/test.sh | 62 ++--- src/lake/tests/online/clean.sh | 2 +- src/lake/tests/online/test.sh | 88 +++---- src/lake/tests/order/clean.sh | 1 + src/lake/tests/order/test.sh | 37 +-- src/lake/tests/packageOverrides/clean.sh | 2 +- src/lake/tests/packageOverrides/test.sh | 40 ++-- src/lake/tests/postUpdate/clean.sh | 1 + src/lake/tests/postUpdate/test.sh | 10 +- src/lake/tests/precompileLink/test.sh | 2 +- src/lake/tests/query/clean.sh | 3 +- src/lake/tests/query/test.sh | 28 ++- src/lake/tests/rebuild/clean.sh | 2 +- src/lake/tests/rebuild/test.sh | 19 +- src/lake/tests/reservoirConfig/clean.sh | 2 +- src/lake/tests/reservoirConfig/test.sh | 16 +- src/lake/tests/reversion/clean.sh | 2 +- src/lake/tests/reversion/test.sh | 13 +- src/lake/tests/serve/test.sh | 21 +- src/lake/tests/setupFile/clean.sh | 2 +- src/lake/tests/setupFile/test.sh | 3 + src/lake/tests/toml/test.sh | 6 +- src/lake/tests/toolchain/test.sh | 26 ++- src/lake/tests/trace/clean.sh | 2 +- src/lake/tests/trace/test.sh | 29 +-- src/lake/tests/translateConfig/clean.sh | 1 + src/lake/tests/translateConfig/test.sh | 47 ++-- src/lake/tests/updateToolchain/clean.sh | 2 +- src/lake/tests/updateToolchain/test.sh | 21 +- src/lake/tests/versionTags/clean.sh | 2 +- src/lake/tests/versionTags/test.sh | 30 ++- 66 files changed, 917 insertions(+), 617 deletions(-) create mode 100755 src/lake/tests/env/clean.sh diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 8ec4540d45..3ca2af008d 100644 --- 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 diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean index 838a0bc015..812be001c8 100644 --- 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 diff --git a/src/lake/Makefile b/src/lake/Makefile index fb6a2268b9..5658162cff 100644 --- 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 diff --git a/src/lake/tests/api/keys.lean b/src/lake/tests/api/keys.lean index 32d84bcd61..66148faec6 100644 --- 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] diff --git a/src/lake/tests/api/test.sh b/src/lake/tests/api/test.sh index 66784be855..e56d7ccfa0 100755 --- 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 diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh index 87c6dddfbc..a9fb4cd6ad 100755 --- 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 diff --git a/src/lake/tests/buildArgs/test.sh b/src/lake/tests/buildArgs/test.sh index 7bb497bc0f..548753b997 100755 --- 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 diff --git a/src/lake/tests/clone/clean.sh b/src/lake/tests/clone/clean.sh index 045cf8cdec..379bb56772 100755 --- 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 diff --git a/src/lake/tests/clone/test.sh b/src/lake/tests/clone/test.sh index 9b2a67bc08..cf4a144a00 100755 --- 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 diff --git a/src/lake/tests/common.sh b/src/lake/tests/common.sh index 4f526b3f06..b7ba1ab1fc 100644 --- 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 +} diff --git a/src/lake/tests/depTree/test.sh b/src/lake/tests/depTree/test.sh index a5379ec021..9a1faf6ca3 100755 --- 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 diff --git a/src/lake/tests/driver/clean.sh b/src/lake/tests/driver/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/driver/test.sh b/src/lake/tests/driver/test.sh index 53fe00f813..046172be07 100755 --- 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 diff --git a/src/lake/tests/env/clean.sh b/src/lake/tests/env/clean.sh new file mode 100755 index 0000000000..6014e830c3 --- /dev/null +++ b/src/lake/tests/env/clean.sh @@ -0,0 +1 @@ +rm -f produced.out diff --git a/src/lake/tests/env/test.sh b/src/lake/tests/env/test.sh index e26720e55e..9c176498e0 100755 --- 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 diff --git a/src/lake/tests/externLib/test.sh b/src/lake/tests/externLib/test.sh index 6786844fec..8915268d97 100755 --- 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 diff --git a/src/lake/tests/globs/test.sh b/src/lake/tests/globs/test.sh index 655ef921c9..eea4b8c46d 100755 --- 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 diff --git a/src/lake/tests/init/clean.sh b/src/lake/tests/init/clean.sh index 58b771ac39..307da07414 100755 --- 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 diff --git a/src/lake/tests/init/test.sh b/src/lake/tests/init/test.sh index df60da92b9..d8bb5951f8 100755 --- 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 " 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 diff --git a/src/lake/tests/inputFile/clean.sh b/src/lake/tests/inputFile/clean.sh index 2787f30c33..b8909efd7a 100755 --- 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 diff --git a/src/lake/tests/inputFile/test.sh b/src/lake/tests/inputFile/test.sh index ad05c51828..40faa3abe1 100755 --- 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 diff --git a/src/lake/tests/kinds/test.sh b/src/lake/tests/kinds/test.sh index 3da791ec01..4e0f27467a 100755 --- 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 diff --git a/src/lake/tests/lean/clean.sh b/src/lake/tests/lean/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/lean/test.sh b/src/lake/tests/lean/test.sh index 802f706089..d9dd890a20 100755 --- 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 diff --git a/src/lake/tests/llvm-bitcode-gen/clean.sh b/src/lake/tests/llvm-bitcode-gen/clean.sh index d88ee8e2bd..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/llvm-bitcode-gen/test.sh b/src/lake/tests/llvm-bitcode-gen/test.sh index 0dc18d308e..e5e3285106 100755 --- 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 diff --git a/src/lake/tests/logLevel/clean.sh b/src/lake/tests/logLevel/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/logLevel/test.sh b/src/lake/tests/logLevel/test.sh index c6f80ec66b..9e8e20dfae 100755 --- 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 diff --git a/src/lake/tests/manifest/clean.sh b/src/lake/tests/manifest/clean.sh index e22e74298b..aab3a685c0 100755 --- 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 diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh index 08d6855d63..cc987c922d 100755 --- 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 diff --git a/src/lake/tests/meta/clean.sh b/src/lake/tests/meta/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/meta/test.sh b/src/lake/tests/meta/test.sh index 45e76b4ba1..8a96f3670d 100755 --- 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 diff --git a/src/lake/tests/noBuild/clean.sh b/src/lake/tests/noBuild/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/noBuild/test.sh b/src/lake/tests/noBuild/test.sh index 4ac8cd6c9d..b6078076e4 100755 --- 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 diff --git a/src/lake/tests/noRelease/clean.sh b/src/lake/tests/noRelease/clean.sh index eb7d9f342e..5250a2fcb8 100755 --- 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 diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh index 002c7c3ac5..62ce32eb20 100755 --- 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 diff --git a/src/lake/tests/online/clean.sh b/src/lake/tests/online/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh index 5c0b11d936..3d495cf69e 100755 --- 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 diff --git a/src/lake/tests/order/clean.sh b/src/lake/tests/order/clean.sh index 3974b61a73..329547e8e6 100755 --- 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 diff --git a/src/lake/tests/order/test.sh b/src/lake/tests/order/test.sh index a627c3778b..e985562daa 100755 --- 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 diff --git a/src/lake/tests/packageOverrides/clean.sh b/src/lake/tests/packageOverrides/clean.sh index 74e99858fb..45d310b51f 100755 --- 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 diff --git a/src/lake/tests/packageOverrides/test.sh b/src/lake/tests/packageOverrides/test.sh index ce833f346b..6d336de871 100755 --- 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 diff --git a/src/lake/tests/postUpdate/clean.sh b/src/lake/tests/postUpdate/clean.sh index 3f0a6430e1..e39b19197d 100755 --- 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 diff --git a/src/lake/tests/postUpdate/test.sh b/src/lake/tests/postUpdate/test.sh index 451c7908af..eb426eb692 100755 --- 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 diff --git a/src/lake/tests/precompileLink/test.sh b/src/lake/tests/precompileLink/test.sh index 6c70d36c6d..ec3c986d48 100755 --- 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 diff --git a/src/lake/tests/query/clean.sh b/src/lake/tests/query/clean.sh index 2639d0cf53..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/query/test.sh b/src/lake/tests/query/test.sh index 2559c748d6..85085dd7ed 100755 --- 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 diff --git a/src/lake/tests/rebuild/clean.sh b/src/lake/tests/rebuild/clean.sh index c63c458159..119d42a2c4 100755 --- 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 diff --git a/src/lake/tests/rebuild/test.sh b/src/lake/tests/rebuild/test.sh index 6b4b8c0715..b9ec2bd7e2 100755 --- 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 diff --git a/src/lake/tests/reservoirConfig/clean.sh b/src/lake/tests/reservoirConfig/clean.sh index 8e49561ad8..8f39883ae3 100755 --- 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 diff --git a/src/lake/tests/reservoirConfig/test.sh b/src/lake/tests/reservoirConfig/test.sh index bf47fa04c4..31c4af6158 100755 --- 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 diff --git a/src/lake/tests/reversion/clean.sh b/src/lake/tests/reversion/clean.sh index b17e778db0..9f69457ad6 100755 --- 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 diff --git a/src/lake/tests/reversion/test.sh b/src/lake/tests/reversion/test.sh index d4e8d877d2..b4eafd0b3c 100755 --- 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 diff --git a/src/lake/tests/serve/test.sh b/src/lake/tests/serve/test.sh index f7cc45f9e2..03df518544 100755 --- 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" diff --git a/src/lake/tests/setupFile/clean.sh b/src/lake/tests/setupFile/clean.sh index 2f04571d69..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/setupFile/test.sh b/src/lake/tests/setupFile/test.sh index 480df6d9e5..1cf83c0110 100755 --- 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 diff --git a/src/lake/tests/toml/test.sh b/src/lake/tests/toml/test.sh index e37facb26a..35ecca13a5 100755 --- 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 diff --git a/src/lake/tests/toolchain/test.sh b/src/lake/tests/toolchain/test.sh index 16e86fe650..4225309355 100755 --- 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 diff --git a/src/lake/tests/trace/clean.sh b/src/lake/tests/trace/clean.sh index b6e54c681e..333b50aba2 100755 --- 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 diff --git a/src/lake/tests/trace/test.sh b/src/lake/tests/trace/test.sh index b94850f950..2e3d45808a 100755 --- 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 diff --git a/src/lake/tests/translateConfig/clean.sh b/src/lake/tests/translateConfig/clean.sh index 99f0127ded..a47a72c7be 100755 --- 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.* diff --git a/src/lake/tests/translateConfig/test.sh b/src/lake/tests/translateConfig/test.sh index 75cfd85c31..668d884f58 100755 --- 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 diff --git a/src/lake/tests/updateToolchain/clean.sh b/src/lake/tests/updateToolchain/clean.sh index 1ba7c542cc..a3d7f2537a 100755 --- 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 diff --git a/src/lake/tests/updateToolchain/test.sh b/src/lake/tests/updateToolchain/test.sh index 094ca86e25..aa688ea305 100755 --- 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 diff --git a/src/lake/tests/versionTags/clean.sh b/src/lake/tests/versionTags/clean.sh index 8e49561ad8..8f39883ae3 100755 --- 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 diff --git a/src/lake/tests/versionTags/test.sh b/src/lake/tests/versionTags/test.sh index b223f5dcd5..9e29463e54 100755 --- 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