fix: lake: library load & link order (#7809)

This PR fixes the order of libraries when loading them via
`--load-dynlib` or `--plugin` in `lean` and when linking them into a
shared library or executable. A `Dynlib` now tracks its dependencies and
they are topologically sorted before being passed to either linking or
loading.

Closes #7790.

src/lake/Lake/Build/Common.lean

@@ -209,14 +209,14 @@ def fetchFileTrace (file : FilePath) (text := false) : JobM BuildTrace := do
 
 /--
 Builds `file` using `build` unless it already exists and the current job's
-trace matches the trace stored in the `.trace` file. If built, save the new
-trace and cache `file`'s hash in a `.hash` file. Otherwise, try to fetch the
+trace matches the trace stored in the `.trace` file. If built, saves the new
+trace and caches `file`'s hash in a `.hash` file. Otherwise, tries to fetch the
 hash from the `.hash` file using `fetchFileTrace`. Build logs (if any) are
 saved to the trace file and replayed from there if the build is skipped.
 
 For example, given `file := "foo.c"`, compares `getTrace` with that in
-`foo.c.trace` with the hash cached in `foo.c.hash` and the log cached in
-`foo.c.trace`.
+`foo.c.trace`. If built, the hash is cached in `foo.c.hash` and the new
+trace is saved to `foo.c.trace` (including the build log).
 
 If `text := true`, `file` is hashed as a text file rather than a binary file.
 -/
@@ -395,6 +395,29 @@ private def mkLinkObjArgs
     args := args.push s!"-l{lib.name}"
   return args
 
+/--
+Topologically sorts the library dependency tree by name.
+Libraries come *before* their dependencies.
+-/
+private partial def mkLinkOrder (libs : Array Dynlib) : JobM (Array Dynlib) := do
+  let r := libs.foldlM (m := Except (Cycle String)) (init := ({}, #[])) fun (v, o) lib =>
+    go lib [] v o
+  match r with
+  | .ok (_, order) => pure order
+  | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}"
+where
+  go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do
+    let o := o.push lib
+    if v.contains lib.name then
+      return (v, o)
+    if ps.contains lib.name then
+      throw (lib.name :: ps)
+    let ps := lib.name :: ps
+    let v := v.insert lib.name ()
+    let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib =>
+      go lib ps v o
+    return (v, o)
+
 /--
 Build a shared library by linking the results of `linkJobs`
 using the Lean toolchain's C compiler.
@@ -404,7 +427,7 @@ def buildSharedLib
   (linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
   (weakArgs traceArgs : Array String := #[]) (linker := "c++")
   (extraDepTrace : JobM _ := pure BuildTrace.nil)
-  (plugin := false)
+  (plugin := false) (linkDeps := Platform.isWindows)
 : SpawnM (Job Dynlib) :=
   (Job.collectArray linkObjs).bindM fun objs => do
   (Job.collectArray linkLibs).mapM (sync := true) fun libs => do
@@ -412,9 +435,10 @@ def buildSharedLib
     addPlatformTrace -- shared libraries are platform-dependent artifacts
     addTrace (← extraDepTrace)
     buildFileUnlessUpToDate' libFile do
+      let libs ← if linkDeps then mkLinkOrder libs else pure #[]
       let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs
       compileSharedLib libFile args linker
-    return {name := libName, path := libFile, plugin}
+    return {name := libName, path := libFile, deps := libs, plugin}
 
 /--
 Build a shared library by linking the results of `linkJobs`
@@ -424,6 +448,7 @@ def buildLeanSharedLib
   (libName : String) (libFile : FilePath)
   (linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
   (weakArgs traceArgs : Array String := #[]) (plugin := false)
+  (linkDeps := Platform.isWindows)
 : SpawnM (Job Dynlib) :=
   (Job.collectArray linkObjs).bindM fun objs => do
   (Job.collectArray linkLibs).mapM (sync := true) fun libs => do
@@ -432,10 +457,11 @@ def buildLeanSharedLib
     addPlatformTrace -- shared libraries are platform-dependent artifacts
     buildFileUnlessUpToDate' libFile do
       let lean ← getLeanInstall
+      let libs ← if linkDeps then mkLinkOrder libs else pure #[]
       let args := mkLinkObjArgs objs libs ++
         weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
       compileSharedLib libFile args lean.cc
-    return {name := libName, path := libFile, plugin}
+    return {name := libName, path := libFile, deps := libs, plugin}
 
 /--
 Build an executable by linking the results of `linkJobs`
@@ -453,6 +479,7 @@ def buildLeanExe
     addPlatformTrace -- executables are platform-dependent artifacts
     buildFileUnlessUpToDate' exeFile do
       let lean ← getLeanInstall
+      let libs ← mkLinkOrder libs
       let args := mkLinkObjArgs objs libs ++
         weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
       compileExe exeFile args lean.cc

src/lake/Lake/Build/Fetch.lean

@@ -36,7 +36,7 @@ abbrev RecBuildT (m : Type → Type) :=
 
 /-- Log build cycle and error. -/
 @[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
-  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
+  error s!"build cycle detected:\n{formatCycle cycle}"
 
 instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
   throwCycle := buildCycleError

src/lake/Lake/Build/Imports.lean

@@ -37,8 +37,8 @@ def buildImportsAndDeps
     let dynlibsJob ← root.dynlibs.fetchIn root
     let pluginsJob ← root.plugins.fetchIn root
     modJob.bindM fun _ =>
-    impLibsJob.bindM fun impLibs =>
-    dynlibsJob.bindM fun dynlibs =>
-    pluginsJob.bindM fun plugins =>
-    externLibsJob.mapM fun externLibs => do
-      return computeModuleDeps impLibs externLibs dynlibs plugins
+    impLibsJob.bindM (sync := true) fun impLibs =>
+    dynlibsJob.bindM (sync := true) fun dynlibs =>
+    pluginsJob.bindM (sync := true) fun plugins =>
+    externLibsJob.mapM (sync := true) fun externLibs => do
+      computeModuleDeps impLibs externLibs dynlibs plugins

src/lake/Lake/Build/Library.lean

@@ -96,27 +96,22 @@ protected def LeanLib.recBuildShared (self : LeanLib) : FetchM (Job Dynlib) := d
   let objJobs ← self.moreLinkObjs.foldlM (init := objJobs)
     (·.push <$> ·.fetchIn self.pkg)
   let libJobs ← id do
-    -- Fetch dependnecy dynlibs
-    -- for platforms that must link to them (e.g., Windows)
-    if Platform.isWindows then
-      let imps ← mods.foldlM (init := OrdModuleSet.empty) fun imps mod => do
-        return imps.appendArray (← (← mod.transImports.fetch).await)
-      let s := (NameSet.empty.insert self.name, #[])
-      let (_, jobs) ← imps.foldlM (init := s) fun (libs, jobs) imp => do
-        if libs.contains imp.lib.name then
-          return (libs, jobs)
-        else
-          let job ← imp.lib.shared.fetch
-          let moreJobs ← imp.lib.moreLinkLibs.mapM (·.fetchIn self.pkg)
-          let jobs := jobs.push job ++ moreJobs
-          return (libs.insert imp.lib.name, jobs)
-      let jobs ← self.moreLinkLibs.foldlM
-        (·.push <$> ·.fetchIn self.pkg) jobs
-      let jobs ← self.pkg.externLibs.foldlM
-        (·.push <$> ·.dynlib.fetch) jobs
-      return jobs
-    else
-      return #[]
+    -- Fetch dependency dynlibs
+    -- for situations that need them (see `Dynlib.deps`)
+    let imps ← mods.foldlM (init := OrdModuleSet.empty) fun imps mod => do
+      return imps.appendArray (← (← mod.transImports.fetch).await)
+    let s := (NameSet.empty.insert self.name, #[])
+    let (_, jobs) ← imps.foldlM (init := s) fun (libs, jobs) imp => do
+      if libs.contains imp.lib.name then
+        return (libs, jobs)
+      else
+        let jobs ← jobs.push <$> imp.lib.shared.fetch
+        return (libs.insert imp.lib.name, jobs)
+    let jobs ← self.moreLinkLibs.foldlM
+      (·.push <$> ·.fetchIn self.pkg) jobs
+    let jobs ← self.pkg.externLibs.foldlM
+      (·.push <$> ·.dynlib.fetch) jobs
+    return jobs
   buildLeanSharedLib self.libName self.sharedLibFile objJobs libJobs
     self.weakLinkArgs self.linkArgs (plugin := self.roots.size == 1)
 

src/lake/Lake/Build/Module.lean

@@ -106,54 +106,70 @@ def fetchExternLibs (pkgs : Array Package) : FetchM (Job (Array Dynlib)) :=
   Job.collectArray <$> pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch))
 
 private def Module.fetchImportLibsCore
-  (self : Module) (imps : Array Module)
-  (init : NameSet × Array (Job Dynlib)): FetchM (NameSet × Array (Job Dynlib))
-:= imps.foldlM (init := init) fun (libs, jobs) imp => do
-  if libs.contains imp.lib.name then
-    return (libs, jobs)
-  else if self.lib.name = imp.lib.name then
-    let job ← imp.dynlib.fetch
-    return (libs, jobs.push job)
-  else
-
-    let jobs ← imp.lib.moreLinkLibs.foldlM (init := jobs)
-      (·.push <$> ·.fetchIn imp.pkg)
-    -- Lean wants the external library symbols before module symbols.
-    let jobs ← jobs.push <$> imp.lib.shared.fetch
-    return (libs.insert imp.lib.name, jobs)
-
+  (self : Module) (imps : Array Module) (compileSelf : Bool)
+  (init : NameSet × Array (Job Dynlib))
+: FetchM (NameSet × Array (Job Dynlib)) :=
+  imps.foldlM (init := init) 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
+      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)
+    else
+      return (libs, jobs)
 /--
 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.
 -/
 @[inline] private def Module.fetchImportLibs
-  (self : Module) (imps : Array Module) : FetchM (Job (Array Dynlib))
-:= do
-  let s ← self.fetchImportLibsCore imps ({}, #[])
-  return Job.collectArray s.2
+  (self : Module) (imps : Array Module) (compileSelf : Bool)
+: FetchM (Array (Job Dynlib)) :=
+  (·.2) <$> self.fetchImportLibsCore imps compileSelf ({}, #[])
 
 /-- Fetch the dynlibs of a list of imports. **For internal use.**  -/
 @[inline] def fetchImportLibs
   (mods : Array Module) : FetchM (Job (Array Dynlib))
 := do
   let (_, jobs) ← mods.foldlM (init := ({}, #[])) fun s mod => do
-    let precompileImports ←
-      if mod.shouldPrecompile
-      then mod.transImports.fetch
-      else mod.precompileImports.fetch
-    let precompileImports ← precompileImports.await
-    mod.fetchImportLibsCore precompileImports s
+    let imports ← (← mod.imports.fetch).await
+    mod.fetchImportLibsCore imports mod.shouldPrecompile s
   let jobs ← mods.foldlM (init := jobs) fun jobs mod => do
-    if mod.shouldPrecompile
-    then jobs.push <$> mod.dynlib.fetch
+    if mod.shouldPrecompile then
+      jobs.push <$> mod.dynlib.fetch
     else return jobs
   return Job.collectArray jobs
 
+/--
+Topologically sorts the library dependency tree by name.
+Libraries come *after* their dependencies.
+-/
+private partial def mkLoadOrder (libs : Array Dynlib) : FetchM (Array Dynlib) := do
+  let r := libs.foldlM (m := Except (Cycle String)) (init := ({}, #[])) fun (v, o) lib =>
+    go lib [] v o
+  match r with
+  | .ok (_, order) => pure order
+  | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}"
+where
+  go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do
+    if v.contains lib.name then
+      return (v, o)
+    if ps.contains lib.name then
+      throw (lib.name :: ps)
+    let ps := lib.name :: ps
+    let v := v.insert lib.name ()
+    let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib =>
+      go lib ps v o
+    let o := o.push lib
+    return (v, o)
+
 def computeModuleDeps
   (impLibs : Array Dynlib) (externLibs : Array Dynlib)
   (dynlibs : Array Dynlib) (plugins : Array Dynlib)
-: ModuleDeps := Id.run do
+: FetchM ModuleDeps := do
   /-
   Requirements:
   * Lean wants the external library symbols before module symbols.
@@ -162,8 +178,9 @@ def computeModuleDeps
     Everything else loads fine with just the augmented library path.
   * Linux needs the augmented path to resolve nested dependencies in dynlibs.
   -/
-  let mut plugins := plugins
+  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
@@ -190,20 +207,17 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
     if imp.name = mod.name then
       logError s!"{mod.leanFile}: module imports itself"
     imp.olean.fetch
-  let precompileImports ← if mod.shouldPrecompile then
-    mod.transImports.fetch else mod.precompileImports.fetch
-  let precompileImports ← precompileImports.await
-  let importLibsJob ← mod.fetchImportLibs precompileImports
-  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty
-  let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs
-  let externLibsJob ← fetchExternLibs pkgs.toArray
+  let impLibsJob ← Job.collectArray <$>
+    mod.fetchImportLibs directImports mod.shouldPrecompile
+  let externLibsJob ← Job.collectArray <$>
+    mod.pkg.externLibs.mapM (·.dynlib.fetch)
   let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg
   let pluginsJob ← mod.plugins.fetchIn mod.pkg
 
   extraDepJob.bindM fun _ => do
   importJob.bindM (sync := true) fun _ => do
   let depTrace ← takeTrace
-  importLibsJob.bindM (sync := true) fun impLibs => do
+  impLibsJob.bindM (sync := true) fun impLibs => do
   externLibsJob.bindM (sync := true) fun externLibs => do
   dynlibsJob.bindM (sync := true) fun dynlibs => do
   pluginsJob.mapM (sync := true) fun plugins => do
@@ -211,7 +225,7 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
     | none => addTrace depTrace
     | some false => addTrace depTrace; addPlatformTrace
     | some true => setTrace depTrace
-    return computeModuleDeps impLibs externLibs dynlibs plugins
+    computeModuleDeps impLibs externLibs dynlibs plugins
 
 /-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/
 def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
@@ -366,44 +380,21 @@ def Module.oFacetConfig : ModuleFacetConfig oFacet :=
 Recursively build the shared library of a module
 (e.g., for `--load-dynlib` or `--plugin`).
 -/
--- TODO: Return `Job OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`?
 def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) :=
   withRegisterJob s!"{mod.name}:dynlib" do
-
   -- Fetch object files
-  let modLinkJobs ← mod.nativeFacets true |>.mapM (·.fetch mod)
-  let modLinksJob := Job.collectArray modLinkJobs
-
-  -- Build dynlib
-  let buildDynlib (moreLibs : Array Dynlib) :=
-    modLinksJob.mapM fun modLinks => do
-      addLeanTrace
-      addPlatformTrace -- shared libraries are platform-dependent artifacts
-      addPureTrace mod.linkArgs
-      buildFileUnlessUpToDate' mod.dynlibFile do
-        let lean ← getLeanInstall
-        let args :=
-          modLinks.map toString ++
-          moreLibs.map (·.path.toString) ++
-          mod.weakLinkArgs ++ mod.linkArgs ++ lean.ccLinkSharedFlags
-        compileSharedLib mod.dynlibFile args lean.cc
-      return ⟨mod.dynlibFile, mod.dynlibName, true⟩
-
+  let objJobs ← (mod.nativeFacets true).mapM (·.fetch mod)
   -- Fetch dependencies' dynlibs
-  -- for platforms that must link to them (e.g., Windows)
-  if Platform.isWindows then
-    let imps ← (← mod.transImports.fetch).await
-    let impLibs ← mod.fetchImportLibs imps
-    let dynlibsJob ← (mod.dynlibs ++ mod.plugins).fetchIn mod.pkg
-    let pkgs := imps.foldl (·.insert ·.pkg) OrdPackageSet.empty
-      |>.insert mod.pkg |>.toArray
-    let externLibsJob ← fetchExternLibs pkgs
-    impLibs.bindM fun impLibs =>
-    dynlibsJob.bindM (sync := true) fun dynlibs =>
-    externLibsJob.bindM (sync := true) fun externLibs =>
-      buildDynlib (impLibs ++ externLibs ++ dynlibs)
-  else
-    buildDynlib #[]
+  let libJobs ← id do
+    let imps ← (← mod.imports.fetch).await
+    let libJobs ← mod.fetchImportLibs imps true
+    let libJobs ← mod.lib.moreLinkLibs.foldlM
+      (·.push <$> ·.fetchIn mod.pkg) libJobs
+    let libJobs ← mod.pkg.externLibs.foldlM
+      (·.push <$> ·.dynlib.fetch) libJobs
+    return libJobs
+  buildLeanSharedLib mod.dynlibName mod.dynlibFile objJobs libJobs
+    mod.weakLinkArgs mod.linkArgs (plugin := true)
 
 /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
 def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=

src/lake/Lake/Build/Target/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Build.Data
+import Lake.Build.Key
 
 /-!
 # Lake Targets

src/lake/Lake/Config/Dynlib.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Config.OutFormat
+import Lake.Build.Target.Basic
 
 open System Lean
 
@@ -18,6 +19,11 @@ structure Dynlib where
   name : String
   /-- Whether this library can be loaded as a plugin. -/
   plugin := false
+  /--
+  Transitive dependencies of this library for situations that need them
+  (e.g., linking on Windows, loading via `lean`).
+  -/
+  deps : Array Dynlib := #[]
   deriving Inhabited, Repr
 
 /-- Optional library directory (for `-L`). -/

src/lake/Lake/Load/Resolve.lean

@@ -81,7 +81,7 @@ abbrev DepStackT m := CallStackT Name m
 
 /-- Log dependency cycle and error. -/
 @[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α :=
-  error s!"dependency cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
+  error s!"dependency cycle detected:\n{formatCycle cycle}"
 
 instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where
   throwCycle := depCycleError

src/lake/Lake/Util/Cycle.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 prelude
 import Init.Control.Except
 import Init.Data.List.Basic
+import Init.Data.ToString
 
 namespace Lake
 
@@ -15,6 +16,9 @@ abbrev CallStack κ := List κ
 /-- A `CallStack` ending in a cycle. -/
 abbrev Cycle κ := CallStack κ
 
+def formatCycle [ToString κ] (cycle : Cycle κ) : String :=
+  "\n".intercalate <| cycle.map (s!"  {·}")
+
 /-- A monad equipped with a call stack. -/
 class MonadCallStackOf (κ :  semiOutParam (Type u)) (m : Type u → Type v) where
   getCallStack : m (CallStack κ)

src/lake/tests/badImport/test.sh

@@ -1,9 +1,5 @@
 #!/usr/bin/env bash
-set -euo pipefail
-
-exit 0  # TODO: flaky test disabled
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh
 
 ./clean.sh
 
@@ -14,36 +10,6 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/3351
 # https://github.com/leanprover/lean4/issues/3809
 
-test_run() {
-  echo "[Command]"
-  echo "$> lake" "$@"
-  if $LAKE "$@" >produced.out 2>&1; then
-    rc=$?
-  else
-    rc=$?
-  fi
-  echo "Lake exited with code $rc"
-  echo "[Output]"
-  cat produced.out
-  return $rc
-}
-
-test_err() {
-  expected=$1; shift
-  if test_run "$@"; then rc=$?; else rc=$?; fi
-  echo "[Match \"$expected\"]"
-  if grep --color -F "$expected" produced.out; then
-    if [ $rc != 1 ]; then
-      echo "[Outcome]"
-      echo "Lake unexpectedly succeeded."
-      return 1
-    fi
-  else
-    echo "No match found."
-    return 1
-  fi
-}
-
 # Test a module with a bad import does not kill the whole build
 test_err "Building Etc" build Lib.U Etc
 # Test importing a missing module from outside the workspace

src/lake/tests/buildArgs/test.sh

@@ -1,41 +1,11 @@
 #!/usr/bin/env bash
-set -euo pipefail
-
-exit 0  # TODO: flaky test disabled
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+source ../common.sh
 
 ./clean.sh
 
 # Test that changing `moreLean/Leanc/LinkArgs` triggers a rebuild
 # Test that changing `weakLean/Leanc/LinkArgs` does not
 
-test_run() {
-  echo "[Command]"
-  echo "$> lake" "$@"
-  if $LAKE "$@" >produced.out 2>&1; then
-    rc=$?
-  else
-    rc=$?
-  fi
-  echo "Lake exited with code $rc"
-  echo "[Output]"
-  cat produced.out
-  return $rc
-}
-
-test_out() {
-  expected=$1; shift
-  if test_run "$@"; then rc=$?; else rc=$?; fi
-  echo "[Match \"$expected\"]"
-  if grep --color -F "$expected" produced.out; then
-    return $rc
-  else
-    echo "No match found."
-    return 1
-  fi
-}
-
 # Test `leanArgs`
 test_run build +Hello -R
 # see https://github.com/leanprover/lake/issues/50

src/lake/tests/common.sh

@@ -0,0 +1,65 @@
+set -euo pipefail
+
+LAKE=${LAKE:-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
+
+test_run() {
+  echo "[COMMAND]"
+  echo "$> lake" "$@"
+  if $LAKE "$@" >produced.out 2>&1; then
+    rc=$?
+  else
+    rc=$?
+  fi
+  echo "Lake exited with code $rc"
+  echo "[OUTPUT]"
+  cat produced.out
+  return $rc
+}
+
+match_out() {
+  expected=$1; shift
+  echo "[MATCH \"$expected\"]"
+  if grep --color -F -- "$expected" produced.out; then
+    return 0
+  else
+    echo "No match found."
+    return 1
+  fi
+}
+
+test_out() {
+  expected=$1; shift
+  if test_run "$@"; then rc=$?; else rc=$?; fi
+  match_out "$expected"
+  return $rc
+}
+
+test_err() {
+  expected=$1; shift
+  if test_run "$@"; then rc=$?; else rc=$?; fi
+  if match_out "$expected"; then
+    if [ $rc != 1 ]; then
+      echo "[OUTCOME]"
+      echo "Lake unexpectedly succeeded."
+      return 1
+    fi
+  fi
+}
+
+test_maybe_err() {
+  expected=$1; shift
+  test_run "$@" || true
+  match_out "$expected"
+}
+

src/lake/tests/precompileArgs/clean.sh

@@ -1 +0,0 @@
-rm -rf .lake lake-manifest.json

src/lake/tests/precompileArgs/test.sh

@@ -1,29 +0,0 @@
-#!/usr/bin/env bash
-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 -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/lean/Foo_Bar.$SHARED_LIB_EXT
-($LAKE build 2>&1 --rehash && exit 1 || true) | grep --color "Building Foo"
-rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
-$LAKE build -R -KplatformIndependent=true
-echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
-$LAKE build --rehash --no-build

src/lake/tests/precompileLink/Foo.lean

@@ -1 +1,2 @@
 import Foo.Bar
+import Foo.Baz

src/lake/tests/precompileLink/Foo/Baz.lean

@@ -0,0 +1,3 @@
+import FooDep
+
+initialize greetingRef : IO.Ref String ← IO.mkRef greeting

src/lake/tests/precompileLink/FooDep.lean

@@ -0,0 +1,3 @@
+import FooDepDep
+
+def greeting := hello

src/lake/tests/precompileLink/FooDepDep.lean

@@ -0,0 +1 @@
+def hello := "Hello"

src/lake/tests/precompileLink/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out

src/lake/tests/precompileLink/lakefile.lean

@@ -8,3 +8,7 @@ lean_lib Foo where
   precompileModules := true
   platformIndependent := if get_config? platformIndependent |>.isSome then true else none
   moreLinkArgs := if let some cfg := get_config? linkArgs then cfg.splitOn " " |>.toArray else #[]
+
+lean_lib FooDep
+lean_lib FooDepDep
+lean_exe orderTest

src/lake/tests/precompileLink/orderTest.lean

@@ -0,0 +1,7 @@
+-- import a module of lib `Foo`  which does not import `FooDep`
+import Foo.Bar
+-- then, import a module which does
+import Foo.Baz
+
+def main : IO Unit := do
+  IO.println (← greetingRef.get)

src/lake/tests/precompileLink/test.sh

@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Test that the link & load order of precompiled libraries is correct
+# https://github.com/leanprover/lean4/issues/7790
+test_run -v exe orderTest
+
+# 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
+test_run build -R
+echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+test_err "Building Foo" build --rehash
+rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+test_run build -R -KplatformIndependent=true
+echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+test_run build --rehash --no-build
+
+# cleanup
+rm -f produced.out

src/shell/CMakeLists.txt

@@ -185,11 +185,12 @@ ENDFOREACH(T)
 # bootstrap: too slow
 # toolchain: requires elan to download toolchain
 # online: downloads remote repositories
+# badImport/buildArgs: flaky for unknown reasons
 file(GLOB_RECURSE LEANLAKETESTS
   "${LEAN_SOURCE_DIR}/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
-  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
+  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online|buildArgs|badImport).*")
     GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
     GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
     add_test(NAME "leanlaketest_${DIR_NAME}"