refactor: build code cleanup / reorg

2022-06-28 01:01:13 -04:00 · 2022-06-28 01:01:13 -04:00 · a4174a560b
commit a4174a560b
parent 0e99494611
11 changed files with 402 additions and 404 deletions
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@ -5,5 +5,5 @@ Authors: Mac Malone
 -/
 import Lake.Build.Monad
 import Lake.Build.Actions
-import Lake.Build.LeanTarget
+import Lake.Build.IndexTargets
 import Lake.Build.Imports
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Module
+import Lake.Build.Index
 import Lake.Config.Workspace

 /-!
@ -36,20 +36,20 @@ as "Lean-only". Otherwise, also build `.c` files.
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
  if imports.isEmpty then
    -- build the package's (and its dependencies') `extraDepTarget`
-    self.buildFacet &`extraDep >>= (·.buildOpaque)
+    self.extraDep.build >>= (·.buildOpaque)
    return #[]
  else
    -- build local imports from list
    let mods := (← getWorkspace).processImportList imports
    let (res, bStore) ← EStateT.run BuildStore.empty <| mods.mapM fun mod =>
      if mod.shouldPrecompile then
-        buildModuleTop mod &`lean.dynlib <&> (·.withoutInfo)
+        buildIndexTop mod.dynlib <&> (·.withoutInfo)
      else if mod.isLeanOnly then
-        buildModuleTop mod &`lean
+        buildIndexTop mod.leanBin
      else
-        buildModuleTop mod &`lean.c <&> (·.withoutInfo)
+        buildIndexTop mod.c <&> (·.withoutInfo)
    let importTargets ← failOnBuildCycle res
-    let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
+    let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet
    let externLibTargets := bStore.collectSharedExternLibs
    importTargets.forM (·.buildOpaque)
    let dynlibs ← dynlibTargets.mapM (·.build)
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@ -3,8 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Module1
-import Lake.Build.LeanTarget1
+import Lake.Build.Roots
+import Lake.Build.Module
 import Lake.Build.Topological
 import Lake.Util.EStateT

@ -81,6 +81,7 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 ## Initial Facet Maps
 -/

+open Module in
 /--
 A module facet name to build function map that contains builders for
 the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
@ -89,28 +90,27 @@ the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
  have : MonadLift BuildM m := ⟨liftM⟩
  ModuleBuildMap.empty (m := m)
  -- Compute unique imports (direct × transitive)
