chore: add test

src/lake/examples/precompile/test.sh

@@ -4,7 +4,9 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
 $LAKE -d bar update
-$LAKE -d bar build # tests lake#83
+# test that build a module w/o precompile modules still precompiles deps
+# https://github.com/leanprover/lake/issues/83
+$LAKE -d bar build
 $LAKE -d foo build
 
 ./clean.sh

src/lake/tests/precompileArgs/lakefile.lean

@@ -6,4 +6,5 @@ package precompileArgs
 @[default_target]
 lean_lib Foo where
   precompileModules := true
-  moreLinkArgs := #["-lBaz"]
+  platformIndependent := if get_config? platformIndependent |>.isSome then true else none
+  moreLinkArgs := if let some cfg := get_config? linkArgs then cfg.splitOn " " |>.toArray else #[]

src/lake/tests/precompileArgs/test.sh

@@ -3,7 +3,27 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
+if [ "$OS" = Windows_NT ]; then
+LIB_PREFIX=
+SHARED_LIB_EXT=dll
+elif [ "`uname`" = Darwin ]; then
+LIB_PREFIX=lib
+SHARED_LIB_EXT=dylib
+else
+LIB_PREFIX=lib
+SHARED_LIB_EXT=so
+fi
+
 ./clean.sh
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
-($LAKE build +Foo:dynlib 2>&1 || true) | grep --color -- "-lBaz"
+($LAKE build -KlinkArgs=-lBaz 2>&1 || true) | grep --color -- "-lBaz"
+
+# Test that dynlibs are part of the module trace unless `platformIndependent` is set
+$LAKE build -R
+echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+($LAKE build 2>&1 --rehash && exit 1 || true) | grep --color "Building Foo"
+rm .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+$LAKE build -R -KplatformIndependent=true
+echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+$LAKE build --rehash --no-build