feat: lake: Dynlib.runtimeOnlyDeps (#14220)

This PR adds `Dynlib.runtimeOnlyDeps`. It specifies transitive
dependencies that should not be linked, but need to be preloaded for
`lean` elaboration when precompiling (e.g., libraries dynamically loaded
at runtime via `dlopen`).

Author: tydeu

src/lake/Lake/Build/Module.lean

@@ -180,8 +180,10 @@ where
       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 =>
+    let step := fun (v, o) lib =>
       go lib ps v o
+    let (v, o) ← lib.deps.foldlM step (v, o)
+    let (v, o) ← lib.runtimeOnlyDeps.foldlM step (v, o)
     let o := o.push lib
     return (v, o)
 

src/lake/Lake/Config/Dynlib.lean

@@ -16,7 +16,7 @@ namespace Lake
 public structure Dynlib where
   /-- Library file path. -/
   path : FilePath
-  /-- Library name without platform-specific prefix/suffix (for `-l`). -/
+  /-- Library name without any platform-specific prefix/suffix (for `-l`). -/
   name : String
   /-- Whether this library can be loaded as a plugin. -/
   plugin := false
@@ -25,6 +25,12 @@ public structure Dynlib where
   (e.g., linking on Windows, loading via `lean`).
   -/
   deps : Array Dynlib := #[]
+  /--
+  Non-link transitive dependencies of this library that are only required
+  at runtime (e.g., libraries loaded dynamically via `dlopen`). Used by Lake
+  to preload such dependencies for `lean` elaboration when precompiling.
+  -/
+  runtimeOnlyDeps : Array Dynlib := #[]
   deriving Inhabited, Repr
 
 namespace Dynlib