diff --git a/src/lake/tests/badImport/clean.sh b/src/lake/tests/badImport/clean.sh index 9075fbd55d..6daefb0011 100755 --- a/src/lake/tests/badImport/clean.sh +++ b/src/lake/tests/badImport/clean.sh @@ -1 +1 @@ -rm -rf .lake lake-manifest.json Lib/Bogus.lean +rm -rf .lake lake-manifest.json Lib/Bogus.lean produced.out diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh index 1ce603e023..363d04f678 100755 --- a/src/lake/tests/badImport/test.sh +++ b/src/lake/tests/badImport/test.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -set -euxo pipefail +set -euo pipefail LAKE=${LAKE:-../../.lake/build/bin/lake} @@ -12,29 +12,65 @@ LAKE=${LAKE:-../../.lake/build/bin/lake} # https://github.com/leanprover/lean4/issues/3351 # https://github.com/leanprover/lean4/issues/3809 +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 +} + +test_err() { + expected=$1; shift + if test_run "$@"; then rc=$?; else rc=$?; fi + echo "[Match \"$expected\"]" + if grep --color -F "$expected" produced.out; then + if [ $rc != 1 ]; then + echo "[Outcome]" + echo "Lake unexpectedly succeeded." + return 1 + fi + else + echo "No match found." + return 1 + fi +} + # Test a module with a bad import does not kill the whole build -($LAKE build Lib.U Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc" -# Test importing a nmissing module from outside the workspace -($LAKE build +Lib.U 2>&1 && exit 1 || true) | grep --color -F "U.lean:2:0: unknown module prefix 'Bogus'" -$LAKE setup-file . Bogus # Lake ignores the file (the server will error) +test_err "Building Etc" build Lib.U Etc +# Test importing a missing module from outside the workspace +test_err "U.lean:2:0: unknown module prefix 'Bogus'" build +Lib.U +test_run setup-file . Bogus # Lake ignores the file (the server will error) # Test importing onself -($LAKE build +Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself" -($LAKE setup-file ./Lib/S.lean Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself" +test_err "S.lean: module imports itself" build +Lib.S +test_err "S.lean: module imports itself" setup-file ./Lib/S.lean Lib.S # Test importing a missing module from within the workspace -($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'" -($LAKE setup-file ./Lib/B.lean Lib.Bogus 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'" +test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B +test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean Lib.Bogus # 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 -($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'" -($LAKE setup-file . Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'" +set +x +test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B +test_err "B.lean: bad import 'Lib.Bogus'" setup-file . Lib.B # Test a module which imports a module containing a bad import -($LAKE build +Lib.B1 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'" -($LAKE setup-file ./Lib/B1.lean Lib.B 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'" +test_err "B1.lean: bad import 'Lib.B'" build +Lib.B1 +test_err "B1.lean: bad import 'Lib.B'" setup-file ./Lib/B1.lean Lib.B # Test an executable with a bad import does not kill the whole build -($LAKE build X Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc" +test_err "Building Etc" build X Etc # Test an executable which imports a missing module from within the workspace -($LAKE build X 2>&1 && exit 1 || true) | grep --color -F "X.lean: bad import 'Lib.Bogus'" -# Test a executable which imports a module containing a bad import -($LAKE build X1 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'" +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 +rm -f produced.out diff --git a/src/lake/tests/buildArgs/test.sh b/src/lake/tests/buildArgs/test.sh index 53776ee767..4a6799c946 100755 --- a/src/lake/tests/buildArgs/test.sh +++ b/src/lake/tests/buildArgs/test.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -set -exo pipefail +set -euo pipefail LAKE=${LAKE:-../../.lake/build/bin/lake} @@ -8,32 +8,61 @@ LAKE=${LAKE:-../../.lake/build/bin/lake} # Test that changing `moreLean/Leanc/LinkArgs` triggers a rebuild # Test that changing `weakLean/Leanc/LinkArgs` does not +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 +} + +test_out() { + expected=$1; shift + if test_run "$@"; then rc=$?; else rc=$?; fi + echo "[Match \"$expected\"]" + if grep --color -F "$expected" produced.out; then + return $rc + else + echo "No match found." + return 1 + fi +} + # Test `leanArgs` -${LAKE} build +Hello -R +test_run build +Hello -R # see https://github.com/leanprover/lake/issues/50 -${LAKE} build +Hello -R -KleanArgs=-DwarningAsError=true -v | grep --color warningAsError +test_out "warningAsError" build +Hello -R -KleanArgs=-DwarningAsError=true -v # Test `weakLeanArgs` -${LAKE} build +Hello -R +test_run build +Hello -R # see https://github.com/leanprover/lake/issues/172 -${LAKE} build +Hello -R -KweakLeanArgs=-DwarningAsError=true --no-build +test_run build +Hello -R -KweakLeanArgs=-DwarningAsError=true --no-build # Test `leancArgs` -${LAKE} build +Hello:o -R -${LAKE} build +Hello:o -R -KleancArgs=-DBAR -v | grep --color "Built Hello:c.o" +test_run build +Hello:o -R +test_out "Built Hello:c.o" build +Hello:o -R -KleancArgs=-DBAR -v # Test `weakLeancArgs` -${LAKE} build +Hello:o -R -${LAKE} build +Hello:o -R -KweakLeancArgs=-DBAR --no-build +test_run build +Hello:o -R +test_run build +Hello:o -R -KweakLeancArgs=-DBAR --no-build # Test `linkArgs` -${LAKE} build +Hello:dynlib Hello:shared hello -R -${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built Hello:dynlib" -${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built Hello:shared" -${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built hello" +test_run build +Hello:dynlib Hello:shared hello -R +test_out "Built Hello:dynlib" build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib -v +test_out "Built Hello:shared" build Hello:shared -R -KlinkArgs=-L.lake/build/lib -v +test_out "Built hello" build hello -R -KlinkArgs=-L.lake/build/lib -v # Test `weakLinkArgs` -${LAKE} build +Hello:dynlib Hello:shared hello -R -${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib --no-build -${LAKE} build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib --no-build -${LAKE} build hello -R -KweakLinkArgs=-L.lake/build/lib --no-build +test_run build +Hello:dynlib Hello:shared hello -R +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 +rm -f produced.out