-  |>.insert &`lean.imports (mkModuleFacetBuild (·.recParseImports))
+  |>.insert importFacet (mkModuleFacetBuild (·.recParseImports))
  -- Build module (`.olean` and `.ilean`)
-  |>.insert &`lean (mkModuleFacetBuild (fun mod => do
+  |>.insert binFacet (mkModuleFacetBuild (fun mod => do
    mod.recBuildLean !mod.isLeanOnly
  ))
-  |>.insert &`olean (mkModuleFacetBuild (fun mod => do
+  |>.insert oleanFacet (mkModuleFacetBuild (fun mod => do
    mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.oleanFile)
  ))
-  |>.insert &`ilean (mkModuleFacetBuild (fun mod => do
+  |>.insert ileanFacet (mkModuleFacetBuild (fun mod => do
    mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.ileanFile)
  ))
  -- Build module `.c` (and `.olean` and `.ilean`)
-  |>.insert &`lean.c (mkModuleFacetBuild <| fun mod => do
+  |>.insert cFacet (mkModuleFacetBuild <| fun mod => do
    mod.recBuildLean true <&> (·.withInfo mod.cFile)
  )
  -- Build module `.o`
-  |>.insert &`lean.o (mkModuleFacetBuild <| fun mod => do
-    let cTarget ← mod.recBuildFacet &`lean.c
-    mod.mkOTarget (Target.active cTarget) |>.activate
+  |>.insert oFacet (mkModuleFacetBuild <| fun mod => do
+    mod.mkOTarget (Target.active (← mod.c.recBuild)) |>.activate
  )
  -- Build shared library for `--load-dynlb`
-  |>.insert &`lean.dynlib (mkModuleFacetBuild (·.recBuildDynLib))
+  |>.insert dynlibFacet (mkModuleFacetBuild (·.recBuildDynlib))

 /--
 A package facet name to build function map that contains builders for
@ -125,7 +125,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
    let mut depSet := PackageSet.empty
    for dep in pkg.dependencies do
      if let some depPkg ← findPackage? dep.name then
-        for depDepPkg in (← depPkg.recBuildFacet &`deps) do
+        for depDepPkg in (← recBuild <| depPkg.facet &`deps) do
          unless depSet.contains depDepPkg do
            deps := deps.push depDepPkg
            depSet := depSet.insert depDepPkg
@ -139,8 +139,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
    let mut target := ActiveTarget.nil
    for dep in pkg.dependencies do
      if let some depPkg ← findPackage? dep.name then
-        let extraDepTarget ← depPkg.recBuildFacet &`extraDep
-        target ← target.mixOpaqueAsync extraDepTarget
+        target ← target.mixOpaqueAsync (← depPkg.extraDep.recBuild)
    target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
  )
 /-!
@ -162,15 +161,17 @@ the initial set of Lake package facets (e.g., `extraDep`).
    else
      error s!"do not know how to build package facet `{facet}`"
  | .staticLeanLib lib =>
-    mkTargetBuild &`leanLib.static lib.recBuildStatic
+    mkTargetBuild LeanLib.staticFacet lib.recBuildStatic
  | .sharedLeanLib lib =>
-    mkTargetBuild &`leanLib.shared lib.recBuildShared
+    mkTargetBuild LeanLib.sharedFacet lib.recBuildShared
  | .leanExe exe =>
-    mkTargetBuild &`leanExe exe.recBuild
+    mkTargetBuild LeanExe.facet exe.recBuild
  | .staticExternLib lib =>
-    mkTargetBuild &`externLib.static <| lib.target.activate
+    mkTargetBuild ExternLib.staticFacet lib.target.activate
  | .sharedExternLib lib =>
-    mkTargetBuild &`externLib.shared <| staticToLeanDynlibTarget (lib.target) |>.activate
+    mkTargetBuild ExternLib.sharedFacet do
+      let staticTarget := Target.active <| ← lib.static.recBuild
+      staticToLeanDynlibTarget staticTarget |>.activate
  | _ =>
    error s!"do not know how to build `{info.key}`"

@ -178,32 +179,31 @@ the initial set of Lake package facets (e.g., `extraDep`).
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler.
 -/
-@[specialize] def buildIndexTop (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
+@[specialize] def buildIndexTop' (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
  buildDTop BuildData BuildInfo.key recBuildIndex info

 /--
-Build the package's specified facet recursively using a topological-based
-scheduler, storing the results in the monad's store and returning the result
-of the top-level build.
+Recursively build the given info using the Lake build index
+and a topological / suspending scheduler and return the dynamic result.
 -/
-@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
-[h : DynamicType PackageData facet α] : CycleT BuildKey m α  :=
-  have of_data := by
-    unfold BuildData, BuildInfo.key, Package.mkBuildKey
-    simp [h.eq_dynamic_type]
-  cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
+@[inline] def buildIndexTop (info : BuildInfo)
+[h : DynamicType BuildData info.key α] : CycleT BuildKey m α := do
+  cast (by simp [h.eq_dynamic_type]) <| buildIndexTop' (m := m) info

 end

-/-!
-## Package Facet Builders
-/
+/- Build the given Lake target using the given Lake build store. -/
+@[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo)
+[DynamicType BuildData self.key α] : BuildM α := do
+  failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self

-/--
-Recursively build the specified facet of the given package,
-returning the result.
-/
-def Package.buildFacet (self : Package) (facet : WfName)
-[DynamicType PackageData facet α] : BuildM α := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    buildPackageTop self facet
+/- Build the given Lake target in a fresh build store. -/
+@[inline] def BuildInfo.build (self : BuildInfo) [DynamicType BuildData self.key α] : BuildM α :=
+  buildIn BuildStore.empty self
+
+export BuildInfo (build buildIn)
+
+/-- An opaque target that builds the Lake target in a fresh build store. -/
+@[inline] def BuildInfo.target (self : BuildInfo)
+[DynamicType BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
+  BuildTarget.mk' () <| self.build <&> (·.task)
--- a/Lake/Build/IndexTargets.lean
+++ b/Lake/Build/IndexTargets.lean
@ -0,0 +1,76 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Index
+
+open Std System
+open Lean hiding SearchPath
+
+namespace Lake
+
+-- # Module Facet Targets
+
+@[inline] def Module.facetTarget (facet : WfName) (self : Module)
+[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
+  self.facet facet |>.target
+
+@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
+  self.facetTarget oleanFacet |>.withInfo self.oleanFile
+
+@[inline] def Module.ileanTarget (self : Module) : FileTarget :=
+  self.facetTarget ileanFacet |>.withInfo self.ileanFile
+
+@[inline] def Module.cTarget (self : Module) : FileTarget :=
+  self.facetTarget cFacet |>.withInfo self.cFile
+
+@[inline] def Module.oTarget (self : Module) : FileTarget :=
+  self.facetTarget oFacet |>.withInfo self.oFile
+
+-- # 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 : WfName)
+[DynamicType 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 <| BuildInfo.module mod facet
+    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
+  buildMods.catchFailure fun _ => pure <| failure
+
+@[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
+  Target.opaque <| self.buildModules Module.binFacet
+
+@[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget :=
+  self.builtinLib.leanTarget
+
+-- # Native Lean Lib Targets
+
+@[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
+  self.static.target.withInfo self.sharedLibFile
+
+@[inline] protected def Package.staticLibTarget (self : Package) : FileTarget :=
+  self.builtinLib.staticLibTarget
+
+@[inline] protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
+  self.shared.target.withInfo self.sharedLibFile
+
+@[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget :=
+  self.builtinLib.sharedLibTarget
+
+-- # Lean Executable Targets
+
+@[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget :=
+  self.info.build
+
+@[inline] protected def LeanExe.target (self : LeanExe) : FileTarget :=
+  self.info.target.withInfo self.file
+
+@[inline] protected def Package.exeTarget (self : Package) : FileTarget :=
+  self.builtinExe.target
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@ -10,28 +10,34 @@ import Lake.Util.EquipT

 namespace Lake

-- # Build Key Constructor Helpers
+-- # Build Key Helper Constructors

-@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
+abbrev Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
  ⟨⟨none, self.name, facet⟩, rfl, rfl⟩

-@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
+abbrev Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
  ⟨⟨self.name, none, facet⟩, rfl, rfl⟩

+abbrev LeanLib.staticFacet := &`leanLib.static
+abbrev LeanLib.sharedFacet := &`leanLib.shared
+abbrev LeanExe.facet := &`leanExe
+abbrev ExternLib.staticFacet := &`externLib.static
+abbrev ExternLib.sharedFacet := &`externLib.shared
+
 abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
-  ⟨self.pkg.name, self.name, &`leanLib.static⟩
+  ⟨self.pkg.name, self.name, staticFacet⟩

 abbrev LeanLib.sharedBuildKey (self : LeanLib) : BuildKey :=
-  ⟨self.pkg.name, self.name, &`leanLib.shared⟩
+  ⟨self.pkg.name, self.name, sharedFacet⟩

 abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
-  ⟨self.pkg.name, self.name, &`leanExe⟩
+  ⟨self.pkg.name, self.name, facet⟩

 abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
-  ⟨self.pkg.name, self.name, &`externLib.static⟩
+  ⟨self.pkg.name, self.name, staticFacet⟩

 abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
-  ⟨self.pkg.name, self.name, &`externLib.shared⟩
+  ⟨self.pkg.name, self.name, sharedFacet⟩

 -- # Build Info

@ -44,9 +50,9 @@ inductive BuildInfo
 | leanExe (exe : LeanExe)
 | staticExternLib (lib : ExternLib)
 | sharedExternLib (lib : ExternLib)
-| target (package : Package) (target : WfName) (facet : WfName)
+| custom (package : Package) (target : WfName) (facet : WfName)

-def BuildInfo.key : (self : BuildInfo) → BuildKey
+abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 | module m f => m.mkBuildKey f
 | package p f => p.mkBuildKey f
 | staticLeanLib l => l.staticBuildKey
@ -54,7 +60,39 @@ def BuildInfo.key : (self : BuildInfo) → BuildKey
 | leanExe x => x.buildKey
 | staticExternLib l => l.staticBuildKey
 | sharedExternLib l => l.sharedBuildKey
-| target p t f => ⟨p.name, t, f⟩
+| custom p t f => ⟨p.name, t, f⟩
+
+-- # Instances for deducing data types of `BuildInfo` keys
+
+instance [DynamicType ModuleData f α]
+: DynamicType BuildData (BuildInfo.key (.module m f)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType PackageData f α]
+: DynamicType BuildData (BuildInfo.key (.package p f)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType TargetData LeanLib.staticFacet α]
+: DynamicType BuildData (BuildInfo.key (.staticLeanLib l)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType TargetData LeanLib.sharedFacet α]
+: DynamicType BuildData (BuildInfo.key (.sharedLeanLib l)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType TargetData LeanExe.facet α]
+: DynamicType BuildData (BuildInfo.key (.leanExe x)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType TargetData ExternLib.staticFacet α]
+: DynamicType BuildData (BuildInfo.key (.staticExternLib l)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+instance [DynamicType TargetData ExternLib.sharedFacet α]
+: DynamicType BuildData (BuildInfo.key (.sharedExternLib l)) α where
+  eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type]
+
+-- # Recursive Facet Builds

 /-- A build function for any element of the Lake build index. -/
 abbrev IndexBuildFn (m : Type → Type v) :=
@ -64,36 +102,74 @@ abbrev IndexBuildFn (m : Type → Type v) :=
 /-- A transformer to equip a monad with a build function for the Lake index. -/
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m

-@[inline] def Module.recBuildFacet (self : Module) (facet : WfName)
-[DynamicType ModuleData facet α] : IndexT m α := fun build =>
-  let to_data := by
-    unfold BuildData, BuildInfo.key, Module.mkBuildKey
-    simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.module self facet
+/-- Build the given info using the Lake build index. -/
+@[inline] def BuildInfo.recBuild (self : BuildInfo) [DynamicType BuildData self.key α] : IndexT m α :=
+  fun build => cast (by simp [eq_dynamic_type]) <| build self

-@[inline] def Package.recBuildFacet (self : Package) (facet : WfName)
-[DynamicType PackageData facet α] : IndexT m α := fun build =>
-  let to_data := by
-    unfold BuildData, BuildInfo.key, Package.mkBuildKey
-    simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.package self facet
+export BuildInfo (recBuild)

-@[inline] def ExternLib.recBuildStatic (self : ExternLib)
-[DynamicType TargetData &`externLib.static α] : IndexT m α := fun build =>
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.staticExternLib self
+-- # Build Info Helper Constructors

-@[inline] def ExternLib.recBuildShared (self : ExternLib)
-[DynamicType TargetData &`externLib.shared α] : IndexT m α := fun build =>
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.sharedExternLib self
+namespace Module
+
+/-- Build info for the module's specified facet. -/
+abbrev facet (facet : WfName) (self : Module) : BuildInfo :=
+  .module self facet
+
+abbrev importFacet   := &`lean.imports
+abbrev binFacet      := &`lean.bin
+abbrev oleanFacet    := &`olean
+abbrev ileanFacet    := &`ilean
+abbrev cFacet        := &`lean.c
+abbrev oFacet        := &`lean.o
+abbrev dynlibFacet   := &`lean.dynlib
+
+variable (self : Module)
+
+abbrev imports  := self.facet importFacet
+abbrev leanBin  := self.facet binFacet
+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
+
+/-- Build info for the package's specified facet. -/
+abbrev Package.facet (facet : WfName) (self : Package) : BuildInfo :=
+  .package self facet
+
+/-- Build info for the package's `extraDepTarget`. -/
+abbrev Package.extraDep (self : Package) : BuildInfo :=
+  self.facet &`extraDep
+
+/-- Build info of the Lean library's static binary. -/
+abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
+  .staticLeanLib self
+
+/-- Build info of the Lean library's shared binary. -/
+abbrev LeanLib.shared (self : LeanLib) : BuildInfo :=
+  .sharedLeanLib self
+
+/-- Build info of the Lean executable. -/
+abbrev LeanExe.info (self : LeanExe) : BuildInfo :=
+  .leanExe self
+
+/-- Build info of the external library's static binary. -/
+abbrev ExternLib.static (self : ExternLib) : BuildInfo :=
+  .staticExternLib self
+
+/-- Build info of the external library's shared binary. -/
+abbrev ExternLib.shared (self : ExternLib) : BuildInfo :=
+  .sharedExternLib self

 -- # Data Types of Build Results

 -- ## For Module Facets

 /-- Lean binary build (`olean`, `ilean` files) -/
-module_data lean : ActiveOpaqueTarget
+module_data lean.bin : ActiveOpaqueTarget

 /-- The `olean` file produced by `lean`  -/
 module_data olean : ActiveFileTarget
--- a/Lake/Build/LeanTarget.lean
+++ b/Lake/Build/LeanTarget.lean
@ -1,71 +0,0 @@
-/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
-/
-import Lake.Build.Module
-
-open Std System
-open Lean hiding SearchPath
-
-namespace Lake
-
-- # Build Lean Lib
-
-/--
-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 : WfName)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
-  let buildMods : BuildM _ := do
-    let mods ← self.getModuleArray
-    let modTargets ← buildModuleFacetArray mods facet
-    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
-  buildMods.catchFailure fun _ => pure <| failure
-
-def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
-  Target.opaque <| self.buildModules &`lean
-
-def Package.libTarget (self : Package) : OpaqueTarget :=
-  self.builtinLib.leanTarget
-
-- # Build Static Lib
-
-def LeanLib.buildStatic (self : LeanLib) : BuildM ActiveFileTarget := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
-    cast of_data <| buildIndexTop <| BuildInfo.staticLeanLib self
-
-protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
-  BuildTarget.mk' self.staticLibFile do self.buildStatic <&> (·.task)
-
-protected def Package.staticLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.staticLibTarget
-
-- # Build Shared Lib
-
-def LeanLib.buildShared (self : LeanLib) : BuildM ActiveFileTarget := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
-    cast of_data <| buildIndexTop <| BuildInfo.sharedLeanLib self
-
-protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
-  BuildTarget.mk' self.sharedLibFile do self.buildShared <&> (·.task)
-
-protected def Package.sharedLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.sharedLibTarget
-
-- # Build Executable
-
-def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
-    cast of_data <| buildIndexTop <| BuildInfo.leanExe self
-
-def LeanExe.target (self : LeanExe) : FileTarget :=
-  BuildTarget.mk' self.file do self.build <&> (·.task)
-
-protected def Package.exeTarget (self : Package) : FileTarget :=
-  self.builtinExe.target
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@ -1,87 +1,162 @@
 /-
-Copyright (c) 2022 Mac Malone. All rights reserved.
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
+Authors: Sebastian Ullrich, Mac Malone
 -/
-import Lake.Build.Index
+import Lean.Elab.Import
+import Lake.Build.Info
+import Lake.Build.Store
+import Lake.Build.Targets
+
+open System

-open Std Lean
 namespace Lake

-- # Index Recursive Build
+-- # Solo Module Targets
+
+def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
+(dynlibPath : SearchPath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
+  Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
+    let argTrace : BuildTrace := pureHash mod.leanArgs
+    let srcTrace : BuildTrace ← computeTrace mod.leanFile
+    let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
+    let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
+    if c then
+      let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
+      unless modUpToDate && cUpToDate do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
+          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+      modTrace.writeToFile mod.cTraceFile
+    else
+      unless modUpToDate do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
+          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+    modTrace.writeToFile mod.traceFile
+    return depTrace
+
+def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget :=
+  Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ =>
+    return mixTrace (← computeTrace self.cFile) (← getLeanTrace)
+
+@[inline]
+def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget :=
+  leanOFileTarget self.oFile cTarget self.leancArgs
+
+@[inline]
+def Module.mkDynlibTarget (self : Module) (oTarget : FileTarget)
+(libDirs : Array FilePath) (libTargets : Array FileTarget) : FileTarget :=
+  let libsTarget : BuildTarget _ := Target.collectArray libTargets
+  Target.mk self.dynlibName do
+    oTarget.bindAsync fun oFile oTrace => do
+    libsTarget.bindSync fun libFiles libTrace => do
+      buildFileUnlessUpToDate self.dynlibFile (oTrace.mix libTrace) do
+        let args := #[oFile.toString] ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}")
+        compileSharedLib self.dynlibFile args (← getLeanc)
+
+-- # Recursive Building

 section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]

-/--
-Build the module's specified facet recursively using a topological-based
-scheduler, storing the results in the monad's store and returning the result
-of the top-level build.
-/
-@[inline] def buildModuleTop (mod : Module) (facet : WfName)
-[h : DynamicType ModuleData facet α] : CycleT BuildKey m α  :=
-  have of_data := by
-    unfold BuildData, BuildInfo.key, Module.mkBuildKey
-    simp [h.eq_dynamic_type]
-  cast of_data <| buildIndexTop (m := m) <| BuildInfo.module mod facet
+/-- Build the dynlibs of the imports that want precompilation. -/
+@[specialize] def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
+: IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  -- Build and collect precompiled imports
+  let mut pkgs := #[]
+  let mut pkgSet := PackageSet.empty.insert pkg
+  let mut modTargets := #[]
+  for imp in imports do
+    if imp.shouldPrecompile then
+      unless pkgSet.contains imp.pkg do
+        pkgSet := pkgSet.insert imp.pkg
+        pkgs := pkgs.push imp.pkg
+      modTargets := modTargets.push <| ← imp.dynlib.recBuild
+  pkgs := pkgs.push pkg
+  -- Compute library directories and external library targets
+  let mut libDirs := #[]
+  let mut pkgTargets := #[]
+  for pkg in pkgs do
+    libDirs := libDirs.push pkg.libDir
+    let externLibTargets ← pkg.externLibs.mapM (·.shared.recBuild)
+    for target in externLibTargets do
+      if let some parent := target.info.parent then
+        libDirs := libDirs.push parent
+      if let some stem := target.info.fileStem then
+        if stem.startsWith "lib" then
+          pkgTargets := pkgTargets.push <| target.withInfo <| stem.drop 3
+        else
+          logWarning s!"external library `{target.info}` was skipped because it does not start with `lib`"
+      else
+        logWarning s!"external library `{target.info}` was skipped because it has no file name"
+  return (modTargets, pkgTargets, libDirs)

 /--
-Build the module's specified facet recursively using a topological-based
-scheduler, storing the results in the monad's store and returning nothing.
+Recursively build a module and its (transitive, local) imports,
+optionally outputting a `.c` file as well if `c` is set to `true`.
 -/
-@[inline] def buildModuleTop' (mod : Module) (facet : WfName) : CycleT BuildKey m PUnit :=
-  discard <| buildIndexTop (m := m) <| BuildInfo.module mod facet
-
-end
-
-- # Module Facet Builders
+@[specialize] def Module.recBuildLean (mod : Module) (c : Bool)
+: IndexT m ActiveOpaqueTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let extraDepTarget ← mod.pkg.extraDep.recBuild
+  let (imports, transImports) ← mod.imports.recBuild
+  let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
+   -- Note: Lean wants the external library symbols before module symbols
+  let dynlibsTarget ← ActiveTarget.collectArray <| pkgTargets ++ modTargets
+  let importTarget ←
+    if c then
+      ActiveTarget.collectOpaqueArray
+        <| ← imports.mapM (·.c.recBuild)
+    else
+      ActiveTarget.collectOpaqueArray
+        <| ← imports.mapM (·.leanBin.recBuild)
+  let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
+    <| ← dynlibsTarget.mixOpaqueAsync importTarget
+  let dynlibs := dynlibsTarget.info.map (FilePath.mk s!"lib{·}.{sharedLibExt}")
+  let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget c |>.activate
+  store mod.leanBin.key modTarget
+  store mod.olean.key <| modTarget.withInfo mod.oleanFile
+  store mod.ilean.key <| modTarget.withInfo mod.ileanFile
+  if c then
+    let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
+    store mod.c.key cTarget
+    return cTarget.withoutInfo
+  else
+    return modTarget

 /--
-Recursively build the specified facet of the given module,
-returning the result.
+Recursively parse the Lean files of a module and its imports
+building an `Array` product of its direct and transitive local imports.
 -/
-def buildModuleFacet
-(mod : Module) (facet : WfName)
-[DynamicType ModuleData facet α] : BuildM α := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    buildModuleTop mod facet
+@[specialize] def Module.recParseImports (mod : Module)
+: IndexT m (Array Module × Array Module) := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let mut transImports := #[]
+  let mut directImports := #[]
+  let mut importSet := ModuleSet.empty
+  let contents ← IO.FS.readFile mod.leanFile
+  let (imports, _, _) ← Lean.Elab.parseImports contents mod.leanFile.toString
+  for imp in imports do
+    if let some mod ← findModule? imp.module then
+      let (_, impTransImports) ← mod.imports.recBuild
+      for transImp in impTransImports do
+        unless importSet.contains transImp do
+          importSet := importSet.insert transImp
+          transImports := transImports.push transImp
+      unless importSet.contains mod do
+        importSet := importSet.insert mod
+        transImports := transImports.push mod
+      directImports := directImports.push mod
+  return (directImports, transImports)

 /--
-Recursively build the specified facet of each module,
-returning an `Array`  of the results.
+Recursively build the shared library of a module (e.g., for `--load-dynlib`).
 -/
-def buildModuleFacetArray
-(mods : Array Module) (facet : WfName)
-[DynamicType ModuleData facet α] : BuildM (Array α) := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty <| mods.mapM fun mod =>
-    buildModuleTop mod facet
-
-/--
-Recursively build the specified facet of the given module,
-returning the resulting map of built modules and their results.
-/
-def buildModuleFacetMap
-(mods : Array Module) (facet : WfName)
-[DynamicType ModuleData facet α] : BuildM (NameMap α) := do
-  let (x, bStore) ← EStateT.run BuildStore.empty <| mods.forM fun mod =>
-    buildModuleTop' mod facet
-  failOnBuildCycle x
-  return bStore.collectModuleFacetMap facet
-
-- # Module Facet Targets
-
-def Module.facetTarget (facet : WfName) (self : Module)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
-  BuildTarget.mk' () do return (← buildModuleFacet self facet).task
-
-@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
-  self.facetTarget &`lean |>.withInfo self.oleanFile
-
-@[inline] def Module.ileanTarget (self : Module) : FileTarget :=
-  self.facetTarget &`lean  |>.withInfo self.ileanFile
-
-@[inline] def Module.cTarget (self : Module) : FileTarget :=
-  self.facetTarget &`lean.c |>.withInfo self.cFile
-
-@[inline] def Module.oTarget (self : Module) : FileTarget :=
-  self.facetTarget &`lean.o |>.withInfo self.oFile
+@[specialize] def Module.recBuildDynlib (mod : Module)
+: IndexT m ActiveFileTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let (_, transImports) ← mod.imports.recBuild
+  let oTarget := Target.active (← mod.o.recBuild)
+  let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
+  let libTargets := modTargets ++ pkgTargets |>.map Target.active
+  mod.mkDynlibTarget oTarget libDirs libTargets |>.activate
--- a/Lake/Build/Module1.lean
+++ b/Lake/Build/Module1.lean
@ -1,162 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Mac Malone
-/
-import Lean.Elab.Import
-import Lake.Build.Info
-import Lake.Build.Store
-import Lake.Build.Targets
-
-open System
-
-namespace Lake
-
-- # Solo Module Targets
-
-def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
-(dynlibPath : SearchPath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
-  Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
-    let argTrace : BuildTrace := pureHash mod.leanArgs
-    let srcTrace : BuildTrace ← computeTrace mod.leanFile
-    let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-    let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
-    if c then
-      let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
-      unless modUpToDate && cUpToDate do
-        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
-          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
-      modTrace.writeToFile mod.cTraceFile
-    else
-      unless modUpToDate do
-        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
-          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
-    modTrace.writeToFile mod.traceFile
-    return depTrace
-
-def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget :=
-  Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ =>
-    return mixTrace (← computeTrace self.cFile) (← getLeanTrace)
-
-@[inline]
-def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget :=
-  leanOFileTarget self.oFile cTarget self.leancArgs
-
-@[inline]
-def Module.mkDynlibTarget (self : Module) (oTarget : FileTarget)
-(libDirs : Array FilePath) (libTargets : Array FileTarget) : FileTarget :=
-  let libsTarget : BuildTarget _ := Target.collectArray libTargets
-  Target.mk self.dynlib do
-    oTarget.bindAsync fun oFile oTrace => do
-    libsTarget.bindSync fun libFiles libTrace => do
-      buildFileUnlessUpToDate self.dynlibFile (oTrace.mix libTrace) do
-        let args := #[oFile.toString] ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}")
-        compileSharedLib self.dynlibFile args (← getLeanc)
-
-- # Recursive Building
-
-section
-variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
-
-/-- Build the dynlibs of the imports that want precompilation. -/
-@[specialize] def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
-: IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  -- Build and collect precompiled imports
-  let mut pkgs := #[]
-  let mut pkgSet := PackageSet.empty.insert pkg
-  let mut modTargets := #[]
-  for imp in imports do
-    if imp.shouldPrecompile then
-      unless pkgSet.contains imp.pkg do
-        pkgSet := pkgSet.insert imp.pkg
-        pkgs := pkgs.push imp.pkg
-      modTargets := modTargets.push <| ← imp.recBuildFacet &`lean.dynlib
-  pkgs := pkgs.push pkg
-  -- Compute library directories and external library targets
-  let mut libDirs := #[]
-  let mut pkgTargets := #[]
-  for pkg in pkgs do
-    libDirs := libDirs.push pkg.libDir
-    let externLibTargets ← pkg.externLibs.mapM (·.recBuildShared)
-    for target in externLibTargets do
-      if let some parent := target.info.parent then
-        libDirs := libDirs.push parent
-      if let some stem := target.info.fileStem then
-        if stem.startsWith "lib" then
-          pkgTargets := pkgTargets.push <| target.withInfo <| stem.drop 3
-        else
-          logWarning s!"external library `{target.info}` was skipped because it does not start with `lib`"
-      else
-        logWarning s!"external library `{target.info}` was skipped because it has no file name"
-  return (modTargets, pkgTargets, libDirs)
-
-/--
-Recursively build a module and its (transitive, local) imports,
-optionally outputting a `.c` file as well if `c` is set to `true`.
-/
-@[specialize] def Module.recBuildLean (mod : Module) (c : Bool)
-: IndexT m ActiveOpaqueTarget := do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep
-  let (imports, transImports) ← mod.recBuildFacet &`lean.imports
-  let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
-   -- Note: Lean wants the external library symbols before module symbols
-  let dynlibsTarget ← ActiveTarget.collectArray <| pkgTargets ++ modTargets
-  let importTarget ←
-    if c then
-      ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (·.recBuildFacet &`lean.c)
-    else
-      ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (·.recBuildFacet &`lean)
-  let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
-    <| ← dynlibsTarget.mixOpaqueAsync importTarget
-  let dynlibs := dynlibsTarget.info.map (FilePath.mk s!"lib{·}.{sharedLibExt}")
-  let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget c |>.activate
-  store (mod.mkBuildKey &`lean) modTarget
-  store (mod.mkBuildKey &`olean) <| modTarget.withInfo mod.oleanFile
-  store (mod.mkBuildKey &`ilean) <| modTarget.withInfo mod.ileanFile
-  if c then
-    let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
-    store (mod.mkBuildKey &`lean.c) cTarget
-    return cTarget.withoutInfo
-  else
-    return modTarget
-
-/--
-Recursively parse the Lean files of a module and its imports
-building an `Array` product of its direct and transitive local imports.
-/
-@[specialize] def Module.recParseImports (mod : Module)
-: IndexT m (Array Module × Array Module) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  let mut transImports := #[]
-  let mut directImports := #[]
-  let mut importSet := ModuleSet.empty
-  let contents ← IO.FS.readFile mod.leanFile
-  let (imports, _, _) ← Lean.Elab.parseImports contents mod.leanFile.toString
-  for imp in imports do
-    if let some mod ← findModule? imp.module then
-      let (_, impTransImports) ← mod.recBuildFacet &`lean.imports
-      for transImp in impTransImports do
-        unless importSet.contains transImp do
-          importSet := importSet.insert transImp
-          transImports := transImports.push transImp
-      unless importSet.contains mod do
-        importSet := importSet.insert mod
-        transImports := transImports.push mod
-      directImports := directImports.push mod
-  return (directImports, transImports)
-
-/--
-Recursively build the shared library of a module (e.g., for `--load-dynlib`).
-/
-@[specialize] def Module.recBuildDynLib (mod : Module)
-: IndexT m ActiveFileTarget := do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  let oTarget := Target.active <| ← mod.recBuildFacet &`lean.o
-  let (_, transImports) ← mod.recBuildFacet &`lean.imports
-  let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
-  let libTargets := modTargets ++ pkgTargets |>.map Target.active
-  mod.mkDynlibTarget oTarget libDirs libTargets |>.activate
--- a/Lake/Build/LeanTarget1.lean
+++ b/Lake/Build/LeanTarget1.lean
@ -14,24 +14,25 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 -- # Build Static Lib

 /-- Build a library and its imports and collect its local modules' o files. -/
-@[specialize] def LeanLib.recBuildOFiles
-(self : LeanLib) (mods : Array Module) : IndexT m (Array ActiveFileTarget) := do
+@[specialize] def LeanLib.recBuildOFiles (self : LeanLib) : IndexT m (Array ActiveFileTarget) := do
  have : MonadLift BuildM m := ⟨liftM⟩
  let mut targets := #[]
  let mut modSet := ModuleSet.empty
+  let mods ← self.getModuleArray
  for mod in mods do
-    let (_, mods) ← mod.recBuildFacet &`lean.imports
+    let (_, mods) ← mod.imports.recBuild
    let mods := mods.push mod
    for mod in mods do
      unless modSet.contains mod do
        if self.isLocalModule mod.name then
-          targets := targets.push <| ← mod.recBuildFacet &`lean.o
+          targets := targets.push <| ← mod.o.recBuild
        modSet := modSet.insert mod
  return targets

+@[specialize]
 protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do
  have : MonadLift BuildM m := ⟨liftM⟩
-  let oTargets := (← self.recBuildOFiles (← self.getModuleArray)).map Target.active
+  let oTargets := (← self.recBuildOFiles).map Target.active
  staticLibTarget self.staticLibFile oTargets |>.activate

 -- # Build Shared Lib
@ -46,7 +47,7 @@ protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarge
  let mut modSet := ModuleSet.empty
  let mut targets := #[]
  for mod in mods do
-    let (_, mods) ← mod.recBuildFacet &`lean.imports
+    let (_, mods) ← mod.imports.recBuild
    let mods := mods.push mod
    for mod in mods do
      unless modSet.contains mod do
@ -54,15 +55,16 @@ protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarge
            pkgSet := pkgSet.insert mod.pkg
            pkgs := pkgs.push mod.pkg
        if self.isLocalModule mod.name then
-          targets := targets.push <| ← mod.recBuildFacet &`lean.o
+          targets := targets.push <| ← mod.o.recBuild
        modSet := modSet.insert mod
  -- Build and collect external library targets
  for pkg in pkgs do
-    let externLibTargets ← pkg.externLibs.mapM (·.recBuildShared)
+    let externLibTargets ← pkg.externLibs.mapM (·.shared.recBuild)
    for target in externLibTargets do
      targets := targets.push target
  return targets

+@[specialize]
 protected def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do
  have : MonadLift BuildM m := ⟨liftM⟩
  let linkTargets := (← self.recBuildLinks (← self.getModuleArray)).map Target.active
@ -70,13 +72,14 @@ protected def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarge

 -- # Build Executable

+@[specialize] protected
 def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
  have : MonadLift BuildM m := ⟨liftM⟩
-  let linkTargets := #[Target.active <| ← self.root.recBuildFacet &`lean.o]
-  let (_, imports) ← self.root.recBuildFacet &`lean.imports
-  let mut linkTargets ← imports.foldlM (init := linkTargets) fun a m => do
-    return a.push <| Target.active <| ← m.recBuildFacet &`lean.o
-  let deps := (← self.pkg.recBuildFacet &`deps).push self.pkg
+  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
+    return arr.push <| Target.active <| ← mod.o.recBuild
+  let deps := (← recBuild <| self.pkg.facet &`deps).push self.pkg
  for dep in deps do for lib in dep.externLibs do
-    linkTargets := linkTargets.push <| Target.active <| ← lib.recBuildStatic
+    linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
  leanExeTarget self.file linkTargets self.linkArgs |>.activate
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@ -13,7 +13,7 @@ def Package.defaultTarget (self : Package) : OpaqueTarget :=
  | .exe | .bin => self.exeTarget.withoutInfo
  | .staticLib => self.staticLibTarget.withoutInfo
  | .sharedLib => self.sharedLibTarget.withoutInfo
-  | .leanLib | .oleans => self.libTarget.withoutInfo
+  | .leanLib | .oleans => self.leanLibTarget.withoutInfo
  | .none => Target.nil

 def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package :=
@ -24,19 +24,20 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
    | some pkg => return pkg
    | none => throw <| CliError.unknownPackage spec

+open Module in
 def resolveModuleTarget (mod : Module) (facet : String) : Except CliError OpaqueTarget :=
  if facet.isEmpty || facet == "bin"  then
-    return mod.facetTarget &`lean
+    return mod.facetTarget binFacet
  else if facet == "ilean" then
-    return mod.facetTarget &`ilean
+    return mod.facetTarget ileanFacet
  else if facet == "olean" then
-    return mod.facetTarget &`olean
+    return mod.facetTarget oleanFacet
  else if facet == "c" then
-    return mod.facetTarget &`lean.c
+    return mod.facetTarget cFacet
  else if facet == "o" then
-    return mod.facetTarget &`lean.o
+    return mod.facetTarget oFacet
  else if facet == "dynlib" then
-    return mod.facetTarget &`lean.dynlib
+    return mod.facetTarget dynlibFacet
  else
    throw <| CliError.unknownFacet "module" facet

@ -88,7 +89,7 @@ def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError Opaq
  else if facet == "sharedLib" then
    return pkg.sharedLibTarget.withoutInfo
  else if facet == "leanLib" || facet == "oleans" then
-    return pkg.libTarget.withoutInfo
+    return pkg.leanLibTarget.withoutInfo
  else
    throw <| CliError.unknownFacet "package" facet

--- a/Lake/Config/Module.lean
+++ b/Lake/Config/Module.lean
@ -59,12 +59,12 @@ abbrev pkg (self : Module) : Package :=
@[inline] def oFile (self : Module) : FilePath :=
  Lean.modToFilePath self.pkg.irDir self.name "o"

-@[inline] def dynlib (self : Module) : FilePath :=
+@[inline] def dynlibName (self : Module) : FilePath :=
  -- NOTE: file name MUST be unique on Windows
  self.name.toStringWithSep "-"

@[inline] def dynlibFile (self : Module) : FilePath :=
-  self.pkg.libDir / s!"lib{self.dynlib}.{sharedLibExt}"
+  self.pkg.libDir / s!"lib{self.dynlibName}.{sharedLibExt}"

@[inline] def leanArgs (self : Module) : Array String :=
  self.lib.leanArgs