fix: various build problems

fixes #139
touches on #132

Lake/Build/Common.lean

@@ -88,9 +88,8 @@ def buildLeanExe
   (extraDepTrace := computeHash linkArgs) fun links => do
     compileExe name exeFile links linkArgs (← getLeanc)
 
-def buildLeanSharedLibOfStatic
-(staticLibJob : BuildJob FilePath) (linkArgs : Array String := #[])
-: SchedulerM (BuildJob FilePath) :=
+def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
+(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
   staticLibJob.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let trace ← buildFileUnlessUpToDate dynlib staticTrace do
@@ -108,9 +107,9 @@ def computeDynlibOfShared
   sharedLibTarget.bindSync fun sharedLib trace => do
     if let some stem := sharedLib.fileStem then
       if Platform.isWindows then
-        return ((sharedLib.parent, stem), trace)
+        return ({path := sharedLib, name := stem}, trace)
       else if stem.startsWith "lib" then
-        return ((sharedLib.parent, stem.drop 3), trace)
+        return ({path := sharedLib, name := stem.drop 3}, trace)
       else
         error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix"
     else

Lake/Build/Executable.lean

@@ -11,7 +11,7 @@ namespace Lake
 
 protected def LeanExe.recBuildExe
 (self : LeanExe) : IndexBuildM (BuildJob FilePath) := do
-  let (_, imports) ← self.root.imports.fetch
+  let imports ← self.root.transImports.fetch
   let mut linkJobs := #[← self.root.o.fetch]
   for mod in imports do for facet in mod.nativeFacets do
     linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name

Lake/Build/Facets.lean

@@ -18,11 +18,16 @@ import said configurations for `BuildInfo`.
 namespace Lake
 export System (FilePath)
 
-/--
-A dynamic/shared library for linking.
-Represented by an optional `-L` library directory × a `-l` library name.
--/
-abbrev Dynlib := Option FilePath × String
+/-- A dynamic/shared library for linking. -/
+structure Dynlib where
+  /-- Library file path. -/
+  path : FilePath
+  /-- Library name without platform-specific prefix/suffix (for `-l`). -/
+  name : String
+
+/-- Optional library directory (for `-L`). -/
+def Dynlib.dir? (self : Dynlib) : Option FilePath :=
+  self.path.parent
 
 /-! ## Module Facets -/
 
@@ -65,10 +70,6 @@ module_data c : BuildJob FilePath
 abbrev Module.oFacet := `o
 module_data o : BuildJob FilePath
 
-/-- Shared library for `--load-dynlib`. Returns just the library name. -/
-abbrev Module.dynlibFacet := `dynlib
-module_data dynlib : BuildJob String
-
 /-! ## Package Facets -/
 
 /-- The package's cloud build release. -/

Lake/Build/Imports.lean

@@ -24,13 +24,33 @@ def Workspace.processImportList
       localImports := localImports.push mod
   return localImports
 
+/--
+Recursively build a set of imported modules and return their build jobs,
+the build jobs of their precompiled modules and the build jobs of said modules'
+external libraries.
+-/
+def recBuildImports (imports : Array Module)
+: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob FilePath)) := do
+  let mut modJobs := #[]
+  let mut precompileImports := OrdModuleSet.empty
+  for mod in imports do
+    if mod.shouldPrecompile then
+      precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod
+    else
+      precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
+    modJobs := modJobs.push <| ← mod.leanBin.fetch
+  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
+  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
+  let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
+  return (modJobs, precompileJobs, externJobs)
+
 /--
 Builds the workspace-local modules of list of imports.
 Used by `lake print-paths` to build modules for the Lean server.
 Returns the set of module dynlibs built (so they can be loaded by the server).
 
 Builds only module `.olean` and `.ilean` files if the package is configured
-as "Lean-only". Otherwise, also build `.c` files.
+as "Lean-only". Otherwise, also builds `.c` files.
 -/
 def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
   let ws ← getWorkspace
@@ -41,17 +61,10 @@ def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
   else
     -- build local imports from list
     let mods := ws.processImportList imports
