refactor: simplify FacetConifg and build monads ala leanprover/lake#107

closes leanprover/lake#107
2022-07-23 19:39:47 -04:00 · 2022-07-23 19:39:47 -04:00 · d68029092a
commit d68029092a
parent 1256453ad5
17 changed files with 227 additions and 300 deletions
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@ -6,4 +6,6 @@ Authors: Mac Malone
 import Lake.Build.Monad
 import Lake.Build.Actions
 import Lake.Build.IndexTargets
+import Lake.Build.Module
+import Lake.Build.Package
 import Lake.Build.Imports
--- a/Lake/Build/Context.lean
+++ b/Lake/Build/Context.lean
@ -9,6 +9,8 @@ import Lake.Util.Error
 import Lake.Util.OptionIO
 import Lake.Config.Context
 import Lake.Build.Trace
+import Lake.Build.Store
+import Lake.Build.Topological

 open System
 namespace Lake
@ -29,9 +31,18 @@ abbrev BuildT := ReaderT BuildContext
 /-- The monad for the Lake build manager. -/
 abbrev SchedulerM := BuildT <| LogT BaseIO

-/-- The monad for Lake builds. -/
+/-- The core monad for Lake builds. -/
 abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO

+/-- A transformer to equip a monad with a Lake build store. -/
+abbrev BuildStoreT := StateT BuildStore
+
+/-- A transformer for monads that may encounter a build cycle. -/
+abbrev BuildCycleT := CycleT BuildKey
+
+/-- A recursive build of a Lake build store that may encounter a cycle. -/
+abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
+
 instance : MonadError BuildM := ⟨MonadLog.error⟩
 instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩

--- a/Lake/Build/Facets.lean
+++ b/Lake/Build/Facets.lean
@ -11,7 +11,7 @@ import Lake.Build.TargetTypes

 This module declares most of the builtin facets an targets and
 their build data builtin facets and targets. Some of these definitions
-are needed for  configurations, so we define them here before we need to
+are needed for configurations, so we define them here before we need to
 import said configurations for `BuildInfo`.
 -/

@ -33,62 +33,59 @@ instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
 instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
  ⟨facet, family_key_eq_type⟩

-namespace Module
-abbrev leanBinFacet  := `lean.bin
-abbrev oleanFacet    := `olean
-abbrev ileanFacet    := `ilean
-abbrev cFacet        := `lean.c
-abbrev oFacet        := `lean.o
-abbrev dynlibFacet   := `dynlib
-end Module
-
 /--
 The core compilation / elaboration of the Lean file via `lean`,
 which produce the Lean binaries of the module (i.e., `olean` and `ilean`).
 It is thus the facet used by default for building imports of a module.
 Also, if the module is not lean-only, it produces `c` files as well.
 -/
+abbrev Module.leanBinFacet  := `lean.bin
 module_data lean.bin : ActiveOpaqueTarget

 /-- The `olean` file produced by `lean`  -/
+abbrev Module.oleanFacet  := `olean
 module_data olean : ActiveFileTarget

 /-- The `ilean` file produced by `lean` -/
+abbrev Module.ileanFacet := `ilean
 module_data ilean : ActiveFileTarget

 /-- The C file built from the Lean file via `lean` -/
+abbrev Module.cFacet := `lean.c
 module_data lean.c : ActiveFileTarget

 /-- The object file built from `lean.c` -/
+abbrev Module.oFacet := `lean.o
 module_data lean.o : ActiveFileTarget

 /-- Shared library for `--load-dynlib` -/
+abbrev Module.dynlibFacet := `dynlib
 module_data dynlib : ActiveFileTarget

 /-! ## Package Facets -/

-/-- The package's `extraDepTarget`. -/
+/-- The package's `extraDepTarget` mixed with its transitive dependencies `extraDepTarget`. -/
+abbrev Package.extraDepFacet := `extraDep
 package_data extraDep : ActiveOpaqueTarget

 /-! ## Target Facets -/

-abbrev LeanLib.staticFacet := `leanLib.static
-abbrev LeanLib.sharedFacet := `leanLib.shared
-abbrev LeanExe.exeFacet := `leanExe
-abbrev ExternLib.staticFacet := `externLib.static
-abbrev ExternLib.sharedFacet := `externLib.shared
-
 /-- A Lean library's static binary. -/
+abbrev LeanLib.staticFacet := `leanLib.static
 target_data leanLib.static : ActiveFileTarget

 /-- A Lean library's shared binary. -/
+abbrev LeanLib.sharedFacet := `leanLib.shared
 target_data leanLib.shared : ActiveFileTarget

 /-- A Lean binary executable. -/
+abbrev LeanExe.exeFacet := `leanExe
 target_data leanExe : ActiveFileTarget

 /-- A external library's static binary. -/
+abbrev ExternLib.staticFacet := `externLib.static
 target_data externLib.static : ActiveFileTarget

 /-- A external library's shared binary. -/
+abbrev ExternLib.sharedFacet := `externLib.shared
 target_data externLib.shared : ActiveFileTarget
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Index
-import Lake.Config.Workspace

 /-!
 Definitions to support `lake print-paths` builds.
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Roots
-import Lake.Build.Module
 import Lake.Build.Topological
 import Lake.Util.EStateT

@ -14,146 +13,35 @@ import Lake.Util.EStateT
 The Lake build index is the complete map of Lake build keys to
 Lake build functions, which is used by Lake to build any Lake build info.

-This module contains the definitions used to formalize this concept,
-and it leverages the index to perform topologically-based recursive builds.
+This module leverages the index to perform topologically-based recursive builds.
 -/

 open Std Lean
 namespace Lake

-/-!
-## Facet Build Maps
-/
-
-/-- A map from module facet names to build functions. -/
-abbrev ModuleBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Module → IndexBuildFn m → m (ModuleData k)
-
-@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
-
-/-- A map from package facet names to build functions. -/
-abbrev PackageBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Package → IndexBuildFn m → m (PackageData k)
-
-@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
-
-/-- A map from target facet names to build functions. -/
-abbrev TargetBuildMap (m : Type → Type v) :=
-  DRBMap Name (cmp := Name.quickCmp) fun k =>
-    Package → IndexBuildFn m → m (PackageData k)
-
-@[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
-
-/-!
-## Build Function Constructor Helpers
-/
-
-/--
-Converts a conveniently typed module facet build function into its
-dynamically typed equivalent.
-/
-@[inline] def mkModuleFacetBuild {facet : Name} (build : Module → IndexT m α)
-[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
-  cast (by rw [← h.family_key_eq_type]) build
-
-/--
-Converts a conveniently typed package facet build function into its
-dynamically typed equivalent.
-/
-@[inline] def mkPackageFacetBuild {facet : Name} (build : Package → IndexT m α)
-[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
-  cast (by rw [← h.family_key_eq_type]) build
-
 /--
 Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
-@[inline] def mkTargetFacetBuild (facet : Name) (build : IndexT m α)
-[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
+@[macroInline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
+[h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) :=
  cast (by rw [← h.family_key_eq_type]) build

-section
-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]`).
-/
-@[specialize] def moduleBuildMap : ModuleBuildMap m :=
-  have : MonadLift BuildM m := ⟨liftM⟩
-  ModuleBuildMap.empty (m := m)
-  -- Compute unique imports (direct × transitive)
-  |>.insert importFacet (mkModuleFacetBuild (·.recParseImports))
-  -- Build module (`.olean`, `.ilean`, and possibly `.c`)
-  |>.insert leanBinFacet (mkModuleFacetBuild (·.recBuildLean .leanBin))
-  |>.insert oleanFacet (mkModuleFacetBuild (·.recBuildLean .olean))
-  |>.insert ileanFacet (mkModuleFacetBuild (·.recBuildLean .ilean))
-  |>.insert cFacet (mkModuleFacetBuild (·.recBuildLean .c))
-  -- Build module `.o`
-  |>.insert oFacet (mkModuleFacetBuild <| fun mod => do
-    mod.mkOTarget (Target.active (← mod.c.recBuild)) |>.activate
-  )
-  -- Build shared library for `--load-dynlb`
-  |>.insert dynlibFacet (mkModuleFacetBuild (·.recBuildDynlib))
-
-/--
-A package facet name to build function map that contains builders for
-the initial set of Lake package facets (e.g., `extraDep`).
-/
-@[specialize] def packageBuildMap : PackageBuildMap m :=
-  have : MonadLift BuildM m := ⟨liftM⟩
-  PackageBuildMap.empty (m := m)
-  -- Compute the package's transitive dependencies
-  |>.insert `deps (mkPackageFacetBuild <| fun pkg => do
-    let mut deps := #[]
-    let mut depSet := PackageSet.empty
-    for dep in pkg.deps do
-      for depDep in (← recBuild <| dep.facet `deps) do
-        unless depSet.contains depDep do
-          deps := deps.push depDep
-          depSet := depSet.insert depDep
-      unless depSet.contains dep do
-        deps := deps.push dep
-        depSet := depSet.insert dep
-    return deps
-  )
-  -- Build the `extraDepTarget` for the package and its transitive dependencies
-  |>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do
-    let mut target := ActiveTarget.nil
-    for dep in pkg.deps do
-      target ← target.mixOpaqueAsync (← dep.extraDep.recBuild)
-    target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
-  )
-
 /-!
 ## Topologically-based Recursive Build Using the Index
 -/

 /-- Recursive build function for anything in the Lake build index. -/
