fix: lake: remove module dynlib from platform-independent trace (#4478)

Fixes a bug where Lake incorrectly included the module dynlib in a
platform-independent trace. It was incorrectly excluded only external
native libraries from the trace. Also adds a test.

src/lake/Lake/Build/Module.lean

@@ -110,22 +110,22 @@ def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array F
     imp.olean.fetch
   let precompileImports ← try mod.precompileImports.fetch
     catch errPos => return Job.error (← takeLogFrom errPos)
-  let modJobs ← precompileImports.mapM (·.dynlib.fetch)
+  let modLibJobs ← precompileImports.mapM (·.dynlib.fetch)
   let pkgs := precompileImports.foldl (·.insert ·.pkg)
     OrdPackageSet.empty |>.insert mod.pkg |>.toArray
   let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
   let externDynlibsJob ← BuildJob.collectArray externJobs
-  let modDynlibsJob ← BuildJob.collectArray modJobs
+  let modDynlibsJob ← BuildJob.collectArray modLibJobs
 
   extraDepJob.bindAsync fun _ extraDepTrace => do
   importJob.bindAsync fun _ importTrace => do
-  modDynlibsJob.bindAsync fun modDynlibs modTrace => do
+  modDynlibsJob.bindAsync fun modDynlibs modLibTrace => do
   return externDynlibsJob.mapWithTrace fun externDynlibs externTrace =>
-    let depTrace := extraDepTrace.mix <| importTrace.mix <| modTrace
+    let depTrace := extraDepTrace.mix <| importTrace
     let depTrace :=
       match mod.platformIndependent with
-      | none => depTrace.mix <| externTrace
-      | some false => depTrace.mix <| externTrace.mix <| platformTrace
+      | none => depTrace.mix <| modLibTrace.mix <| externTrace
+      | some false => depTrace.mix <| modLibTrace.mix <| externTrace.mix <| platformTrace
       | some true => depTrace
     /-
     Requirements:

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