reverse FFI: building a "fat" static library?

Stream: lean4

[Siddharth Bhat]

What I want to do is to build a single fat library that ships with Batteries + Mathlib + <my stuff>.

I am currently doing the following in my lakefile.lean

@[default_target]
lean_lib «Monodrone» where
  defaultFacets := #[LeanLib.staticExportFacet]

This builds a.lake/build/lib/libMonodrone.a. However, the lean implementation of libMonodrone uses Batteries.Data.RBMap and Mathlib.Order.Interval.Basic. These dependencies on mathlib and batteries lead to link errors down the line when linking against libMonodrone.a, since the linker is unable to find:

"_initialize_Batteries_Data_RBMap", referenced from:
    _initialize_Monodrone in libMonodrone.a[2](Monodrone.c.o.export)
"_initialize_Mathlib_Order_Disjoint", referenced from:
    _initialize_Monodrone in libMonodrone.a[2](Monodrone.c.o.export)
"_initialize_Mathlib_Order_Interval_Basic", referenced from:
    _initialize_Monodrone in libMonodrone.a[2](Monodrone.c.o.export)

I was hoping to build a "fat static library" that includes everything transitively imported from mathlib and batteries as well. In my naive imagination, since lake already knows enough to build the associated object files, it ought to know enough to build the static library as well?

CC @Mac Malone

[Siddharth Bhat]

OK, here's a solution, I'd need @Mac Malone 's review on it to know if it's sane or not. I modified `Lake.LeanLib.recCollectLocalModules to collect all (not necessarily local) modules and smash it into a single object file:

import Lake
import Lake.Build.Library
open Lake DSL

partial def Lake.LeanLib.collectAllModulesForFatlib (self : LeanLib) : FetchM (Array Module) := do
  let mut mods := #[]
  let mut modSet := ModuleSet.empty
  for mod in (← self.getModuleArray) do
    (mods, modSet) ← go mod mods modSet
  return mods
where
  go root mods modSet := do
    let mut mods := mods
    let mut modSet := modSet
    unless modSet.contains root do
      modSet := modSet.insert root
      let imps ← root.imports.fetch
      for mod in imps do
          (mods, modSet) ← go mod mods modSet
      mods := mods.push root
    return (mods, modSet)


/-- The path to the static fat library in the package's `libDir`. -/
@[inline] def fatStaticFile (self : LeanLib) : FilePath :=
  self.pkg.nativeLibDir / nameToStaticLib s!"{self.config.libName}Fat"

@[specialize] protected def LeanLib.buildFatStatic
(self : LeanLib) : FetchM (BuildJob FilePath) := do
  withRegisterJob s!"{self.name}:fatStatic" do
  let mods := (← self.collectAllModulesForFatlib) ++ (← self.modules.fetch)
  -- trace s!"{self.name}:static{suffix} modules: {mods.map (·.name)}"
  let oJobs ← mods.concatMapM fun mod =>
    mod.nativeFacets (shouldExport := true) |>.mapM fun facet => fetch <| mod.facet facet.name
  let libFile := fatStaticFile self
  IO.println s!"successfully built: {libFile}"
  buildStaticLib libFile oJobs


library_facet fatStatic (lib : LeanLib) : FilePath :=
  LeanLib.buildFatStatic lib

package «Monodrone» where

@[default_target]
lean_lib «Monodrone» where
  defaultFacets := #[`fatStatic]

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "86653eb"

@Mac Malone could you let me know if this is a sane solution?

[Mac Malone]

@Siddharth Bhat Looks good to me! One minor comment is that you should not need to import Lake.Build.Library; that is already part of import Lake.Also, this made me realize the recCollectLocalModules code should really be using OrdModuleSet (I think the only reason it isn't is because OrdModuleSet was added later).

[Mac Malone]

Also, since you are simply trying to fetch the transitive imports, one could forgo the recursion in go entirely and just collect the root.transImports.fetchon the elements of libraries module array.

[Siddharth Bhat]

Okay, will PR this later tonight, thanks!

[Siddharth Bhat]

@Mac Malone PR'd at https://github.com/leanprover/lean4/pull/4271. It's a draft since I want to check that CI passes on Windows.

[Mac Malone]

@Siddharth Bhat Oh, I didn't realize you were suggesting this as a PR.

[Siddharth Bhat]

@Mac Malone aha, I didn't realise I didn't make that clear! Sorry about that. Yes, I believe it deserves to live upstream, since I would imagine that I (and other users) who use Lean for "reverse" FFI scenarios would benefit from by linking against lean dependencies this way, especially in complex cross-language scenarios.

[Siddharth Bhat]

What do you feel?

[Mac Malone]

It seems reasonable to me.

The PR is a bit big, so it will take some time to review. I am also on vacation next week, so I probably won't get around to it until June.

[Siddharth Bhat]

Thanks! I too find it compelling to be in lean proper.

Note that the changes to lake are small, and you already reviewed it in the chat. I added your sugggestion of using mod.transImports.fetch . The larger part of the change is another example that showcases how to use it in a new example in a library with a dependency, which has been adapted from the already existing example of reverse-ffi

Also, enjoy your vacations! :beach: