fix: load missing dynlibs individually with precompileModules

src/lake/Lake/Build/Module.lean

@@ -124,40 +124,55 @@ def Module.recComputePrecompileImports (mod : Module) : FetchM (Job (Array Modul
 public def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
   mkFacetJobConfig recComputePrecompileImports (buildable := false)
 
+private def Module.includedInSharedTarget (mod : Module) : FetchM Bool := do
+  return (← (← mod.lib.modules.fetch).await).contains mod
+
 /--
-Computes the transitive dynamic libraries of a module's imports.
-Modules from the same library are loaded individually, while modules
-from other libraries are loaded as part of the whole library.
--/
+Computes the dynamic libraries of `self`'s transitive imports `imps`.
+Modules from the same library as `self` are loaded individually,
+while modules from other libraries are
+- loaded through their library's shared target if they are included in this target,
+- otherwise also individually. -/
 def Module.fetchImportLibs
   (self : Module) (imps : Array Module) (compileSelf : Bool)
 : FetchM (Array (Job Dynlib)) := do
   let (_, jobs) ← imps.foldlM (init := (({} : NameSet), #[])) fun (libs, jobs) imp => do
-    if libs.contains imp.lib.name then
-      return (libs, jobs)
-    else if compileSelf && self.lib.name = imp.lib.name then
+    if compileSelf && self.lib.name = imp.lib.name then
       let job ← imp.dynlib.fetch
       return (libs, jobs.push job)
     else if compileSelf || imp.shouldPrecompile then
-      let jobs ← jobs.push <$> imp.lib.shared.fetch
-      return (libs.insert imp.lib.name, jobs)
+      if ← imp.includedInSharedTarget then
+        if libs.contains imp.lib.name then
+          return (libs, jobs)
+        else
+          let job ← imp.lib.shared.fetch
+          return (libs.insert imp.lib.name, jobs.push job)
+      else
+        let job ← imp.dynlib.fetch
+        return (libs, jobs.push job)
     else
       return (libs, jobs)
   return jobs
 
 /--
-Fetches the library dynlibs of a list of non-local imports.
-Modules are loaded as part of their whole library.
+Fetches the dynamic libraries of a list `mods` of non-local imports.
+Modules are loaded through their library's shared target if they are included in this target,
+otherwise individually.
 -/
 def fetchImportLibs
   (mods : Array Module) : FetchM (Job (Array Dynlib))
 := do
   let (_, jobs) ← mods.foldlM (init := (({} : NameSet), #[])) fun (libs, jobs) imp => do
-    if libs.contains imp.lib.name then
-      return (libs, jobs)
-    else if imp.shouldPrecompile then
-      let jobs ← jobs.push <$> imp.lib.shared.fetch
-      return (libs.insert imp.lib.name, jobs)
+    if imp.shouldPrecompile then
+      if ← imp.includedInSharedTarget then
+        if libs.contains imp.lib.name then
+          return (libs, jobs)
+        else
+          let job ← imp.lib.shared.fetch
+          return (libs.insert imp.lib.name, jobs.push job)
+      else
+        let job ← imp.dynlib.fetch
+        return (libs, jobs.push job)
     else
       return (libs, jobs)
   return Job.collectArray jobs "import dynlibs"

tests/lake/tests/precompileLink/Downstream/ImportDetached.lean

@@ -0,0 +1,3 @@
+import Foo.Detached
+
+#eval detachedValue

tests/lake/tests/precompileLink/Foo/Detached.lean

@@ -0,0 +1,3 @@
+/-! A module in the library `Foo` not imported by `Foo.lean`. -/
+
+def detachedValue := 1234

tests/lake/tests/precompileLink/ImportDetached.lean

@@ -0,0 +1,3 @@
+import Foo.Detached
+
+#eval detachedValue

tests/lake/tests/precompileLink/test.sh

@@ -17,13 +17,18 @@ test_run -v exe orderTest
 test_not_out '"plugins":[]' -v setup-file ImportDownstream.lean
 test_run -v build Downstream
 
+# Test that imports of precompiled modules absent from their library's shared target
+# load the individual module dynlib.
+PKG=precompileArgs
+test_out "${PKG}_Foo_Detached.$SHARED_LIB_EXT" -v setup-file ImportDetached.lean
+test_out "${PKG}_Foo_Detached.$SHARED_LIB_EXT" -v setup-file Downstream/ImportDetached.lean
+
 # Test that `moreLinkArgs` are included when linking precompiled modules
 ./clean.sh
 test_maybe_err "-lBogus" build -KlinkArgs=-lBogus
 ./clean.sh
 
 # Test that dynlibs are part of the module trace unless `platformIndependent` is set
-PKG=precompileArgs
 test_run build -R
 echo foo > .lake/build/lib/lean/${PKG}_Foo_Bar.$SHARED_LIB_EXT
 test_err "Building Foo" build --rehash