From f1d12562012c6c68262ac983ec2cc3fa088449f9 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 17 Jun 2024 17:03:39 -0400
Subject: [PATCH] chore: add test

---
 src/lake/examples/precompile/test.sh        |  4 +++-
 src/lake/tests/precompileArgs/lakefile.lean |  3 ++-
 src/lake/tests/precompileArgs/test.sh       | 22 ++++++++++++++++++++-
 3 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/lake/examples/precompile/test.sh b/src/lake/examples/precompile/test.sh
index a9ee14b9b018..b2265570a6b1 100755
--- a/src/lake/examples/precompile/test.sh
+++ b/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
diff --git a/src/lake/tests/precompileArgs/lakefile.lean b/src/lake/tests/precompileArgs/lakefile.lean
index 785966cbf714..4a63e8eb87c0 100644
--- a/src/lake/tests/precompileArgs/lakefile.lean
+++ b/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 #[]
diff --git a/src/lake/tests/precompileArgs/test.sh b/src/lake/tests/precompileArgs/test.sh
index df071f1b8415..99181f0cc2c4 100755
--- a/src/lake/tests/precompileArgs/test.sh
+++ b/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