590ff23e71
This PR fixes a bug where Lake ignored `moreLinkObjs` and `moreLinkLibs` on a `lean_exe`.
22 lines
661 B
Bash
Executable file
22 lines
661 B
Bash
Executable file
#!/usr/bin/env bash
|
|
set -euxo pipefail
|
|
|
|
LAKE=${LAKE:-../../.lake/build/bin/lake}
|
|
|
|
./clean.sh
|
|
|
|
$LAKE -d app build -v
|
|
$LAKE -d lib build -v
|
|
|
|
$LAKE exe -d app app
|
|
$LAKE exe -d lib test
|
|
$LAKE exe -d lib standalone
|
|
|
|
# Tests that a non-precompiled build does not load anything as a dynlib/plugin
|
|
# https://github.com/leanprover/lean4/issues/4565
|
|
$LAKE -d app build -v | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
|
|
$LAKE -d lib build -v | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
|
|
|
|
# Tests the successful precompilation of an FFI library
|
|
# Also tests a module with `precompileModules` always precompiles its imports
|
|
$LAKE -d app build Test
|