From 24d51b90cc4adbc68386671bba4587d6e47188d6 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Fri, 21 Jun 2024 21:24:23 -0400
Subject: [PATCH] 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             | 12 +++++------
 src/lake/examples/precompile/test.sh        |  4 +++-
 src/lake/tests/precompileArgs/lakefile.lean |  3 ++-
 src/lake/tests/precompileArgs/test.sh       | 22 ++++++++++++++++++++-
 4 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 784f9bf9846f..66caa9a62a2c 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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:
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