-@[specialize] def recBuildIndex (info : BuildInfo) : IndexT m (BuildData info.key) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+def recBuildWithIndex (info : BuildInfo) : IndexBuildM (BuildData info.key) := do
  match info with
  | .moduleFacet mod facet =>
-    if let some build := moduleBuildMap.find? facet then
-      build mod
-    else if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-      have := config.familyDef
-      mkModuleFacetBuild config.build mod
+    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 =>
-    if let some build := packageBuildMap.find? facet then
-      build pkg
-    else if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-      have := config.familyDef
-      mkPackageFacetBuild config.build pkg
+    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 =>
@ -170,7 +58,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
  | .sharedLeanLib lib =>
    mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared
  | .leanExe exe =>
-    mkTargetFacetBuild LeanExe.exeFacet exe.recBuild
+    mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
  | .staticExternLib lib =>
    mkTargetFacetBuild ExternLib.staticFacet lib.target.activate
  | .sharedExternLib lib =>
@ -182,31 +70,41 @@ 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) :=
-  buildDTop BuildData BuildInfo.key recBuildIndex info
+def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
+  buildDTop BuildData BuildInfo.key recBuildWithIndex info

 /--
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler and return the dynamic result.
 -/
-@[inline] def buildIndexTop (info : BuildInfo)
-[FamilyDef BuildData info.key α] : CycleT BuildKey m α := do
-  cast (by simp) <| buildIndexTop' (m := m) info
-
-end
+@[macroInline] def buildIndexTop (info : BuildInfo)
+[FamilyDef BuildData info.key α] : RecBuildM α := do
+  cast (by simp) <| buildIndexTop' info

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

 /-- Build the given Lake target in a fresh build store. -/
-@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
+@[macroInline] def BuildInfo.build
+(self : BuildInfo) [FamilyDef 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. -/
+/-! ## Targets Using the Build Index -/
+
+/-- An opaque target that builds the info in a fresh build store. -/
@[inline] def BuildInfo.target (self : BuildInfo)
 [FamilyDef BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
  BuildTarget.mk' () <| self.build <&> (·.task)
+
+/-- A smart constructor for facet configurations that generate targets. -/
+@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α))
+[h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where
+  build := cast (by rw [← h.family_key_eq_type]) build
+  toTarget? := fun info key_eq_type =>
+    have : FamilyDef BuildData info.key (ActiveBuildTarget α) :=
+      ⟨h.family_key_eq_type ▸ key_eq_type⟩
+    info.target
--- a/Lake/Build/IndexTargets.lean
+++ b/Lake/Build/IndexTargets.lean
@ -10,25 +10,14 @@ open Lean hiding SearchPath

 namespace Lake

-/-! # Module Facet Targets -/
+/-! ## Module Facet Targets -/

+/-- An opaque target thats build the module facet in a fresh build store. -/
@[inline] def Module.facetTarget (facet : Name) (self : Module)
 [FamilyDef 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 -/
+/-! ## Pure Lean Lib Targets -/

 /--
 Build the `extraDepTarget` of a package and its (transitive) dependencies
@ -50,7 +39,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name)
@[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget :=
  self.builtinLib.leanTarget

-/-! # Native Lean Lib Targets -/
+/-! ## Native Lean Lib Targets -/

@[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
  self.static.target.withInfo self.sharedLibFile
@ -64,11 +53,14 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name)
@[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget :=
  self.builtinLib.sharedLibTarget

-/-! # Lean Executable Targets -/
+/-! ## Lean Executable Targets -/

@[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget :=
  self.exe.build

+@[inline] protected def LeanExe.recBuild (self : LeanExe) : IndexBuildM ActiveFileTarget :=
+  self.exe.recBuild
+
@[inline] protected def LeanExe.target (self : LeanExe) : FileTarget :=
  self.exe.target.withInfo self.file

--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@ -118,6 +118,9 @@ 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

+/-- The monad for build functions that are part of the index. -/
+abbrev IndexBuildM := IndexT RecBuildM
+
 /-- Build the given info using the Lake build index. -/
@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexT m α :=
  fun build => cast (by simp) <| build self
@ -136,12 +139,12 @@ Defined here because they need to import configurations, whereas the definitions
 there need to be imported by configurations.
 -/

-abbrev Module.importFacet := `lean.imports
-
 /-- The direct × transitive imports of the Lean module. -/
+abbrev Module.importFacet := `lean.imports
 module_data lean.imports : Array Module × Array Module

 /-- The package's complete array of transitive dependencies. -/
+abbrev Package.depsFacet := `deps
 package_data deps : Array Package


@ -174,7 +177,7 @@ end Module
 abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
  .packageFacet self facet

-/-- Build info for the package's `extraDepTarget`. -/
+/-- Build info for the package and its dependencies collective `extraDepTarget`. -/
 abbrev Package.extraDep (self : Package) : BuildInfo :=
  self.facet `extraDep

--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@ -4,9 +4,7 @@ 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
+import Lake.Build.Index

 open System

@ -64,12 +62,9 @@ def Module.mkDynlibTarget (self : Module) (linkTargets : Array FileTarget)

 /-! # Recursive Building -/

-section
-variable [Monad m] [MonadBuildStore m]
-
 /-- Compute library directories and build external library targets of the given packages. -/
 def recBuildExternalDynlibs (pkgs : Array Package)
-[MonadLog m] : IndexT m (Array ActiveFileTarget × Array FilePath) := do
+: IndexBuildM (Array ActiveFileTarget × Array FilePath) := do
  let mut libDirs := #[]
  let mut targets : Array ActiveFileTarget := #[]
  for pkg in pkgs do
@ -90,8 +85,8 @@ def recBuildExternalDynlibs (pkgs : Array Package)
  return (targets, libDirs)

 /-- Build the dynlibs of all imports. -/
-@[specialize] def recBuildDynlibs (pkg : Package) (imports : Array Module)
-[MonadLog m] : IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
+def recBuildDynlibs (pkg : Package) (imports : Array Module)
+: IndexBuildM (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
  let mut pkgs := #[]
  let mut pkgSet := PackageSet.empty.insert pkg
  let mut targets := #[]
@ -103,8 +98,8 @@ def recBuildExternalDynlibs (pkgs : Array Package)
  return (targets, ← recBuildExternalDynlibs <| pkgs.push pkg)

 /-- Build the dynlibs of the imports that want precompilation (and *their* imports). -/
-@[specialize] def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
-[MonadLog m] : IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
+def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
+: IndexBuildM (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
  let mut pkgs := #[]
  let mut pkgSet := PackageSet.empty.insert pkg
  let mut modSet := ModuleSet.empty
@ -134,9 +129,8 @@ optionally outputting a `.c` file if the modules' is not lean-only or the
 requested artifact is `c`. Returns an active target producing the requested
 artifact.
 -/
-@[specialize] def Module.recBuildLean (mod : Module) (art : LeanArtifact)
-: IndexT m (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+def Module.recBuildLean (mod : Module) (art : LeanArtifact)
+: IndexBuildM (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do
  let leanOnly := mod.isLeanOnly ∧ art ≠ .c

  -- Compute and build dependencies
@ -176,14 +170,38 @@ artifact.
    | .ilean => ileanTarget
    | .c => cTarget

+/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
+def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
+  mkFacetTargetConfig (·.recBuildLean .leanBin)
+
+/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
+def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
+  mkFacetTargetConfig (·.recBuildLean .olean)
+
+/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
+def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
+  mkFacetTargetConfig (·.recBuildLean .ilean)
+
+/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
+def Module.cFacetConfig : ModuleFacetConfig cFacet :=
+  mkFacetTargetConfig (·.recBuildLean .c)
+
+/--
+Recursively build the module's object file from its C file produced by `lean`.
+-/
+def Module.recBuildLeanO (self : Module) : IndexBuildM ActiveFileTarget := do
+  self.mkOTarget (Target.active (← self.c.recBuild)) |>.activate
+
+/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
+def Module.oFacetConfig : ModuleFacetConfig oFacet :=
+  mkFacetTargetConfig (·.recBuildLeanO)

 /--
 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⟩
+def Module.recParseImports (mod : Module)
+: IndexBuildM (Array Module × Array Module) := do
  let mut transImports := #[]
  let mut directImports := #[]
  let mut importSet := ModuleSet.empty
@ -202,15 +220,36 @@ building an `Array` product of its direct and transitive local imports.
      directImports := directImports.push mod
  return (directImports, transImports)

+/-- The `ModuleFacetConfig` for the builtin `importFacet`. -/
+def Module.importFacetConfig : ModuleFacetConfig importFacet :=
+  mkFacetConfig (·.recParseImports)
+
 /--
 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⟩
+def Module.recBuildDynlib (mod : Module) : IndexBuildM ActiveFileTarget := do
  let (_, transImports) ← mod.imports.recBuild
  let linkTargets ← mod.nativeFacets.mapM fun facet => do
    return Target.active <| ← recBuild <| mod.facet facet.name
  let (modTargets, pkgTargets, libDirs) ← recBuildDynlibs mod.pkg transImports
  let libTargets := modTargets ++ pkgTargets |>.map Target.active
  mod.mkDynlibTarget linkTargets libDirs libTargets |>.activate
+
+/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
+def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
+  mkFacetTargetConfig (·.recBuildDynlib)
+
+open Module in
+/--
+A name-configuration map for the initial set of
+Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
+-/
+def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
+  DNameMap.empty
+  |>.insert importFacet importFacetConfig
+  |>.insert leanBinFacet leanBinFacetConfig
+  |>.insert oleanFacet oleanFacetConfig
+  |>.insert ileanFacet ileanFacetConfig
+  |>.insert cFacet cFacetConfig
+  |>.insert oFacet oFacetConfig
+  |>.insert dynlibFacet dynlibFacetConfig
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@ -0,0 +1,47 @@
+/-
+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
+
+namespace Lake
+
+/-- Compute a topological ordering of the package's transitive dependencies. -/
+def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do
+  let mut deps := #[]
+  let mut depSet := PackageSet.empty
+  for dep in self.deps do
+    for depDep in (← recBuild <| dep.facet `deps) do
+      unless depSet.contains depDep do
+        deps := deps.push depDep
+        depSet := depSet.insert depDep
+    unless depSet.contains dep do
+      deps := deps.push dep
+      depSet := depSet.insert dep
+  return deps
+
+/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
+def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
+  mkFacetConfig (·.recComputeDeps)
+
+/-- Build the `extraDepTarget` for the package and its transitive dependencies. -/
+def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM ActiveOpaqueTarget := do
+  let mut target := ActiveTarget.nil
+  for dep in self.deps do
+    target ← target.mixOpaqueAsync (← dep.extraDep.recBuild)
+  target.mixOpaqueAsync <| ← self.extraDepTarget.activate
+
+/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
+def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
+  mkFacetTargetConfig (·.recBuildExtraDepTargets)
+
+open Package in
+/--
+A package facet name to build function map that contains builders for
+the initial set of Lake package facets (e.g., `extraDep`).
+-/
+def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
+  DNameMap.empty
+  |>.insert depsFacet depsFacetConfig
+  |>.insert extraDepFacet extraDepFacetConfig
--- a/Lake/Build/Roots.lean
+++ b/Lake/Build/Roots.lean
@ -9,14 +9,11 @@ import Lake.Build.Targets

 namespace Lake

-variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
-
 /-! # Build Static Lib -/

 /-- Build and collect the specified facet of the library's local modules. -/
-@[specialize] def LeanLib.recBuildLocalModules
-(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexT m (Array α) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+def LeanLib.recBuildLocalModules
+(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexT RecBuildM (Array α) := do
  let mut results := #[]
  let mut modSet := ModuleSet.empty
  let mods ← self.getModuleArray
@ -31,9 +28,7 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
          modSet := modSet.insert mod
  return results

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

@ -43,10 +38,9 @@ def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do
 Build and collect the local object files and external libraries
 of a library and its modules' imports.
 -/
-@[specialize] def LeanLib.recBuildLinks
+def LeanLib.recBuildLinks
 (facets : Array (ModuleFacet ActiveFileTarget)) (self : LeanLib)
-: IndexT m (Array ActiveFileTarget) := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+: IndexT RecBuildM (Array ActiveFileTarget) := do
  -- Build and collect modules
  let mut pkgs := #[]
  let mut pkgSet := PackageSet.empty
@ -72,17 +66,13 @@ of a library and its modules' imports.
      targets := targets.push target
  return targets

-@[specialize] protected
-def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+protected def LeanLib.recBuildShared (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
  let linkTargets := (← self.recBuildLinks self.nativeFacets).map Target.active
  leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate

 /-! # Build Executable -/

-@[specialize] protected
-def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
-  have : MonadLift BuildM m := ⟨liftM⟩
+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
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@ -38,12 +38,10 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except
    return mod.facetTarget oFacet
  else if facet == `dynlib then
    return mod.facetTarget dynlibFacet
-  else if let some config := ws.findModuleFacetConfig? facet then
-    if let some (.up ⟨_, h⟩) := config.result_eq_target? then
-      have := config.familyDefTarget h
-      return mod.facetTarget facet
-    else
-      throw <| CliError.nonTargetFacet "module" facet
+  else if let some config := ws.findModuleFacetConfig? facet then do
+    let some target := config.toTarget? (mod.facet facet) rfl
+      | throw <| CliError.nonTargetFacet "module" facet
+    return target
  else
    throw <| CliError.unknownFacet "module" facet

@ -105,12 +103,10 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Excep
    return pkg.sharedLibTarget.withoutInfo
  else if facet == `leanLib then
    return pkg.leanLibTarget.withoutInfo
-  else if let some config := ws.findPackageFacetConfig? facet then
-    if let some (.up ⟨_, h⟩) := config.result_eq_target? then
-      have := config.familyDefTarget h
-      return pkg.facet facet |>.target
-    else
-      throw <| CliError.nonTargetFacet "package" facet
+  else if let some config := ws.findPackageFacetConfig? facet then do
+    let some target := config.toTarget? (pkg.facet facet) rfl
+      | throw <| CliError.nonTargetFacet "package" facet
+    return target
  else
    throw <| CliError.unknownFacet "package" facet

--- a/Lake/Config/FacetConfig.lean
+++ b/Lake/Config/FacetConfig.lean
@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
+Authors: Mac Malone, Mario Carneiro
 -/
 import Lake.Build.Info
 import Lake.Build.Store
@ -9,67 +9,34 @@ import Lake.Build.Store
 namespace Lake

 /-- A facet's declarative configuration. -/
-structure FacetConfig (DataFam : Name → Type u) (BuildFn : Type u → Type v) (name : Name) where
-  /-- The type of the target's build result. -/
-  resultType : Type u
-  /-- The facet's build function. -/
-  build : BuildFn resultType
-  /-- Proof that the facet's build result data type is properly registered. -/
-  data_eq_result : DataFam name = resultType
-   /-- Is this facet a buildable target? -/
-  result_eq_target? : Option <| PLift <| PSigma fun α => resultType = ActiveBuildTarget α
+structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where
+  /-- 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})
+  deriving Inhabited

-instance [(α : Type u) → Inhabited (BuildFn α)] : Inhabited (FacetConfig DataFam BuildFn name) := ⟨{
-  resultType := DataFam name
-  build := default
-  data_eq_result := rfl
-  result_eq_target? := none
-}⟩
+protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name

-abbrev FacetBuildFn (ι) :=
-  fun resultType => {m : Type → Type} →
-    [Monad m] → [MonadLift BuildM m] → [MonadBuildStore m] →
-    ι → IndexT m resultType
-
-instance : Inhabited (FacetBuildFn ι α) :=
-  ⟨fun _ => liftM (m := BuildM) failure⟩
-
-namespace FacetConfig
-
-protected def name (_ : FacetConfig DataFam BuildFn name) :=
-  name
-
-instance (cfg : FacetConfig Fam Fn name) :
-  FamilyDef Fam cfg.name cfg.resultType := ⟨cfg.data_eq_result⟩
-
-def familyDef (cfg : FacetConfig Fam Fn name) : FamilyDef Fam name cfg.resultType :=
-  ⟨cfg.data_eq_result⟩
-
-def familyDefTarget (cfg : FacetConfig Fam Fn name)
-(h : cfg.resultType = ActiveBuildTarget α) : FamilyDef Fam name (ActiveBuildTarget α) :=
-  ⟨h ▸ cfg.data_eq_result⟩
-
-end FacetConfig
+/-- A smart constructor for facet configurations that are not known to generate targets. -/
+@[inline] def mkFacetConfig (build : ι → IndexBuildM α)
+[h : FamilyDef Fam facet α] : FacetConfig Fam ι facet where
+  build := cast (by rw [← h.family_key_eq_type]) build
+  toTarget? := fun _ _ => none

 /-- A dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where
  name : Name
  config : β name

--------------------------------------------------------------------------------
-
 /-- A module facet's declarative configuration. -/
-abbrev ModuleFacetConfig := FacetConfig ModuleData (FacetBuildFn Module)
-hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig name
+abbrev ModuleFacetConfig := FacetConfig ModuleData Module

 /-- A module facet declaration from a configuration file. -/
 abbrev ModuleFacetDecl := NamedConfigDecl ModuleFacetConfig

--------------------------------------------------------------------------------
-
 /-- A package facet's declarative configuration. -/
-abbrev PackageFacetConfig := FacetConfig PackageData (FacetBuildFn Package)
-hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig name
+abbrev PackageFacetConfig := FacetConfig PackageData Package

 /-- A package facet declaration from a configuration file. -/
 abbrev PackageFacetDecl := NamedConfigDecl PackageFacetConfig
--- a/Lake/Config/Opaque.lean
+++ b/Lake/Config/Opaque.lean
@ -14,11 +14,5 @@ declare_opaque_type OpaquePackage
 /-- Opaque reference to a `Workspace` used for forward declaration. -/
 declare_opaque_type OpaqueWorkspace

-/-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/
-declare_opaque_type OpaqueModuleFacetConfig (name : Name)
-
-/-- Opaque reference to a `PackageFacetConfig` used for forward declaration. -/
-declare_opaque_type OpaquePackageFacetConfig (name : Name)
-
 /-- Opaque reference to a `TargetConfig` used for forward declaration. -/
 declare_opaque_type OpaqueTargetConfig
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@ -239,6 +239,7 @@ end PackageConfig
 --------------------------------------------------------------------------------

 abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp
+@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty

 /-- A Lake package -- its location plus its configuration. -/
 structure Package where
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@ -17,7 +17,7 @@ namespace Lake
 def manifestFileName := "manifest.json"

 /-- A Lake workspace -- the top-level package directory. -/
-structure Workspace where
+structure Workspace : Type where
  /-- The root package of the workspace. -/
  root : Package
  /-- The detect `Lake.Env` of the workspace. -/
@ -28,12 +28,12 @@ structure Workspace where
  Name-configuration map of (opaque references to)
  module facets defined in the workspace.
  -/
-  opaqueModuleFacetConfigs : DNameMap OpaqueModuleFacetConfig := {}
+  moduleFacetConfigs : DNameMap ModuleFacetConfig := {}
  /--
  Name-configuration map of (opaque references to)
  module facets defined in the workspace.
  -/
-  opaquePackageFacetConfigs : DNameMap OpaquePackageFacetConfig := {}
+  packageFacetConfigs : DNameMap PackageFacetConfig := {}
  deriving Inhabited

 hydrate_opaque_type OpaqueWorkspace Workspace
@ -102,23 +102,19 @@ def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × Targ

 /-- Add a module facet to the workspace. -/
 def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
-  {self with opaqueModuleFacetConfigs := self.opaqueModuleFacetConfigs.insert cfg.name (.mk cfg)}
+  {self with moduleFacetConfigs := self.moduleFacetConfigs.insert cfg.name cfg}

 /-- Try to find a module facet configuration in the workspace with the given name. -/
 def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
-  match self.opaqueModuleFacetConfigs.find? name with
-  | some cfg => cfg.get
-  | none  => none
+  self.moduleFacetConfigs.find? name

 /-- Add a package facet to the workspace. -/
 def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
-  {self with opaquePackageFacetConfigs := self.opaquePackageFacetConfigs.insert cfg.name (.mk cfg)}
+  {self with packageFacetConfigs := self.packageFacetConfigs.insert cfg.name cfg}

 /-- Try to find a package facet configuration in the workspace with the given name. -/
 def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
-  match self.opaquePackageFacetConfigs.find? name with
-  | some cfg => cfg.get
-  | none  => none
+  self.packageFacetConfigs.find? name

 /-- The `LEAN_PATH` of the workspace. -/
 def leanPath (self : Workspace) : SearchPath :=
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.DSL.DeclUtil
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
+import Lake.Build.Index

 /-!
 Macros for declaring custom facets and targets.
@ -21,17 +22,11 @@ kw:"module_facet " sig:simpleDeclSig : command => do
  | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) =>
    let attr ← withRef kw `(Term.attrInstance| moduleFacet)
    let attrs := #[attr] ++ expandAttrs attrs?
-    let axm := mkIdentFrom id <| ``ModuleData ++ id.getId
    let name := Name.quoteFrom id id.getId
    `(module_data $id : ActiveBuildTarget $ty
      $[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
        name := $name
-        config := {
-          resultType := ActiveBuildTarget $ty
-          build := $defn
-          data_eq_result := $axm
-          result_eq_target? := some (.up ⟨$ty, rfl⟩)
-        }
+        config := Lake.mkFacetTargetConfig $defn
      })
  | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"

@ -42,17 +37,11 @@ kw:"package_facet " sig:simpleDeclSig : command => do
  | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) =>
    let attr ← withRef kw `(Term.attrInstance| packageFacet)
    let attrs := #[attr] ++ expandAttrs attrs?
-    let axm := mkIdentFrom id <| ``PackageData ++ id.getId
    let name := Name.quoteFrom id id.getId
    `(package_data $id : ActiveBuildTarget $ty
      $[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
        name := $name
-        config := {
-          resultType := ActiveBuildTarget $ty
-          build := $defn
-          data_eq_result := $axm
-          result_eq_target? := some (.up ⟨$ty, rfl⟩)
-        }
+        config := Lake.mkFacetTargetConfig $defn
      })
  | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"

--- a/Lake/Load/Main.lean
+++ b/Lake/Load/Main.lean
@ -7,6 +7,8 @@ import Lake.Util.EStateT
 import Lake.Util.StoreInsts
 import Lake.Config.Workspace
 import Lake.Build.Topological
+import Lake.Build.Module
+import Lake.Build.Package
 import Lake.Load.Materialize
 import Lake.Load.Package
 import Lake.Load.Elab
@ -69,7 +71,11 @@ elaborating its configuration file and resolve its dependencies.
 def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
  Lean.searchPathRef.set config.env.leanSearchPath
  let root ← loadPkg config.rootDir config.configOpts config.leanOpts config.configFile
-  let ws : Workspace := {root, lakeEnv := config.env}
+  let ws : Workspace := {
+    root, lakeEnv := config.env
+    moduleFacetConfigs := initModuleFacetConfigs
+    packageFacetConfigs := initPackageFacetConfigs
+  }
  let deps ← IO.ofExcept <| loadDeps root.configEnv config.leanOpts
  let manifest ← Manifest.loadFromFile ws.manifestFile |>.catchExceptions fun _ => pure {}
  let ((ws, deps), manifest) ← resolveDeps ws root