refactor: make LeanLib.buildModules a proper recursive build

Lake/Build/Facets.lean

@@ -70,6 +70,10 @@ package_data extraDep : ActiveOpaqueTarget
 
 /-! ## Target Facets -/
 
+/-- A Lean library's Lean libraries. -/
+abbrev LeanLib.leanFacet := `leanLib.lean
+target_data leanLib.lean : ActiveOpaqueTarget
+
 /-- A Lean library's static binary. -/
 abbrev LeanLib.staticFacet := `leanLib.static
 target_data leanLib.static : ActiveFileTarget

Lake/Build/Index.lean

@@ -32,39 +32,40 @@ dynamically typed equivalent.
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex (info : BuildInfo) : IndexBuildM (BuildData info.key) := do
-  match info with
-  | .moduleFacet mod facet =>
-    if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-      config.build mod
+def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
+| .moduleFacet mod facet => do
+  if let some config := (← getWorkspace).findModuleFacetConfig? facet then
+    config.build mod
+  else
+    error s!"do not know how to build module facet `{facet}`"
+| .packageFacet pkg facet => do
+  if let some config := (← getWorkspace).findPackageFacetConfig? facet then
+    config.build pkg
+  else
+    error s!"do not know how to build package facet `{facet}`"
+| .customTarget pkg target =>
+  if let some config := pkg.findTargetConfig? target then
+    if h : pkg.name = config.package ∧ target = config.name then
+      have h' : CustomData (pkg.name, target) = ActiveBuildTarget config.resultType := by simp [h]
+      liftM <| cast (by rw [← h']) <| config.target.activate
     else
-      error s!"do not know how to build module facet `{facet}`"
-  | .packageFacet pkg facet =>
-    if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-      config.build pkg
-    else
-      error s!"do not know how to build package facet `{facet}`"
-  | .customTarget pkg target =>
-    if let some config := pkg.findTargetConfig? target then
-      if h : pkg.name = config.package ∧ target = config.name then
-        have h' : CustomData (pkg.name, target) = ActiveBuildTarget config.resultType := by simp [h]
-        liftM <| cast (by rw [← h']) <| config.target.activate
-      else
-        error "target's name in the configuration does not match the name it was registered with"
-    else
-       error s!"could not build `{target}` of `{pkg.name}` -- target not found"
-  | .staticLeanLib lib =>
-    mkTargetFacetBuild LeanLib.staticFacet lib.recBuildStatic
-  | .sharedLeanLib lib =>
-    mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared
-  | .leanExe exe =>
-    mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
-  | .staticExternLib lib =>
-    mkTargetFacetBuild ExternLib.staticFacet lib.target.activate
-  | .sharedExternLib lib =>
-    mkTargetFacetBuild ExternLib.sharedFacet do
-      let staticTarget := Target.active <| ← lib.static.recBuild
-      staticToLeanDynlibTarget staticTarget |>.activate
+      error "target's name in the configuration does not match the name it was registered with"
+  else
+      error s!"could not build `{target}` of `{pkg.name}` -- target not found"
+| .leanLib lib =>
+  mkTargetFacetBuild LeanLib.leanFacet lib.recBuildLean
+| .staticLeanLib lib =>
+  mkTargetFacetBuild LeanLib.staticFacet lib.recBuildStatic
+| .sharedLeanLib lib =>
+  mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared
+| .leanExe exe =>
+  mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
+| .staticExternLib lib =>
+  mkTargetFacetBuild ExternLib.staticFacet lib.target.activate
+| .sharedExternLib lib =>
+  mkTargetFacetBuild ExternLib.sharedFacet do
+    let staticTarget := Target.active <| ← lib.static.recBuild
+    staticToLeanDynlibTarget staticTarget |>.activate
 
 /--
 Recursively build the given info using the Lake build index

Lake/Build/IndexTargets.lean

@@ -5,9 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Build.Index
 
-open Std System
-open Lean hiding SearchPath
-
 namespace Lake
 
 /-! ## Module Facet Targets -/
@@ -19,22 +16,8 @@ namespace Lake
 
 /-! ## Pure Lean Lib Targets -/
 
-/--
-Build the `extraDepTarget` of a package and its (transitive) dependencies
-and then build the target `facet` of library's modules recursively, constructing
-a single opaque target for the whole build.
--/
-def LeanLib.buildModules (self : LeanLib) (facet : Name)
-[FamilyDef ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
-  let buildMods : BuildM _ := do
-    let mods ← self.getModuleArray
-    let modTargets ← failOnBuildCycle <| ← EStateT.run' BuildStore.empty
-      <| mods.mapM fun mod => buildIndexTop <| mod.facet facet
-    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
-  buildMods.catchFailure fun _ => pure <| failure
-
 @[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
-  Target.opaque <| self.buildModules Module.leanBinFacet
+  self.lean.target
 
 @[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget :=
   self.builtinLib.leanTarget

Lake/Build/Info.lean

@@ -22,6 +22,7 @@ namespace Lake
 inductive BuildInfo
 | moduleFacet (module : Module) (facet : Name)
 | packageFacet (package : Package) (facet : Name)
+| leanLib (lib : LeanLib)
 | staticLeanLib (lib : LeanLib)
 | sharedLeanLib (lib : LeanLib)
 | leanExe (exe : LeanExe)
@@ -44,6 +45,9 @@ abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
 abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
   .customTarget self.name target
 
+abbrev LeanLib.leanBuildKey (self : LeanLib) : BuildKey :=
+  .targetFacet self.pkg.name self.name leanFacet
+
 abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
   .targetFacet self.pkg.name self.name staticFacet
 
@@ -65,6 +69,7 @@ abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
 abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 | moduleFacet m f => m.facetBuildKey f
 | packageFacet p f => p.facetBuildKey f
+| leanLib l => l.leanBuildKey
 | staticLeanLib l => l.staticBuildKey
 | sharedLeanLib l => l.sharedBuildKey
 | leanExe x => x.buildKey
@@ -86,6 +91,10 @@ instance [FamilyDef CustomData (p.name, t) α]
 : FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
   family_key_eq_type := by unfold BuildData; simp
 
+instance [FamilyDef TargetData LeanLib.leanFacet α]
+: FamilyDef BuildData (BuildInfo.key (.leanLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
 instance [FamilyDef TargetData LeanLib.staticFacet α]
 : FamilyDef BuildData (BuildInfo.key (.staticLeanLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
@@ -185,6 +194,10 @@ abbrev Package.extraDep (self : Package) : BuildInfo :=
 abbrev Package.customTarget (target : Name) (self : Package) : BuildInfo :=
   .customTarget self target
 
+/-- Build info of the Lean library's Lean binaries. -/
+abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
+  .leanLib self
+
 /-- Build info of the Lean library's static binary. -/
 abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
   .staticLeanLib self

Lake/Build/Roots.lean

@@ -28,7 +28,13 @@ def LeanLib.recBuildLocalModules
           modSet := modSet.insert mod
   return results
 
-protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
+protected def LeanLib.recBuildLean
+(self : LeanLib) : IndexT RecBuildM ActiveOpaqueTarget := do
+  ActiveTarget.collectOpaqueArray (i := PUnit) <|
+    ← self.recBuildLocalModules #[Module.leanBinFacet]
+
+protected def LeanLib.recBuildStatic
+(self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
   let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
   staticLibTarget self.staticLibFile oTargets |>.activate
 
@@ -38,8 +44,7 @@ protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT RecBuildM ActiveF
 Build and collect the local object files and external libraries
 of a library and its modules' imports.
 -/
-def LeanLib.recBuildLinks
-(facets : Array (ModuleFacet ActiveFileTarget)) (self : LeanLib)
+def LeanLib.recBuildLinks (self : LeanLib)
 : IndexT RecBuildM (Array ActiveFileTarget) := do
   -- Build and collect modules
   let mut pkgs := #[]
@@ -56,7 +61,7 @@ def LeanLib.recBuildLinks
             pkgSet := pkgSet.insert mod.pkg
             pkgs := pkgs.push mod.pkg
         if self.isLocalModule mod.name then
-          for facet in facets do
+          for facet in self.nativeFacets do
             targets := targets.push <| ← recBuild <| mod.facet facet.name
         modSet := modSet.insert mod
   -- Build and collect external library targets
@@ -66,13 +71,15 @@ def LeanLib.recBuildLinks
       targets := targets.push target
   return targets
 
-protected def LeanLib.recBuildShared (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
-  let linkTargets := (← self.recBuildLinks self.nativeFacets).map Target.active
+protected def LeanLib.recBuildShared
+(self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
+  let linkTargets := (← self.recBuildLinks).map Target.active
   leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate
 
 /-! # Build Executable -/
 
-protected def LeanExe.recBuildExe (self : LeanExe) : IndexT RecBuildM ActiveFileTarget := do
+protected def LeanExe.recBuildExe
+(self : LeanExe) : IndexT RecBuildM ActiveFileTarget := do
   let (_, imports) ← self.root.imports.recBuild
   let linkTargets := #[Target.active <| ← self.root.o.recBuild]
   let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do

Lake/Build/TargetTypes.lean

@@ -63,10 +63,10 @@ abbrev ActiveFileTarget := ActiveBuildTarget FilePath
 --------------------------------------------------------------------------------
 
 /-- A `BuildTarget` with no artifact information. -/
-abbrev OpaqueTarget := BuildTarget PUnit
+abbrev OpaqueTarget := BuildTarget Unit
 
 /-- An `ActiveBuildTarget` with no artifact information. -/
-abbrev ActiveOpaqueTarget := ActiveBuildTarget PUnit
+abbrev ActiveOpaqueTarget := ActiveBuildTarget Unit
 
 namespace OpaqueTarget
 

Lake/Config/FacetConfig.lean

@@ -13,7 +13,7 @@ structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type
   /-- The facet's build (function). -/
   build : ι → IndexBuildM (DataFam name)
   /-- Is this facet a buildable target? -/
-  toTarget? : (info : BuildInfo) → BuildData info.key = DataFam name → Option (OpaqueTarget.{0})
+  toTarget? : (info : BuildInfo) → BuildData info.key = DataFam name → Option OpaqueTarget
   deriving Inhabited
 
 protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name

Lake/Config/Package.lean

@@ -70,7 +70,7 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   **DEPRECATED:** Use separate custom `target` declarations instead?
   -/
-  extraDepTarget : Option OpaqueTarget.{0} := none
+  extraDepTarget : Option OpaqueTarget := none
 
   /--
   The optional `PackageFacet` to build on a bare `lake build` of the package.