-    let (importTargets, bStore) ← RecBuildM.runIn {} <| mods.mapM fun mod =>
-      if mod.shouldPrecompile then
-        (discard ·.toJob) <$> buildIndexTop mod.dynlib
-      else
-        (discard ·.toJob) <$> buildIndexTop mod.leanBin
-    let dynlibJobs := bStore.collectModuleFacetArray Module.dynlibFacet
-    let externLibJobs := bStore.collectSharedExternLibs
-    importTargets.forM (·.await)
-    -- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care)
-    let dynlibs ← dynlibJobs.mapM fun dynlib => do
-      return FilePath.mk <| nameToSharedLib (← dynlib.await)
+    let (modJobs, precompileJobs, externLibJobs) ←
+      recBuildImports mods |>.run.run
+    modJobs.forM (·.await)
+    let dynlibs ← precompileJobs.mapM (·.await <&> (·.path))
     let externLibs ← externLibJobs.mapM (·.await)
     -- NOTE: Lean wants the external library symbols before module symbols
     return externLibs ++ dynlibs

Lake/Build/Index.lean

@@ -70,12 +70,19 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
 | .dynlibExternLib lib =>
   mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
 
+/--
+Run the given recursive build using the Lake build index
+and a topological / suspending scheduler.
+-/
+def IndexBuildM.run (build : IndexBuildM α) : RecBuildM α :=
+  build <| recFetchMemoize BuildInfo.key recBuildWithIndex
+
 /--
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler.
 -/
 def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
-  buildDTop BuildData BuildInfo.key info recBuildWithIndex
+  recFetchMemoize BuildInfo.key recBuildWithIndex info
 
 /--
 Recursively build the given info using the Lake build index

Lake/Build/Info.lean

@@ -144,9 +144,25 @@ Defined here because they need to import configurations, whereas the definitions
 there need to be imported by configurations.
 -/
 
-/-- The direct × transitive imports of the Lean module. -/
-abbrev Module.importFacet := `lean.imports
-module_data lean.imports : Array Module × Array Module
+/-- The direct local imports of the Lean module. -/
+abbrev Module.importsFacet := `lean.imports
+module_data lean.imports : Array Module
+
+/-- The transitive local imports of the Lean module. -/
+abbrev Module.transImportsFacet := `lean.transImports
+module_data lean.transImports : Array Module
+
+/-- The transitive local imports of the Lean module. -/
+abbrev Module.precompileImportsFacet := `lean.precompileImports
+module_data lean.precompileImports : Array Module
+
+/-- Shared library for `--load-dynlib`. -/
+abbrev Module.dynlibFacet := `dynlib
+module_data dynlib : BuildJob Dynlib
+
+/-- A Lean library's Lean modules. -/
+abbrev LeanLib.modulesFacet := `modules
+library_data modules : Array Module
 
 /-- The package's complete array of transitive dependencies. -/
 abbrev Package.depsFacet := `deps
@@ -168,13 +184,15 @@ abbrev facet (facet : Name) (self : Module) : BuildInfo :=
 
 variable (self : Module)
 
-abbrev imports  := self.facet importFacet
-abbrev leanBin  := self.facet leanBinFacet
-abbrev olean    := self.facet oleanFacet
-abbrev ilean    := self.facet ileanFacet
-abbrev c        := self.facet cFacet
-abbrev o        := self.facet oFacet
-abbrev dynlib   := self.facet dynlibFacet
+abbrev imports            := self.facet importsFacet
+abbrev transImports       := self.facet transImportsFacet
+abbrev precompileImports  := self.facet precompileImportsFacet
+abbrev leanBin            := self.facet leanBinFacet
+abbrev olean              := self.facet oleanFacet
+abbrev ilean              := self.facet ileanFacet
+abbrev c                  := self.facet cFacet
+abbrev o                  := self.facet oFacet
+abbrev dynlib             := self.facet dynlibFacet
 
 end Module
 
@@ -198,6 +216,10 @@ abbrev Package.target (target : Name) (self : Package) : BuildInfo :=
 abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
   .libraryFacet self facet
 
+/-- Build info of the Lean library's Lean modules. -/
+abbrev LeanLib.modules (self : LeanLib) : BuildInfo :=
+  self.facet modulesFacet
+
 /-- Build info of the Lean library's Lean binaries. -/
 abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
   self.facet leanFacet

Lake/Build/Library.lean

@@ -9,34 +9,48 @@ namespace Lake
 
 /-! # Build Lean & Static Lib -/
 
-/-- Build and collect the specified facet of the library's local modules. -/
-def LeanLib.recBuildLocalModules
-(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexBuildM (Array α) := do
-  let mut results := #[]
+/--
+Collect the local modules of a library.
+That is, the modules from `getModuleArray` plus their local transitive imports.
+-/
+partial def LeanLib.recCollectLocalModules (self : LeanLib) : IndexBuildM (Array Module) := do
+  let mut mods := #[]
   let mut modSet := ModuleSet.empty
-  let mods ← self.getModuleArray
-  for mod in mods do
-    let (_, mods) ← mod.imports.fetch
-    let mods := mods.push mod
-    for mod in mods do
-      if self.isLocalModule mod.name then
-        unless modSet.contains mod do
-          for facet in facets do
-            results := results.push <| ← fetch <| mod.facet facet.name
-          modSet := modSet.insert mod
-  return results
+  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
+        if self.isLocalModule mod.name then
+          (mods, modSet) ← go mod mods modSet
+      mods := mods.push root
+    return (mods, modSet)
+
+/-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
+def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=
+  mkFacetConfig LeanLib.recCollectLocalModules
 
 protected def LeanLib.recBuildLean
 (self : LeanLib) : IndexBuildM (BuildJob Unit) := do
-  BuildJob.mixArray (α := Unit) <| ← self.recBuildLocalModules #[Module.leanBinFacet]
+  let mods ← self.modules.fetch
+  mods.foldlM (init := BuildJob.nil) fun job mod => do
+    job.mix <| ← mod.leanBin.fetch
 
 /-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
 def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
   mkFacetJobConfig LeanLib.recBuildLean
 
 protected def LeanLib.recBuildStatic
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
-  let oJobs ← self.recBuildLocalModules self.nativeFacets
+  let mods ← self.modules.fetch
+  let oJobs ← mods.concatMapM fun mod =>
+    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
   buildStaticLib self.staticLibFile oJobs
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
@@ -45,40 +59,14 @@ def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
 
 /-! # Build Shared Lib -/
 
-/--
-Build and collect the local object files and external libraries
-of a library and its modules' imports.
--/
-def LeanLib.recBuildLinks
-(self : LeanLib) : IndexBuildM (Array (BuildJob FilePath)) := do
-  -- Build and collect modules
-  let mut jobs := #[]
-  let mut pkgs := #[]
-  let mut pkgSet := PackageSet.empty
-  let mut modSet := ModuleSet.empty
-  let mods ← self.getModuleArray
-  for mod in mods do
-    let (_, mods) ← mod.imports.fetch
-    let mods := mods.push mod
-    for mod in mods do
-      unless modSet.contains mod do
-        unless pkgSet.contains mod.pkg do
-            pkgSet := pkgSet.insert mod.pkg
-            pkgs := pkgs.push mod.pkg
-        if self.isLocalModule mod.name then
-          for facet in self.nativeFacets do
-            jobs := jobs.push <| ← fetch <| mod.facet facet.name
-        modSet := modSet.insert mod
-  -- Build and collect external library jobs
-  for pkg in pkgs do
-    let externLibJobs ← pkg.externLibs.mapM (·.shared.fetch)
-    for job in externLibJobs do
-      jobs := jobs.push job
-  return jobs
-
 protected def LeanLib.recBuildShared
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
-  buildLeanSharedLib self.sharedLibFile (← self.recBuildLinks) self.linkArgs
+  let mods ← self.modules.fetch
+  let oJobs ← mods.concatMapM fun mod =>
+    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
+  let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
+  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
+  buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.linkArgs
 
 /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
 def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
@@ -87,10 +75,11 @@ def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
 open LeanLib in
 /--
 A library facet name to build function map that contains builders for
-the initial set of Lake package facets (e.g., `lean`, `static`, and `shared`).
+the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`).
 -/
 def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
   DNameMap.empty
+  |>.insert modulesFacet modulesFacetConfig
   |>.insert leanFacet leanFacetConfig
   |>.insert staticFacet staticFacetConfig
   |>.insert sharedFacet sharedFacetConfig