lean4-htt/tests/lake/examples/hello/test.sh
Mac Malone aa3d409eb6
refactor: lake: mv tests/examples to top-level tests dir (#10688)
This PR moves Lake's test infrastructure from `src/lake` to
`tests/lake`.
2025-10-06 21:47:57 +00:00

33 lines
826 B
Bash
Executable file

#!/usr/bin/env bash
set -euxo pipefail
LAKE=${LAKE:-../../.lake/build/bin/lake}
./clean.sh
$LAKE exe hello
$LAKE exe hello Bob Bill
.lake/build/bin/hello
# Tests that quiet mode (-q) produces no output on no-op build
$LAKE -q build hello 2>&1 | diff - /dev/null
# Tests that build produces a manifest if there is none.
# Related: https://github.com/leanprover/lean4/issues/2549
test -f lake-manifest.json
# Test pack/unpack
$LAKE pack .lake/build.tgz 2>&1 | grep --color "packing"
rm -rf .lake/build
$LAKE unpack .lake/build.tgz 2>&1 | grep --color "unpacking"
.lake/build/bin/hello
$LAKE pack 2>&1 | grep --color "packing"
rm -rf .lake/build
$LAKE unpack 2>&1 | grep --color "unpacking"
.lake/build/bin/hello
./clean.sh
$LAKE -f lakefile.toml exe hello
$LAKE -f lakefile.toml exe hello Bob Bill
.lake/build/bin/hello