chore: lake: make failing tests more verbose (#7666)
This PR makes the Lake tests that have intermittently failed more verbose in their output to hopefully help diagnose the issue.
This commit is contained in:
Mac Malone
GitHub
parent
748e8da728
commit
1465c23e12
3 changed files with 100 additions and 35 deletions
|
|
@ -1 +1 @@
|
|||
rm -rf .lake lake-manifest.json Lib/Bogus.lean
|
||||
rm -rf .lake lake-manifest.json Lib/Bogus.lean produced.out
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue