From 7a394172986e4020362fcaa9fed4a22ef2e34996 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 8 Jul 2026 11:19:54 -0400
Subject: [PATCH 01/10] fix(Lake): load missing dynlibs individually with
 precompileModules

---
 src/lake/Lake/Build/Module.lean               | 47 ++++++++++++-------
 .../Downstream/ImportDetached.lean            |  3 ++
 .../tests/precompileLink/Foo/Detached.lean    |  3 ++
 .../tests/precompileLink/ImportDetached.lean  |  3 ++
 tests/lake/tests/precompileLink/test.sh       |  5 ++
 5 files changed, 45 insertions(+), 16 deletions(-)
 create mode 100644 tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
 create mode 100644 tests/lake/tests/precompileLink/Foo/Detached.lean
 create mode 100644 tests/lake/tests/precompileLink/ImportDetached.lean

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 1266fd0bf409..f49955b99016 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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"
diff --git a/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean b/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
new file mode 100644
index 000000000000..05215d22448c
--- /dev/null
+++ b/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
@@ -0,0 +1,3 @@
+import Foo.Detached
+
+#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/Foo/Detached.lean b/tests/lake/tests/precompileLink/Foo/Detached.lean
new file mode 100644
index 000000000000..06b03798ddab
--- /dev/null
+++ b/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
diff --git a/tests/lake/tests/precompileLink/ImportDetached.lean b/tests/lake/tests/precompileLink/ImportDetached.lean
new file mode 100644
index 000000000000..05215d22448c
--- /dev/null
+++ b/tests/lake/tests/precompileLink/ImportDetached.lean
@@ -0,0 +1,3 @@
+import Foo.Detached
+
+#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/test.sh b/tests/lake/tests/precompileLink/test.sh
index 5e52c36a1213..13dd7e747188 100755
--- a/tests/lake/tests/precompileLink/test.sh
+++ b/tests/lake/tests/precompileLink/test.sh
@@ -17,6 +17,11 @@ 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.
+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

From dca7655545d3b709370233dcbe5ef2f1507ef51f Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 8 Jul 2026 14:00:47 -0400
Subject: [PATCH 02/10] fix: typo

---
 tests/lake/tests/precompileLink/test.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lake/tests/precompileLink/test.sh b/tests/lake/tests/precompileLink/test.sh
index 13dd7e747188..fb4c91f36a3e 100755
--- a/tests/lake/tests/precompileLink/test.sh
+++ b/tests/lake/tests/precompileLink/test.sh
@@ -19,6 +19,7 @@ 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
 
@@ -28,7 +29,6 @@ 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

From aadc8da3ff277fe22bd09ab59f7303537b6fa93d Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 8 Jul 2026 22:58:10 -0400
Subject: [PATCH 03/10] fix: make test reproduce segfault

---
 tests/lake/tests/precompileLink/Downstream/ImportDetached.lean | 3 ---
 tests/lake/tests/precompileLink/Foo/Detached.lean              | 3 ++-
 .../precompileLink/PrecompiledDownstream/ImportDetached.lean   | 1 +
 .../PrecompiledDownstream/ImportImportDetached.lean            | 3 +++
 tests/lake/tests/precompileLink/lakefile.lean                  | 3 +++
 tests/lake/tests/precompileLink/test.sh                        | 3 ++-
 6 files changed, 11 insertions(+), 5 deletions(-)
 delete mode 100644 tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
 create mode 100644 tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
 create mode 100644 tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean

diff --git a/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean b/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
deleted file mode 100644
index 05215d22448c..000000000000
--- a/tests/lake/tests/precompileLink/Downstream/ImportDetached.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Foo.Detached
-
-#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/Foo/Detached.lean b/tests/lake/tests/precompileLink/Foo/Detached.lean
index 06b03798ddab..faaeafd2e9cc 100644
--- a/tests/lake/tests/precompileLink/Foo/Detached.lean
+++ b/tests/lake/tests/precompileLink/Foo/Detached.lean
@@ -1,3 +1,4 @@
 /-! A module in the library `Foo` not imported by `Foo.lean`. -/
 
-def detachedValue := 1234
+initialize detachedValue : Nat ←
+  return 1234
diff --git a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
new file mode 100644
index 000000000000..dfabaeb45912
--- /dev/null
+++ b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
@@ -0,0 +1 @@
+import Foo.Detached
diff --git a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean
new file mode 100644
index 000000000000..9b968d3b7e4b
--- /dev/null
+++ b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean
@@ -0,0 +1,3 @@
+import PrecompiledDownstream.ImportDetached
+
+#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/lakefile.lean b/tests/lake/tests/precompileLink/lakefile.lean
index 015f2039d635..5f35252910c9 100644
--- a/tests/lake/tests/precompileLink/lakefile.lean
+++ b/tests/lake/tests/precompileLink/lakefile.lean
@@ -15,6 +15,9 @@ lean_exe orderTest
 
 lean_lib Downstream
 
+lean_lib PrecompiledDownstream where
+  precompileModules := true
+
 lean_lib LakeTest
 
 lean_lib PlatformIndependent where
diff --git a/tests/lake/tests/precompileLink/test.sh b/tests/lake/tests/precompileLink/test.sh
index fb4c91f36a3e..890ffc7c6b5d 100755
--- a/tests/lake/tests/precompileLink/test.sh
+++ b/tests/lake/tests/precompileLink/test.sh
@@ -21,7 +21,8 @@ test_run -v build Downstream
 # 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_out "${PKG}_Foo_Detached.$SHARED_LIB_EXT" -v setup-file PrecompiledDownstream/ImportDetached.lean
+test_run build -R PrecompiledDownstream.ImportImportDetached
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
 ./clean.sh

From f868bd75d5bbc42331eaca8b9e9c83b60749e4e4 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Thu, 9 Jul 2026 16:13:37 -0400
Subject: [PATCH 04/10] chore: move test

---
 .../lake/tests/precompileLink/Foo/Detached.lean  |  4 ----
 .../tests/precompileLink/ImportDetached.lean     |  3 ---
 .../PrecompiledDownstream/ImportDetached.lean    |  1 -
 .../ImportImportDetached.lean                    |  3 ---
 tests/lake/tests/precompileLink/lakefile.lean    |  3 ---
 tests/lake/tests/precompileLink/test.sh          |  8 +-------
 .../Downstream/ImportDetached.lean               |  1 +
 .../Downstream/ImportImportDetached.lean         |  3 +++
 .../ImportDetached.lean                          |  3 +++
 .../precompileModules-detached/Upstream.lean     |  0
 .../Upstream/Detached.lean                       |  4 ++++
 .../tests/precompileModules-detached/clean.sh    |  1 +
 .../precompileModules-detached/lakefile.toml     |  8 ++++++++
 .../tests/precompileModules-detached/test.sh     | 16 ++++++++++++++++
 14 files changed, 37 insertions(+), 21 deletions(-)
 delete mode 100644 tests/lake/tests/precompileLink/Foo/Detached.lean
 delete mode 100644 tests/lake/tests/precompileLink/ImportDetached.lean
 delete mode 100644 tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
 delete mode 100644 tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean
 create mode 100644 tests/lake/tests/precompileModules-detached/Downstream/ImportDetached.lean
 create mode 100644 tests/lake/tests/precompileModules-detached/Downstream/ImportImportDetached.lean
 create mode 100644 tests/lake/tests/precompileModules-detached/ImportDetached.lean
 create mode 100644 tests/lake/tests/precompileModules-detached/Upstream.lean
 create mode 100644 tests/lake/tests/precompileModules-detached/Upstream/Detached.lean
 create mode 100755 tests/lake/tests/precompileModules-detached/clean.sh
 create mode 100644 tests/lake/tests/precompileModules-detached/lakefile.toml
 create mode 100755 tests/lake/tests/precompileModules-detached/test.sh

diff --git a/tests/lake/tests/precompileLink/Foo/Detached.lean b/tests/lake/tests/precompileLink/Foo/Detached.lean
deleted file mode 100644
index faaeafd2e9cc..000000000000
--- a/tests/lake/tests/precompileLink/Foo/Detached.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-/-! A module in the library `Foo` not imported by `Foo.lean`. -/
-
-initialize detachedValue : Nat ←
-  return 1234
diff --git a/tests/lake/tests/precompileLink/ImportDetached.lean b/tests/lake/tests/precompileLink/ImportDetached.lean
deleted file mode 100644
index 05215d22448c..000000000000
--- a/tests/lake/tests/precompileLink/ImportDetached.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Foo.Detached
-
-#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
deleted file mode 100644
index dfabaeb45912..000000000000
--- a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportDetached.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Foo.Detached
diff --git a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean b/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean
deleted file mode 100644
index 9b968d3b7e4b..000000000000
--- a/tests/lake/tests/precompileLink/PrecompiledDownstream/ImportImportDetached.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import PrecompiledDownstream.ImportDetached
-
-#eval detachedValue
diff --git a/tests/lake/tests/precompileLink/lakefile.lean b/tests/lake/tests/precompileLink/lakefile.lean
index 5f35252910c9..015f2039d635 100644
--- a/tests/lake/tests/precompileLink/lakefile.lean
+++ b/tests/lake/tests/precompileLink/lakefile.lean
@@ -15,9 +15,6 @@ lean_exe orderTest
 
 lean_lib Downstream
 
-lean_lib PrecompiledDownstream where
-  precompileModules := true
-
 lean_lib LakeTest
 
 lean_lib PlatformIndependent where
diff --git a/tests/lake/tests/precompileLink/test.sh b/tests/lake/tests/precompileLink/test.sh
index 890ffc7c6b5d..5e52c36a1213 100755
--- a/tests/lake/tests/precompileLink/test.sh
+++ b/tests/lake/tests/precompileLink/test.sh
@@ -17,19 +17,13 @@ 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 PrecompiledDownstream/ImportDetached.lean
-test_run build -R PrecompiledDownstream.ImportImportDetached
-
 # 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
diff --git a/tests/lake/tests/precompileModules-detached/Downstream/ImportDetached.lean b/tests/lake/tests/precompileModules-detached/Downstream/ImportDetached.lean
new file mode 100644
index 000000000000..dbca95f8b630
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/Downstream/ImportDetached.lean
@@ -0,0 +1 @@
+import Upstream.Detached
diff --git a/tests/lake/tests/precompileModules-detached/Downstream/ImportImportDetached.lean b/tests/lake/tests/precompileModules-detached/Downstream/ImportImportDetached.lean
new file mode 100644
index 000000000000..8a8ad5645558
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/Downstream/ImportImportDetached.lean
@@ -0,0 +1,3 @@
+import Downstream.ImportDetached
+
+#eval detachedValue
diff --git a/tests/lake/tests/precompileModules-detached/ImportDetached.lean b/tests/lake/tests/precompileModules-detached/ImportDetached.lean
new file mode 100644
index 000000000000..42c3d052554f
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/ImportDetached.lean
@@ -0,0 +1,3 @@
+import Upstream.Detached
+
+#eval detachedValue
diff --git a/tests/lake/tests/precompileModules-detached/Upstream.lean b/tests/lake/tests/precompileModules-detached/Upstream.lean
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/tests/lake/tests/precompileModules-detached/Upstream/Detached.lean b/tests/lake/tests/precompileModules-detached/Upstream/Detached.lean
new file mode 100644
index 000000000000..7af489468e06
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/Upstream/Detached.lean
@@ -0,0 +1,4 @@
+/-! A module in the library `Upstream` not imported by `Upstream.lean`. -/
+
+initialize detachedValue : Nat ←
+  return 1234
diff --git a/tests/lake/tests/precompileModules-detached/clean.sh b/tests/lake/tests/precompileModules-detached/clean.sh
new file mode 100755
index 000000000000..333b50aba242
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out
diff --git a/tests/lake/tests/precompileModules-detached/lakefile.toml b/tests/lake/tests/precompileModules-detached/lakefile.toml
new file mode 100644
index 000000000000..956e5ebdfb2b
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/lakefile.toml
@@ -0,0 +1,8 @@
+name = "precompileModules-detached"
+precompileModules = true
+
+[[lean_lib]]
+name = "Upstream"
+
+[[lean_lib]]
+name = "Downstream"
diff --git a/tests/lake/tests/precompileModules-detached/test.sh b/tests/lake/tests/precompileModules-detached/test.sh
new file mode 100755
index 000000000000..f1bb6f3349e5
--- /dev/null
+++ b/tests/lake/tests/precompileModules-detached/test.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Test that a precompiled module absent from its parent library's shared target
+# is loaded as an individual dylib when elaborating a downstream module that imports it.
+PKG="precompileModules_x2ddetached"
+test_out "${PKG}_Upstream_Detached.$SHARED_LIB_EXT" -v setup-file ImportDetached.lean
+test_out "${PKG}_Upstream_Detached.$SHARED_LIB_EXT" -v setup-file Downstream/ImportDetached.lean
+
+# This segfaults if the individual module dynlib isn't loaded.
+test_run build -R Downstream.ImportImportDetached
+
+# cleanup
+rm -f produced.out

From 0926f6c86fd3178a2e82d751e11e40fb12e481a5 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Thu, 9 Jul 2026 16:26:05 -0400
Subject: [PATCH 05/10] feat: test another segfault

---
 .../precompileModules-pkgInit/Downstream.lean    |  2 ++
 .../precompileModules-pkgInit/Downstream/A.lean  |  1 +
 .../precompileModules-pkgInit/Downstream/B.lean  |  0
 .../precompileModules-pkgInit/ExternalMod.lean   |  1 +
 .../precompileModules-pkgInit/Upstream.lean      |  0
 .../Upstream/Detached.lean                       |  4 ++++
 .../tests/precompileModules-pkgInit/clean.sh     |  1 +
 .../precompileModules-pkgInit/lakefile.toml      |  8 ++++++++
 .../lake/tests/precompileModules-pkgInit/test.sh | 16 ++++++++++++++++
 9 files changed, 33 insertions(+)
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/Downstream.lean
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/Downstream/A.lean
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/Downstream/B.lean
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/ExternalMod.lean
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/Upstream.lean
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/Upstream/Detached.lean
 create mode 100755 tests/lake/tests/precompileModules-pkgInit/clean.sh
 create mode 100644 tests/lake/tests/precompileModules-pkgInit/lakefile.toml
 create mode 100755 tests/lake/tests/precompileModules-pkgInit/test.sh

diff --git a/tests/lake/tests/precompileModules-pkgInit/Downstream.lean b/tests/lake/tests/precompileModules-pkgInit/Downstream.lean
new file mode 100644
index 000000000000..9a064b7fb6a1
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/Downstream.lean
@@ -0,0 +1,2 @@
+import Downstream.A
+import Downstream.B
diff --git a/tests/lake/tests/precompileModules-pkgInit/Downstream/A.lean b/tests/lake/tests/precompileModules-pkgInit/Downstream/A.lean
new file mode 100644
index 000000000000..dbca95f8b630
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/Downstream/A.lean
@@ -0,0 +1 @@
+import Upstream.Detached
diff --git a/tests/lake/tests/precompileModules-pkgInit/Downstream/B.lean b/tests/lake/tests/precompileModules-pkgInit/Downstream/B.lean
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/tests/lake/tests/precompileModules-pkgInit/ExternalMod.lean b/tests/lake/tests/precompileModules-pkgInit/ExternalMod.lean
new file mode 100644
index 000000000000..d40cc58b06e0
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/ExternalMod.lean
@@ -0,0 +1 @@
+import Downstream.B
diff --git a/tests/lake/tests/precompileModules-pkgInit/Upstream.lean b/tests/lake/tests/precompileModules-pkgInit/Upstream.lean
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/tests/lake/tests/precompileModules-pkgInit/Upstream/Detached.lean b/tests/lake/tests/precompileModules-pkgInit/Upstream/Detached.lean
new file mode 100644
index 000000000000..7af489468e06
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/Upstream/Detached.lean
@@ -0,0 +1,4 @@
+/-! A module in the library `Upstream` not imported by `Upstream.lean`. -/
+
+initialize detachedValue : Nat ←
+  return 1234
diff --git a/tests/lake/tests/precompileModules-pkgInit/clean.sh b/tests/lake/tests/precompileModules-pkgInit/clean.sh
new file mode 100755
index 000000000000..333b50aba242
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out
diff --git a/tests/lake/tests/precompileModules-pkgInit/lakefile.toml b/tests/lake/tests/precompileModules-pkgInit/lakefile.toml
new file mode 100644
index 000000000000..3dfc10719719
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/lakefile.toml
@@ -0,0 +1,8 @@
+name = "precompileModules-pkgInit"
+precompileModules = true
+
+[[lean_lib]]
+name = "Upstream"
+
+[[lean_lib]]
+name = "Downstream"
diff --git a/tests/lake/tests/precompileModules-pkgInit/test.sh b/tests/lake/tests/precompileModules-pkgInit/test.sh
new file mode 100755
index 000000000000..b856278161df
--- /dev/null
+++ b/tests/lake/tests/precompileModules-pkgInit/test.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Test that elaborating `ExternalMod` succeeds.
+# Prior to https://github.com/leanprover/lean4/pull/14326,
+# we used to load `Downstream` as a plugin rather than a dynlib.
+# This would try to initialize `Downstream`,
+# and then (transitively through `Downstream.A`) `Upstream.Detached`.
+# But the native symbol to initialize `Upstream.Detached` is not in `Upstream:shared`,
+# so we would get a crash.
+test_run -v lean ExternalMod.lean
+
+# cleanup
+rm -f produced.out

From 3f995b5bb16b0d649b5bc9106307786e8ded5be9 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Thu, 9 Jul 2026 16:26:42 -0400
Subject: [PATCH 06/10] fix: load imports as dynlibs

---
 src/lake/Lake/Build/Module.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index f49955b99016..e59d76c0ff01 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -221,17 +221,19 @@ def computeModuleDeps
   -/
   let impLibs ← mkLoadOrder impLibs
   let mut dynlibs := externLibs ++ dynlibs
-  let mut plugins := plugins
   for impLib in impLibs do
-    if impLib.plugin then
-      plugins := plugins.push impLib
-    else
-      dynlibs := dynlibs.push impLib
+    /- Load as dynlib (not plugin) because:
+    - imported modules will be initialized in `importModules` anyway; and
+    - since imports from a different `pkg` are loaded together through `pkg:shared`,
+      passing `pkg:shared` as a plugin would initialize too much,
+      namely all modules in `pkg` rather than just the ones we have imported. -/
+    dynlibs := dynlibs.push impLib
   /-
   On MacOS, Lake must be loaded as a plugin for
   `import Lake` to work with precompiled modules.
   https://github.com/leanprover/lean4/issues/7388
   -/
+  let mut plugins := plugins
   if Platform.isOSX && !(plugins.isEmpty && dynlibs.isEmpty) then
     plugins := plugins.push (← getLakeInstall).sharedDynlib
   return {dynlibs, plugins}

From 821c558e010a98649dcf6f6bc60b3a9e15a862b6 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Thu, 9 Jul 2026 17:09:49 -0400
Subject: [PATCH 07/10] fix: test

---
 tests/lake/tests/precompileLink/test.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/lake/tests/precompileLink/test.sh b/tests/lake/tests/precompileLink/test.sh
index 5e52c36a1213..40f5ab84136f 100755
--- a/tests/lake/tests/precompileLink/test.sh
+++ b/tests/lake/tests/precompileLink/test.sh
@@ -3,6 +3,7 @@ source ../common.sh
 
 ./clean.sh
 
+PKG=precompileArgs
 
 # Test that precompilation works with a Lake import
 # https://github.com/leanprover/lean4/issues/7388
@@ -13,8 +14,8 @@ test_run -v build LakeTest
 test_run -v exe orderTest
 
 # Test that transitively importing a precompiled module
-# from a non-precompiled module works
-test_not_out '"plugins":[]' -v setup-file ImportDownstream.lean
+# from a non-precompiled module loads the correct shared object.
+test_out "${PKG}_Foo.$SHARED_LIB_EXT" -v setup-file ImportDownstream.lean
 test_run -v build Downstream
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
@@ -23,7 +24,6 @@ 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

From d9cdae8fb3c20d06f728c2c6e93de457601591c8 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 22 Jul 2026 14:42:01 -0400
Subject: [PATCH 08/10] chore: avoid private and add doc

---
 src/lake/Lake/Build/Module.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index e59d76c0ff01..97fc7626c793 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -124,7 +124,9 @@ 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
+/-- Whether this modules is included in `lib.modules` for its parent library `lib`.
+This is false of "orphaned" modules not imported by their parent library's root module. -/
+def Module.containedInLibModules (mod : Module) : FetchM Bool := do
   return (← (← mod.lib.modules.fetch).await).contains mod
 
 /--
@@ -141,13 +143,14 @@ def Module.fetchImportLibs
       let job ← imp.dynlib.fetch
       return (libs, jobs.push job)
     else if compileSelf || imp.shouldPrecompile then
-      if ← imp.includedInSharedTarget then
+      if ← imp.containedInLibModules 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
+        -- TODO: consider linting for orphaned modules
         let job ← imp.dynlib.fetch
         return (libs, jobs.push job)
     else

From 50fcca814d28cd6d7ac5a688b0ab9bc707e5b5d0 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 22 Jul 2026 14:52:47 -0400
Subject: [PATCH 09/10] feat: use OrdHashSet in modules facet

---
 src/lake/Lake/Build/Infos.lean     | 5 +++--
 src/lake/Lake/Build/Library.lean   | 8 ++++----
 src/lake/Lake/Util/OrdHashSet.lean | 3 +++
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/lake/Lake/Build/Infos.lean b/src/lake/Lake/Build/Infos.lean
index cc9e9d546b7e..c4a31d6cb7cb 100644
--- a/src/lake/Lake/Build/Infos.lean
+++ b/src/lake/Lake/Build/Infos.lean
@@ -111,8 +111,9 @@ builtin_facet precompileImports : Module => Array Module
 /-- Shared library for `--load-dynlib`. -/
 builtin_facet dynlib : Module => Dynlib
 
-/-- A Lean library's Lean modules. -/
-builtin_facet modules : LeanLib => Array Module
+/-- A Lean library's Lean modules, topologically sorted
+(`A` comes before `B` when `B` imports `A`). -/
+builtin_facet modules : LeanLib => OrdModuleSet
 
 /-- The package's array of dependencies. -/
 builtin_facet deps : Package => Array Package
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 4ad16e148ab3..7888020277d2 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -34,7 +34,7 @@ Collect the local modules of a library.
 That is, the modules from `getModuleArray` plus their local transitive imports.
 -/
 partial def LeanLib.recCollectLocalModules
-  (self : LeanLib) : FetchM (Job (Array Module))
+  (self : LeanLib) : FetchM (Job OrdModuleSet)
 := ensureJob do
   let mut col : ModuleCollection := {}
   for mod in (← self.getModuleArray) do
@@ -43,7 +43,7 @@ partial def LeanLib.recCollectLocalModules
     -- This is not considered a fatal error because we want the modules
     -- built to provide better error categorization in the monitor.
     logError s!"{self.name}: some modules have bad imports"
-  return Job.pure col.mods
+  return Job.pure ⟨col.modSet, col.mods⟩
 where
   go root col := do
     let mut col := col
@@ -83,7 +83,7 @@ public def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
       ""
   withRegisterJob s!"{self.name}:static{suffix}" <| withCurrPackage self.pkg do
   let mods ← (← self.modules.fetch).await
-  let oJobs ← mods.flatMapM fun mod =>
+  let oJobs ← mods.toArray.flatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM (·.fetch mod)
   let moreOJobs ← self.moreLinkObjs.mapM (·.fetchIn self.pkg)
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
@@ -126,7 +126,7 @@ public def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFace
 def LeanLib.recBuildShared (self : LeanLib) : FetchM (Job Dynlib) := do
   withRegisterJob s!"{self.name}:shared" <| withCurrPackage self.pkg do
   let mods ← (← self.modules.fetch).await
-  let objJobs ← mods.flatMapM fun mod =>
+  let objJobs ← mods.toArray.flatMapM fun mod =>
     mod.nativeFacets true |>.mapM (·.fetch mod)
   let objJobs ← self.moreLinkObjs.foldlM (init := objJobs)
     (·.push <$> ·.fetchIn self.pkg)
diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean
index 25b8e9a221c6..0ceae09c4d76 100644
--- a/src/lake/Lake/Util/OrdHashSet.lean
+++ b/src/lake/Lake/Util/OrdHashSet.lean
@@ -30,6 +30,9 @@ public instance : EmptyCollection (OrdHashSet α) := ⟨empty⟩
 public def mkEmpty (size : Nat) : OrdHashSet α :=
   ⟨∅, .mkEmpty size⟩
 
+public def contains (self : OrdHashSet α) (a : α) : Bool :=
+  self.toHashSet.contains a
+
 public def insert (self : OrdHashSet α) (a : α) : OrdHashSet α :=
   if self.toHashSet.contains a then
     self

From 332cddd1287ff46f62cb1e9e6e2fa43c3f127763 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjn@lean-fro.org>
Date: Wed, 22 Jul 2026 15:34:49 -0400
Subject: [PATCH 10/10] fix: typo

---
 src/lake/Lake/Build/Module.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 97fc7626c793..6b9ee05e7f7f 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -124,7 +124,7 @@ def Module.recComputePrecompileImports (mod : Module) : FetchM (Job (Array Modul
 public def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
   mkFacetJobConfig recComputePrecompileImports (buildable := false)
 
-/-- Whether this modules is included in `lib.modules` for its parent library `lib`.
+/-- Whether this module is included in `lib.modules` for its parent library `lib`.
 This is false of "orphaned" modules not imported by their parent library's root module. -/
 def Module.containedInLibModules (mod : Module) : FetchM Bool := do
   return (← (← mod.lib.modules.fetch).await).contains mod
@@ -167,7 +167,7 @@ def fetchImportLibs
 := do
   let (_, jobs) ← mods.foldlM (init := (({} : NameSet), #[])) fun (libs, jobs) imp => do
     if imp.shouldPrecompile then
-      if ← imp.includedInSharedTarget then
+      if ← imp.containedInLibModules then
         if libs.contains imp.lib.name then
           return (libs, jobs)
         else