diff --git a/Lake/Build.lean b/Lake/Build.lean
index 48d1962077..cc9b7b7da1 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -5,8 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Build.Monad
 import Lake.Build.Actions
-import Lake.Build.TargetTypes
-import Lake.Build.Targets
 import Lake.Build.Module
-import Lake.Build.Package
-import Lake.Build.Binary
+import Lake.Build.Library
+import Lake.Build.Executable
+import Lake.Build.Imports
diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
new file mode 100644
index 0000000000..0502c0d103
--- /dev/null
+++ b/Lake/Build/Data.lean
@@ -0,0 +1,53 @@
+/-
+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.Key
+import Lake.Util.DynamicType
+
+open Lean
+namespace Lake
+
+/--
+Type of build data associated with a module facet in the Lake build store.
+For example a transitive × direct import pair for `imports` or an active build
+target for `lean.c`.
+
+It is a dynamic type, meaning additional alternatives can be add lazily
+as needed.
+-/
+opaque ModuleData (facet : WfName) : Type
+
+/-- Type of build data associated with package facets (e.g., `extraDep`). -/
+opaque PackageData (facet : WfName) : Type
+
+/-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
+opaque TargetData (key : BuildKey) : Type
+
+/--
+Type of the build data associated with a key in the Lake build store.
+It is dynamic type composed of the three separate dynamic types for modules,
+packages, and targets.
+-/
+def BuildData (key : BuildKey) :=
+  if key.isModuleKey then
+    ModuleData key.facet
+  else if key.isPackageKey then
+    PackageData key.facet
+  else
+    TargetData key
+
+/-- Macro for declaring new `PackageData`. -/
+scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
+"package_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``PackageData
+  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+
+/-- Macro for declaring new `ModuleData`. -/
+scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
+"module_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``ModuleData
+  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean
new file mode 100644
index 0000000000..d18658e311
--- /dev/null
+++ b/Lake/Build/Executable.lean
@@ -0,0 +1,32 @@
+/-
+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.Library
+
+open Std System
+open Lean (Name NameMap)
+
+namespace Lake
+
+-- # Build Package Executable
+
+def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
+  let exeFile := self.binDir / exe.fileName
+  BuildTarget.mk' exeFile do
+    let root : Module := ⟨self, WfName.ofName exe.root⟩
+    let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
+    let pkgLinkTargets ← self.linkTargetsOf cTargetMap
+    let linkTargets :=
+      if self.isLocalModule exe.root then
+        pkgLinkTargets
+      else
+        let rootTarget := cTargetMap.find? root.name |>.get!
+        let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
+        #[rootLinkTarget] ++ pkgLinkTargets
+    let target := leanExeTarget exeFile linkTargets exe.linkArgs
+    target.materializeAsync
+
+protected def Package.exeTarget (self : Package) : FileTarget :=
+  self.mkExeTarget self.builtinExeConfig
diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
new file mode 100644
index 0000000000..80067af460
--- /dev/null
+++ b/Lake/Build/Imports.lean
@@ -0,0 +1,46 @@
+/-
+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.Config.Workspace
+
+/-!
+Definitions to support `lake print-paths` builds.
+-/
+
+namespace Lake
+
+/--
+Construct an `Array` of `Module`s for the workspace-local modules of
+a `List` of import strings.
+-/
+def Workspace.processImportList
+(imports : List String) (self : Workspace) : Array Module := Id.run do
+  let mut localImports := #[]
+  for imp in imports do
+    if let some mod := self.findModule? imp.toName then
+      localImports := localImports.push mod
+  return localImports
+
+/--
+Build the workspace-local modules of list of imports.
+
+Build only module `.olean` and `.ilean` files if
+the default package build does not include any binary targets
+Otherwise, also build `.c` files.
+-/
+def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
+  if imports.isEmpty then
+    -- build the package's (and its dependencies') `extraDepTarget`
+    buildPackageFacet self &`extraDep >>= (·.buildOpaque)
+  else
+    -- build local imports from list
+    let mods := (← getWorkspace).processImportList imports
+    if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
+      let targets ← buildModuleFacetArray mods &`lean
+      targets.forM (·.buildOpaque)
+    else
+      let targets ← buildModuleFacetArray mods &`lean.c
+      targets.forM (·.buildOpaque)
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
new file mode 100644
index 0000000000..f280b431c7
--- /dev/null
+++ b/Lake/Build/Index.lean
@@ -0,0 +1,178 @@
+/-
+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.Topological
+import Lake.Util.EStateT
+
+/-!
+# The Lake Build Index
+
+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 topological-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 WfName (cmp := WfName.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 WfName (cmp := WfName.quickCmp) fun k =>
+    Package → IndexBuildFn m → m (PackageData k)
+
+@[inline] def PackageBuildMap.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 : WfName}
+(build : Module → IndexBuildFn m → m α) [h : DynamicType ModuleData facet α]
+: Module → IndexBuildFn m → m (ModuleData facet) :=
+  cast (by rw [← h.eq_dynamic_type]) build
+
+/--
+Converts a conveniently typed package facet build function into its
+dynamically typed equivalent.
+-/
+@[inline] def mkPackageFacetBuild {facet : WfName}
+(build : Package → IndexBuildFn m → m α) [h : DynamicType PackageData facet α]
+: Package → IndexBuildFn m → m (PackageData facet) :=
+  cast (by rw [← h.eq_dynamic_type]) build
+
+section
+variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
+
+/-!
+## Initial Facet Maps
+-/
+
+/--
+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.insert
+  -- Compute unique imports (direct × transitive)
+  &`lean.imports (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recParseImports recurse
+  ) |>.insert
+  -- Build module (`.olean` and `.ilean`)
+  &`lean (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recBuildLean false recurse
+  ) |>.insert
+  &`olean (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recBuildFacet &`lean recurse
+  ) |>.insert
+  &`ilean (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recBuildFacet &`lean recurse
+  ) |>.insert
+  -- Build module `.c` (and `.olean` and `.ilean`)
+  &`lean.c (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recBuildLean true recurse <&> (·.withInfo mod.cFile)
+  ) |>.insert
+  -- Build module `.o`
+  &`lean.o (mkModuleFacetBuild <| fun mod recurse => do
+    let cTarget ← mod.recBuildFacet &`lean.c recurse
+    mod.mkOTarget (Target.active cTarget) |>.activate
+  ) |>.insert
+  -- Build shared library for `--load-dynlb`
+  &`lean.dynlib (mkModuleFacetBuild <| fun mod recurse => do
+    mod.recBuildDynLib recurse
+  )
+
+/--
+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.insert
+  -- Build the `extraDepTarget` for the package and its transitive dependencies
+  &`extraDep (mkPackageFacetBuild <| fun pkg recurse => do
+    let mut target := ActiveTarget.nil
+    for dep in pkg.dependencies do
+      if let some depPkg ← findPackage? dep.name then
+        let extraDepTarget ← depPkg.recBuildFacet &`extraDep recurse
+        target ← target.mixOpaqueAsync extraDepTarget
+    target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
+  )
+
+/-!
+## Topologically-based Recursive Build Using the Index
+-/
+
+/-- The type of a recursive build function for the Lake build index. -/
+abbrev RecIndexBuildFn (m) :=
+  DRecBuildFn BuildInfo (BuildData ·.key) m
+
+/-- Recursive build function for anything in the Lake build index. -/
+@[specialize] def recBuildIndex : RecIndexBuildFn m := fun info recurse => do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  match info with
+  | .module mod facet =>
+    if let some build := moduleBuildMap.find? facet then
+      build mod recurse
+    else
+      error s!"do not know how to build module facet `{facet}`"
+  | .package pkg facet =>
+    if let some build := packageBuildMap.find? facet then
+      build pkg recurse
+    else
+      error s!"do not know how to build package facet `{facet}`"
+  | _ =>
+    error s!"do not know how to build `{info.key}`"
+
+/--
+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
+
+/--
+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.
+-/
+@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
+[h : DynamicType PackageData facet α] : CycleT BuildKey m α  :=
+  have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
+  cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
+
+end
+
+/-!
+## Package Facet Builders
+-/
+
+/--
+Recursively build the specified facet of the given package,
+returning the result.
+-/
+def buildPackageFacet
+(pkg : Package) (facet : WfName)
+[DynamicType PackageData facet α] : BuildM α := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
+    buildPackageTop pkg facet
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
new file mode 100644
index 0000000000..ab369f94f3
--- /dev/null
+++ b/Lake/Build/Info.lean
@@ -0,0 +1,73 @@
+/-
+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.Data
+import Lake.Config.Module
+
+namespace Lake
+
+-- # Build Key Constructor Helpers
+
+@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
+  ⟨⟨none, self.name, facet⟩, rfl, rfl⟩
+
+@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
+  ⟨⟨self.name, none, facet⟩, rfl, rfl⟩
+
+-- # Build Info
+
+/-- The type of Lake's build info. -/
+inductive BuildInfo
+| module (module : Module) (facet : WfName)
+| package (package : Package) (facet : WfName)
+| target (package : Package) (target : WfName) (facet : WfName)
+
+def BuildInfo.key : (self : BuildInfo) → BuildKey
+| module m f => ⟨none, m.name, f⟩
+| package p f => ⟨p.name, none, f⟩
+| target p t f => ⟨p.name, t, f⟩
+
+/-- A build function for a single element of the Lake build index. -/
+abbrev IndexBuildFn (m : Type → Type v) :=
+  -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (BuildData info.key)
+
+@[inline] def Module.recBuildFacet {m : Type → Type v}
+(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
+(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
+  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.module mod facet
+
+@[inline] def Package.recBuildFacet {m : Type → Type v}
+(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
+(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
+  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.package pkg facet
+
+-- # Data Types of Build Results
+
+/-- Lean binary build (`olean`, `ilean` files) -/
+module_data lean : ActiveOpaqueTarget
+
+/-- The `olean` file produced by `lean`  -/
+module_data olean : ActiveOpaqueTarget
+
+/-- The `ilean` file produced by `lean` -/
+module_data ilean : ActiveOpaqueTarget
+
+/-- The C file built from the Lean file via `lean` -/
+module_data lean.c : ActiveFileTarget
+
+/-- The object file built from `lean.c` -/
+module_data lean.o : ActiveFileTarget
+
+/-- Shared library for `--load-dynlib` -/
+module_data lean.dynlib : ActiveFileTarget
+
+/-- The direct × transitive imports of the Lean module. -/
+module_data lean.imports : Array Module × Array Module
+
+/-- The package's `extraDepTarget`. -/
+package_data extraDep : ActiveOpaqueTarget
diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean
new file mode 100644
index 0000000000..9d50ca92ed
--- /dev/null
+++ b/Lake/Build/Key.lean
@@ -0,0 +1,142 @@
+/-
+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.Util.Name
+
+namespace Lake
+
+/-- The type of keys in the Lake build store. -/
+structure BuildKey where
+  package? : Option WfName
+  target? : Option WfName
+  facet : WfName
+  deriving Inhabited, Repr, DecidableEq, Hashable
+
+namespace BuildKey
+
+@[inline] def hasPackage (self : BuildKey) : Bool :=
+  self.package? ≠ none
+
+@[simp] theorem hasPackage_mk : BuildKey.hasPackage ⟨some p, x, f⟩ := by
+  simp [BuildKey.hasPackage]
+
+@[inline] def package (self : BuildKey) (h : self.hasPackage) : WfName :=
+  match mh:self.package? with
+  | some n => n
+  | none => absurd mh <| by
+    unfold hasPackage at h
+    exact of_decide_eq_true h
+
+@[inline] def hasTarget (self : BuildKey) : Bool :=
+  self.target? ≠ none
+
+@[simp] theorem hasTarget_mk : BuildKey.hasTarget ⟨x, some t, f⟩ := by
+  simp [BuildKey.hasTarget]
+
+@[inline] def target (self : BuildKey) (h : self.hasTarget) : WfName :=
+  match mh:self.target? with
+  | some n => n
+  | none => absurd mh <| by
+    unfold hasTarget at h
+    exact of_decide_eq_true h
+
+@[inline] def isModuleKey (self : BuildKey) : Bool :=
+  self.package? = none ∧ self.hasTarget
+
+@[simp] theorem isModuleKey_mk : BuildKey.isModuleKey ⟨none, some m, f⟩ := by
+  simp [BuildKey.isModuleKey]
+
+@[simp] theorem not_isModuleKey_pkg : ¬BuildKey.isModuleKey ⟨some pkg, x, f⟩ := by
+  simp [BuildKey.isModuleKey]
+
+@[inline] def module (self : BuildKey) (h : self.isModuleKey) : WfName :=
+  self.target <| by
+    unfold isModuleKey at h
+    exact of_decide_eq_true h |>.2
+
+@[inline] def isPackageKey (self : BuildKey) : Bool :=
+  self.hasPackage ∧ self.target? = none
+
+@[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
+  simp [BuildKey.isPackageKey]
+
+@[inline] def isTargetKey (self : BuildKey) : Bool :=
+  self.hasPackage ∧ self.hasTarget
+
+@[simp] theorem isTargetKey_mk : BuildKey.isTargetKey ⟨some p, some t, f⟩ := by
+  simp [BuildKey.isTargetKey]
+
+protected def toString : (self : BuildKey) → String
+| ⟨some p,  none,   f⟩ => s!"@{p}:{f}"
+| ⟨none,    some m, f⟩ => s!"+{m}:{f}"
+| ⟨some p,  some t, f⟩ => s!"{p}/{t}:{f}"
+| ⟨none,    none,   f⟩ => s!":{f}"
+
+instance : ToString BuildKey := ⟨(·.toString)⟩
+
+def quickCmp (k k' : BuildKey) :=
+  match Option.compareWith WfName.quickCmp k.package? k'.package? with
+  | .eq =>
+    match Option.compareWith WfName.quickCmp k.target? k'.target? with
+    | .eq => k.facet.quickCmp k'.facet
+    | ord => ord
+  | ord => ord
+
+theorem eq_of_quickCmp :
+{k k' : _} → quickCmp k k' = Ordering.eq → k = k' := by
+  intro ⟨p, t, f⟩ ⟨p', t', f'⟩
+  unfold quickCmp
+  simp only []
+  split
+  next p_eq =>
+    split
+    next t_eq =>
+      intro f_eq
+      have p_eq := eq_of_cmp p_eq
+      have t_eq := eq_of_cmp t_eq
+      have f_eq := eq_of_cmp f_eq
+      simp only [p_eq, t_eq, f_eq]
+    next =>
+      intros; contradiction
+  next =>
+    intros; contradiction
+
+instance : EqOfCmp BuildKey quickCmp where
+  eq_of_cmp := eq_of_quickCmp
+
+end BuildKey
+
+-- ## Subtypes
+
+/-- The type of build keys for modules. -/
+structure ModuleBuildKey (fixedFacet : WfName) extends BuildKey where
+  is_module_key : toBuildKey.isModuleKey = true
+  facet_eq_fixed : toBuildKey.facet = fixedFacet
+
+instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
+
+@[inline] def BuildKey.toModuleKey
+(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
+  ⟨self, h, rfl⟩
+
+@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
+  self.toBuildKey.module self.is_module_key
+
+/-- The type of build keys for packages. -/
+structure PackageBuildKey (fixedFacet : WfName) extends BuildKey where
+  is_package_key : toBuildKey.isPackageKey = true
+  facet_eq_fixed : toBuildKey.facet = fixedFacet
+
+instance : Coe (PackageBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
+
+@[inline] def BuildKey.toPackageKey
+(self : BuildKey) (h : self.isPackageKey) : PackageBuildKey self.facet :=
+  ⟨self, h, rfl⟩
+
+@[inline] def PackageBuildKey.package (self : PackageBuildKey f) : WfName :=
+  self.toBuildKey.package <| by
+    have h := self.is_package_key
+    unfold BuildKey.isPackageKey at h
+    exact (of_decide_eq_true h).1
diff --git a/Lake/Build/Binary.lean b/Lake/Build/Library.lean
similarity index 64%
rename from Lake/Build/Binary.lean
rename to Lake/Build/Library.lean
index 99766ecf0a..6246ff58d2 100644
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Library.lean
@@ -1,16 +1,40 @@
 /-
-Copyright (c) 2021 Mac Malone. All rights reserved.
+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.Package
-import Lake.Build.Targets
+import Lake.Build.Module
 
 open Std System
-open Lean (Name NameMap)
+open Lean hiding SearchPath
 
 namespace Lake
 
+-- # Build Package Lean Lib
+
+def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
+  return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
+
+/--
+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 Package.buildLibModules
+(self : Package) (lib : LeanLibConfig) (facet : WfName)
+[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
+  let buildMods : BuildM _ := do
+    let mods ← self.getLibModuleArray lib
+    let modTargets ← buildModuleFacetArray mods facet
+    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
+  buildMods.catchFailure fun _ => pure <| failure
+
+def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
+  Target.opaque <| self.buildLibModules lib &`lean
+
+def Package.libTarget (self : Package) : OpaqueTarget :=
+  self.mkLibTarget self.builtinLibConfig
+
 -- # Build Package Static Lib
 
 def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
@@ -52,24 +76,3 @@ def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarge
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
   self.mkSharedLibTarget self.builtinLibConfig
-
--- # Build Package Bin
-
-def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
-  let exeFile := self.binDir / exe.fileName
-  BuildTarget.mk' exeFile do
-    let root : Module := ⟨self, WfName.ofName exe.root⟩
-    let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
-    let pkgLinkTargets ← self.linkTargetsOf cTargetMap
-    let linkTargets :=
-      if self.isLocalModule exe.root then
-        pkgLinkTargets
-      else
-        let rootTarget := cTargetMap.find? root.name |>.get!
-        let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
-        #[rootLinkTarget] ++ pkgLinkTargets
-    let target := leanExeTarget exeFile linkTargets exe.linkArgs
-    target.materializeAsync
-
-protected def Package.exeTarget (self : Package) : FileTarget :=
-  self.mkExeTarget self.builtinExeConfig
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index b430211b37..5403009c80 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -1,536 +1,19 @@
+
 /-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Mac Malone
+Authors: Mac Malone
 -/
-import Lake.Util.EStateT
-import Lean.Elab.Import
-import Lake.Build.Target
-import Lake.Build.Actions
-import Lake.Build.Recursive
-import Lake.Build.Targets
-import Lake.Config.Module
-
-open Std System
-open Lean hiding SearchPath
+import Lake.Build.Index
 
+open Std Lean
 namespace Lake
 
-abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
-@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
-
-abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
-@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
-
--- # Dynamic Data
-
-class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
-  eq_dynamic_type : Δ a = β
-
-export DynamicType (eq_dynamic_type)
-
-@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
-  cast eq_dynamic_type.symm b
-
-@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
-  cast eq_dynamic_type b
-
-/--
-The syntax:
-
-```lean
-dynamic_data foo : Data 0 := Nat
-```
-
-Declares a new alternative for the dynamic `Data` type via the
-production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
-that uses this axiom for key `0`.
--/
-scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
-"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
-  let tid := extractMacroScopes dty.getId |>.name
-  if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
-    let app := Syntax.mkApp dty #[key]
-    let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
-    `($[$doc?]? @[simp] axiom $axm : $app = $ty
-    instance : DynamicType $dty $key $ty := ⟨$axm⟩)
-  else
-    Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
-
-@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
-  fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
-  store a := store k <| cast t.eq_dynamic_type.symm a
-
--- # Build Key
-
-/-- The type of keys in the Lake build store. -/
-structure BuildKey where
-  package? : Option WfName
-  target? : Option WfName
-  facet : WfName
-  deriving Inhabited, Repr, DecidableEq, Hashable
-
-namespace BuildKey
-
-@[inline] def hasPackage (self : BuildKey) : Bool :=
-  self.package? ≠ none
-
-@[simp] theorem hasPackage_mk : BuildKey.hasPackage ⟨some p, x, f⟩ := by
-  simp [BuildKey.hasPackage]
-
-@[inline] def package (self : BuildKey) (h : self.hasPackage) : WfName :=
-  match mh:self.package? with
-  | some n => n
-  | none => absurd mh <| by
-    unfold hasPackage at h
-    exact of_decide_eq_true h
-
-@[inline] def hasTarget (self : BuildKey) : Bool :=
-  self.target? ≠ none
-
-@[simp] theorem hasTarget_mk : BuildKey.hasTarget ⟨x, some t, f⟩ := by
-  simp [BuildKey.hasTarget]
-
-@[inline] def target (self : BuildKey) (h : self.hasTarget) : WfName :=
-  match mh:self.target? with
-  | some n => n
-  | none => absurd mh <| by
-    unfold hasTarget at h
-    exact of_decide_eq_true h
-
-@[inline] def isModuleKey (self : BuildKey) : Bool :=
-  self.package? = none ∧ self.hasTarget
-
-@[simp] theorem isModuleKey_mk : BuildKey.isModuleKey ⟨none, some m, f⟩ := by
-  simp [BuildKey.isModuleKey]
-
-@[simp] theorem not_isModuleKey_pkg : ¬BuildKey.isModuleKey ⟨some pkg, x, f⟩ := by
-  simp [BuildKey.isModuleKey]
-
-@[inline] def module (self : BuildKey) (h : self.isModuleKey) : WfName :=
-  self.target <| by
-    unfold isModuleKey at h
-    exact of_decide_eq_true h |>.2
-
-@[inline] def isPackageKey (self : BuildKey) : Bool :=
-  self.hasPackage ∧ self.target? = none
-
-@[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
-  simp [BuildKey.isPackageKey]
-
-@[inline] def isTargetKey (self : BuildKey) : Bool :=
-  self.hasPackage ∧ self.hasTarget
-
-@[simp] theorem isTargetKey_mk : BuildKey.isTargetKey ⟨some p, some t, f⟩ := by
-  simp [BuildKey.isTargetKey]
-
-protected def toString : (self : BuildKey) → String
-| ⟨some p,  none,   f⟩ => s!"@{p}:{f}"
-| ⟨none,    some m, f⟩ => s!"+{m}:{f}"
-| ⟨some p,  some t, f⟩ => s!"{p}/{t}:{f}"
-| ⟨none,    none,   f⟩ => s!":{f}"
-
-instance : ToString BuildKey := ⟨(·.toString)⟩
-
-def quickCmp (k k' : BuildKey) :=
-  match Option.compareWith WfName.quickCmp k.package? k'.package? with
-  | .eq =>
-    match Option.compareWith WfName.quickCmp k.target? k'.target? with
-    | .eq => k.facet.quickCmp k'.facet
-    | ord => ord
-  | ord => ord
-
-theorem eq_of_quickCmp :
-{k k' : _} → quickCmp k k' = Ordering.eq → k = k' := by
-  intro ⟨p, t, f⟩ ⟨p', t', f'⟩
-  unfold quickCmp
-  simp only []
-  split
-  next p_eq =>
-    split
-    next t_eq =>
-      intro f_eq
-      have p_eq := eq_of_cmp p_eq
-      have t_eq := eq_of_cmp t_eq
-      have f_eq := eq_of_cmp f_eq
-      simp only [p_eq, t_eq, f_eq]
-    next =>
-      intros; contradiction
-  next =>
-    intros; contradiction
-
-instance : EqOfCmp BuildKey quickCmp where
-  eq_of_cmp := eq_of_quickCmp
-
-end BuildKey
-
--- ## Subtypes
-
-/-- The type of build keys for modules. -/
-structure ModuleBuildKey (fixedFacet : WfName) extends BuildKey where
-  is_module_key : toBuildKey.isModuleKey = true
-  facet_eq_fixed : toBuildKey.facet = fixedFacet
-
-instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
-
-@[inline] def BuildKey.toModuleKey
-(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
-  ⟨self, h, rfl⟩
-
-@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
-  self.toBuildKey.module self.is_module_key
-
-/-- The type of build keys for packages. -/
-structure PackageBuildKey (fixedFacet : WfName) extends BuildKey where
-  is_package_key : toBuildKey.isPackageKey = true
-  facet_eq_fixed : toBuildKey.facet = fixedFacet
-
-instance : Coe (PackageBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
-
-@[inline] def BuildKey.toPackageKey
-(self : BuildKey) (h : self.isPackageKey) : PackageBuildKey self.facet :=
-  ⟨self, h, rfl⟩
-
-@[inline] def PackageBuildKey.package (self : PackageBuildKey f) : WfName :=
-  self.toBuildKey.package <| by
-    have h := self.is_package_key
-    unfold BuildKey.isPackageKey at h
-    exact (of_decide_eq_true h).1
-
--- ## Constructor Helpers
-
-@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
-  ⟨⟨none, self.name, facet⟩, rfl, rfl⟩
-
-@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
-  ⟨⟨self.name, none, facet⟩, rfl, rfl⟩
-
--- # Build Data
-
-/--
-Build data associated with module facets in the Lake build store.
-For example a transitive × direct import pair for `imports` or an
-active build target for `lean.c`.
-
-It is a dynamic type, meaning additional alternatives can be add lazily
-as needed.
--/
-opaque ModuleData (facet : WfName) : Type
-
-/-- Build data associated with package facets (e.g., `extraDep`). -/
-opaque PackageData (facet : WfName) : Type
-
-/-- Build data associated with Lake targets (e.g., `extern_lib`). -/
-opaque TargetData (key : BuildKey) : Type
-
-/--
-The build data associated with the given key in the Lake build store.
-It is dynamic type composed of the three separate dynamic types for modules,
-packages, and targets.
--/
-def BuildData (key : BuildKey) :=
-  if key.isModuleKey then
-    ModuleData key.facet
-  else if key.isPackageKey then
-    PackageData key.facet
-  else
-    TargetData key
-
-/-- Macro for declaring new `PackageData`. -/
-scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
-"package_data " id:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``PackageData
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
-
-/-- Macro for declaring new `ModuleData`. -/
-scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
-"module_data " id:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``ModuleData
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
-
-/-- Lean binary build (`olean`, `ilean` files) -/
-module_data lean : ActiveOpaqueTarget
-
-/-- The `olean` file produced by `lean`  -/
-module_data olean : ActiveOpaqueTarget
-
-/-- The `ilean` file produced by `lean` -/
-module_data ilean : ActiveOpaqueTarget
-
-/-- The C file built from the Lean file via `lean` -/
-module_data lean.c : ActiveFileTarget
-
-/-- The object file built from `lean.c` -/
-module_data lean.o : ActiveFileTarget
-
-/-- Shared library for `--load-dynlib` -/
-module_data lean.dynlib : ActiveFileTarget
-
-/-- The direct × transitive imports of the Lean module. -/
-module_data lean.imports : Array Module × Array Module
-
-/-- The package's `extraDepTarget`. -/
-package_data extraDep : ActiveOpaqueTarget
-
--- # Build Store
-
-/-- A monad equipped with a Lake build store. -/
-abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
-
-instance (k : ModuleBuildKey f)
-[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    unfold BuildData
-    simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
-
-@[inline] instance [MonadBuildStore m]
-[DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
-  fetch? k := fetch? k.toBuildKey
-  store k a := store k.toBuildKey a
-
-instance (k : PackageBuildKey f)
-[t : DynamicType PackageData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    unfold BuildData, BuildKey.isModuleKey
-    have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
-    simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
-
-@[inline] instance [MonadBuildStore m]
-[DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
-  fetch? k := fetch? k.toBuildKey
-  store k a := store k.toBuildKey a
-
--- # Build Info
-
-inductive BuildInfo
-| module (module : Module) (facet : WfName)
-| package (package : Package) (facet : WfName)
-| externLib (package : Package) (externLib : ExternLibConfig)
-| target (package : Package) (target : WfName) (facet : WfName)
-
-def BuildInfo.key : (self : BuildInfo) → BuildKey
-| module m f => ⟨none, m.name, f⟩
-| package p f => ⟨p.name, none, f⟩
-| externLib p e => ⟨p.name, WfName.ofName e.name, &`externLib⟩
-| target p t f => ⟨p.name, t, f⟩
-
--- # Build Index
-
-/-- A build function for a single element of the Lake build index. -/
-abbrev IndexBuild (m) :=
-  DBuild BuildInfo (BuildData ·.key) m
-
-/-- A recursive build function for the Lake build index. -/
-abbrev RecIndexBuild (m) :=
-  DRecBuild BuildInfo (BuildData ·.key) m
-
-@[inline] def mkModuleBuild {facet : WfName} (build : Module → IndexBuild m → m α)
-[h : DynamicType ModuleData facet α] : Module → IndexBuild m → m (ModuleData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
-
-@[inline] def recBuildModuleFacet {m : Type → Type v}
-(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
-(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.module mod facet
-
-@[inline] def mkPackageBuild {facet : WfName} (build : Package → IndexBuild m → m α)
-[h : DynamicType PackageData facet α] : Package → IndexBuild m → m (PackageData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
-
-@[inline] def recBuildPackageFacet {m : Type → Type v}
-(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
-(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.package pkg facet
-
-abbrev ModuleBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
-    Module → IndexBuild m → m (ModuleData k)
-
-@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
-
-abbrev PackageBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
-    Package → IndexBuild m → m (PackageData k)
-
-@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
-
--- # Solo Module Targets
-
-def Module.soloTarget (mod : Module)
-(dynlibs : Array FilePath) (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 mod.leanArgs (← getLean)
-      modTrace.writeToFile mod.cTraceFile
-    else
-      unless modUpToDate do
-        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
-          (← getOleanPath) mod.pkg.rootDir dynlibs 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 (linkTargets : Array FileTarget) (self : Module) : FileTarget :=
-  leanSharedLibTarget self.dynlib linkTargets self.linkArgs
-
--- # Recursive Building
+-- # Index Recursive Build
 
 section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 
-/--
-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.recBuildLeanModule (mod : Module) (c : Bool)
-(recurse : IndexBuild m) : m ActiveOpaqueTarget := do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  let extraDepTarget ← recBuildPackageFacet mod.pkg &`extraDep recurse
-  let (imports, transImports) ← recBuildModuleFacet mod &`lean.imports recurse
-  let dynlibsTarget ←
-    if mod.shouldPrecompile then
-      ActiveTarget.collectArray
-        <| ← transImports.mapM (recBuildModuleFacet · &`lean.dynlib recurse)
-    else
-      pure <| ActiveTarget.nil.withInfo #[]
-  let importTarget ←
-    if c then
-      ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (recBuildModuleFacet · &`lean.c recurse)
-    else
-      ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (recBuildModuleFacet · &`lean recurse)
-  let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
-    <| ← dynlibsTarget.mixOpaqueAsync importTarget
-  let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
-  store (mod.mkBuildKey &`lean) modTarget
-  store (mod.mkBuildKey &`olean) modTarget
-  store (mod.mkBuildKey &`ilean) modTarget
-  if c then
-    let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
-    store (mod.mkBuildKey &`lean.c) cTarget
-    return cTarget.withoutInfo
-  else
-    return modTarget
-
-/--
-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.insert
-  -- Compute unique imports (direct × transitive)
-  &`lean.imports (mkModuleBuild <| fun mod recurse => do
-    let contents ← IO.FS.readFile mod.leanFile
-    let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
-    let importSet ← imports.foldlM (init := ModuleSet.empty) fun a imp => do
-      if let some mod ← findModule? imp.module then return a.insert mod else return a
-    let mut imports := #[]
-    let mut transImports := ModuleSet.empty
-    for imp in importSet do
-      let (_, impTransImports) ← recBuildModuleFacet imp &`lean.imports recurse
-      for imp in impTransImports do
-        transImports := transImports.insert imp
-      transImports := transImports.insert imp
-      imports := imports.push imp
-    return (imports, transImports.toArray)
-  ) |>.insert
-  -- Build module (`.olean` and `.ilean`)
-  &`lean (mkModuleBuild <| fun mod recurse => do
-    mod.recBuildLeanModule false recurse
-  ) |>.insert
-  &`olean (mkModuleBuild <| fun mod recurse => do
-    recBuildModuleFacet mod &`lean recurse
-  ) |>.insert
-  &`ilean (mkModuleBuild <| fun mod recurse => do
-    recBuildModuleFacet mod &`lean recurse
-  ) |>.insert
-  -- Build module `.c` (and `.olean` and `.ilean`)
-  &`lean.c (mkModuleBuild <| fun mod recurse => do
-    mod.recBuildLeanModule true recurse <&> (·.withInfo mod.cFile)
-  ) |>.insert
-  -- Build module `.o`
-  &`lean.o (mkModuleBuild <| fun mod recurse => do
-    let cTarget ← recBuildModuleFacet mod &`lean.c recurse
-    mod.mkOTarget (Target.active cTarget) |>.activate
-  ) |>.insert
-  -- Build shared library for `--load-dynlb`
-  &`lean.dynlib (mkModuleBuild <| fun mod recurse => do
-    let oTarget ← recBuildModuleFacet mod &`lean.o recurse
-    let dynlibTargets ←
-      if mod.shouldPrecompile then
-        let (_, transImports) ← recBuildModuleFacet mod &`lean.imports recurse
-        transImports.mapM fun mod => recBuildModuleFacet mod &`lean.dynlib recurse
-      else
-        pure #[]
-    -- TODO: Link in external libraries
-    -- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate)
-    -- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active
-    let linkTargets := #[oTarget] ++ dynlibTargets |>.map Target.active
-    mod.mkDynlibTarget linkTargets |>.activate
-  )
-
-/--
-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.insert
-  -- Build the `extraDepTarget` for the package and its transitive dependencies
-  &`extraDep (mkPackageBuild <| fun pkg recurse => do
-    let mut target := ActiveTarget.nil
-    for dep in pkg.dependencies do
-      if let some depPkg ← findPackage? dep.name then
-        let extraDepTarget ← recBuildPackageFacet depPkg &`extraDep recurse
-        target ← target.mixOpaqueAsync extraDepTarget
-    target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
-  )
-
-/-- Recursive builder for anything in the Lake build index. -/
-@[specialize] def recBuildIndex : RecIndexBuild m := fun info recurse => do
-  have : MonadLift BuildM m := ⟨liftM⟩
-  match info with
-  | .module mod facet =>
-    if let some build := moduleBuildMap.find? facet then
-      build mod recurse
-    else
-      error s!"do not know how to build module facet `{facet}`"
-  | .package pkg facet =>
-    if let some build := packageBuildMap.find? facet then
-      build pkg recurse
-    else
-      error s!"do not know how to build package facet `{facet}`"
-  | _ =>
-    error s!"do not know how to build `{info.key}`"
-
-/--
-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
-
 /--
 Build the module's specified facet recursively using a topological-based
 scheduler, storing the results in the monad's store and returning the result
@@ -548,36 +31,9 @@ scheduler, storing the results in the monad's store and returning nothing.
 @[inline] def buildModuleTop' (mod : Module) (facet : WfName) : CycleT BuildKey m PUnit :=
   discard <| buildIndexTop (m := m) <| BuildInfo.module mod facet
 
-/--
-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.
--/
-@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
-[h : DynamicType PackageData facet α] : CycleT BuildKey m α  :=
-  have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
-  cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
-
 end
 
--- ## Build Store
-
-abbrev BuildStore :=
-  DRBMap BuildKey BuildData BuildKey.quickCmp
-
-@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
-
--- ## Facet Builders
-
-/--
-Recursively build the specified facet of the given package,
-returning the result.
--/
-def buildPackageFacet
-(pkg : Package) (facet : WfName)
-[DynamicType PackageData facet α] : BuildM α := do
-  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    buildPackageTop pkg facet
+-- # Module Facet Builders
 
 /--
 Recursively build the specified facet of the given module,
@@ -617,3 +73,21 @@ def buildModuleFacetMap
         simp [h, eq_dynamic_type]
       res := res.insert (k.module h.1) <| cast of_data v
   return res
+
+-- # 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
diff --git a/Lake/Build/Module1.lean b/Lake/Build/Module1.lean
new file mode 100644
index 0000000000..72f5af7c58
--- /dev/null
+++ b/Lake/Build/Module1.lean
@@ -0,0 +1,134 @@
+/-
+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 Std System
+open Lean hiding SearchPath
+
+namespace Lake
+
+abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
+@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
+
+abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
+@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
+
+-- # Solo Module Targets
+
+def Module.soloTarget (mod : Module)
+(dynlibs : Array FilePath) (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 mod.leanArgs (← getLean)
+      modTrace.writeToFile mod.cTraceFile
+    else
+      unless modUpToDate do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
+          (← getOleanPath) mod.pkg.rootDir dynlibs 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 (linkTargets : Array FileTarget) (self : Module) : FileTarget :=
+  leanSharedLibTarget self.dynlib linkTargets self.linkArgs
+
+-- # Recursive Building
+
+section
+variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
+
+/--
+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)
+(recurse : IndexBuildFn m) : m ActiveOpaqueTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep recurse
+  let (imports, transImports) ← mod.recBuildFacet &`lean.imports recurse
+  let dynlibsTarget ←
+    if mod.shouldPrecompile then
+      ActiveTarget.collectArray
+        <| ← transImports.mapM (·.recBuildFacet &`lean.dynlib recurse)
+    else
+      pure <| ActiveTarget.nil.withInfo #[]
+  let importTarget ←
+    if c then
+      ActiveTarget.collectOpaqueArray
+        <| ← imports.mapM (·.recBuildFacet &`lean.c recurse)
+    else
+      ActiveTarget.collectOpaqueArray
+        <| ← imports.mapM (·.recBuildFacet &`lean recurse)
+  let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
+    <| ← dynlibsTarget.mixOpaqueAsync importTarget
+  let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
+  store (mod.mkBuildKey &`lean) modTarget
+  store (mod.mkBuildKey &`olean) modTarget
+  store (mod.mkBuildKey &`ilean) modTarget
+  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)
+(recurse : IndexBuildFn m) : m (Array Module × Array Module) := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let contents ← IO.FS.readFile mod.leanFile
+  let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
+  let importSet ← imports.foldlM (init := ModuleSet.empty) fun a imp => do
+    if let some mod ← findModule? imp.module then return a.insert mod else return a
+  let mut imports := #[]
+  let mut transImports := ModuleSet.empty
+  for imp in importSet do
+    let (_, impTransImports) ← imp.recBuildFacet &`lean.imports recurse
+    for imp in impTransImports do
+      transImports := transImports.insert imp
+    transImports := transImports.insert imp
+    imports := imports.push imp
+  return (imports, transImports.toArray)
+
+/--
+Recursively build the shared library of a module (e.g., for `--load-dynlib`).
+-/
+@[specialize] def Module.recBuildDynLib (mod : Module)
+(recurse : IndexBuildFn m) : m ActiveFileTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let oTarget ← mod.recBuildFacet &`lean.o recurse
+  let dynlibTargets ←
+    if mod.shouldPrecompile then
+      let (_, transImports) ← mod.recBuildFacet &`lean.imports recurse
+      transImports.mapM fun mod => mod.recBuildFacet &`lean.dynlib recurse
+    else
+      pure #[]
+  -- TODO: Link in external libraries
+  -- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate)
+  -- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active
+  let linkTargets := #[oTarget] ++ dynlibTargets |>.map Target.active
+  mod.mkDynlibTarget linkTargets |>.activate
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
deleted file mode 100644
index 22f1a14969..0000000000
--- a/Lake/Build/Package.lean
+++ /dev/null
@@ -1,93 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
--/
-import Lake.Build.Module
-
-open Std System
-open Lean hiding SearchPath
-
-namespace Lake
-
--- # Build Packages
-
--- # Build Package Modules
-
-
-
-def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
-  return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
-
-/--
-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 Package.buildLibModules
-(self : Package) (lib : LeanLibConfig) (facet : WfName)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
-  let buildMods : BuildM _ := do
-    let mods ← self.getLibModuleArray lib
-    let modTargets ← buildModuleFacetArray mods facet
-    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
-  buildMods.catchFailure fun _ => pure <| failure
-
-def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
-  Target.opaque <| self.buildLibModules lib &`lean
-
-def Package.libTarget (self : Package) : OpaqueTarget :=
-  self.mkLibTarget self.builtinLibConfig
-
--- # Build Specific Modules of the Package
-
-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
-
--- # Build Imports
-
-/--
-Construct an `Array` of `Module`s for the workspace-local modules of
-a `List` of import strings.
--/
-def Workspace.processImportList
-(imports : List String) (self : Workspace) : Array Module := Id.run do
-  let mut localImports := #[]
-  for imp in imports do
-    if let some mod := self.findModule? imp.toName then
-      localImports := localImports.push mod
-  return localImports
-
-/--
-Build the workspace-local modules of list of imports.
-
-Build only module `.olean` and `.ilean` files if
-the default package build does not include any binary targets
-Otherwise, also build `.c` files.
--/
-def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
-  if imports.isEmpty then
-    -- build the package's (and its dependencies') `extraDepTarget`
-    buildPackageFacet self &`extraDep >>= (·.buildOpaque)
-  else
-    -- build local imports from list
-    let mods := (← getWorkspace).processImportList imports
-    if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
-      let targets ← buildModuleFacetArray mods &`lean
-      targets.forM (·.buildOpaque)
-    else
-      let targets ← buildModuleFacetArray mods &`lean.c
-      targets.forM (·.buildOpaque)
diff --git a/Lake/Build/Recursive.lean b/Lake/Build/Recursive.lean
deleted file mode 100644
index 2a9f0a6b07..0000000000
--- a/Lake/Build/Recursive.lean
+++ /dev/null
@@ -1,101 +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 Lake.Util.DRBMap
-
-open Std
-namespace Lake
-
---------------------------------------------------------------------------------
--- # Build Store
---------------------------------------------------------------------------------
-
-/-- A monad equipped with a dependently typed key-value store for a particular key. -/
-class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
-  fetch? : m (Option α)
-  store : α → m PUnit
-
-export MonadStore1 (fetch? store)
-
-/-- A monad equipped with a dependently typed key-object store. -/
-class MonadDStore (κ : Type u) (β : outParam $ κ → Type v) (m : Type v → Type w) where
-  fetch? : (key : κ) → m (Option (β key))
-  store : (key : κ) → β key → m PUnit
-
-instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
-  fetch? := MonadDStore.fetch? k
-  store o := MonadDStore.store k o
-
-/-- A monad equipped with a key-object store. -/
-abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
-
-instance [MonadLiftT m n] [MonadDStore κ β m] : MonadDStore κ β n where
-  fetch? k := liftM (m := m) <| fetch? k
-  store k a := liftM (m := m) <| store k a
-
-instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
-  fetch? k := return (← get).find? k
-  store k a :=  modify (·.insert k a)
-
-instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
-  fetch? k := return (← get).find? k
-  store k a := modify (·.insert k a)
-
---------------------------------------------------------------------------------
--- # Topological / Suspending Builder
---------------------------------------------------------------------------------
-
--- ## Abstractions
-
-/-- A dependently typed object builder. -/
-abbrev DBuild.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
-  (i : ι) → m (β i)
-
-/-- A dependently typed recursive object builder. -/
-abbrev DRecBuild.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
-  (i : ι) → DBuild ι β m → m (β i)
-
-/-- A recursive object builder. -/
-abbrev RecBuild ι α m := DRecBuild ι (fun _ => α) m
-
-/-- `ExceptT` for build cycles. -/
-abbrev CycleT (κ) :=
-  ExceptT (List κ)
-
--- ## Algorithm
-
-/-- Auxiliary function for `buildTop`. -/
-@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]
-(parents : List κ) (keyOf : ι → κ) (build : DRecBuild ι (β ∘ keyOf) (CycleT κ m))
-(info : ι) : CycleT κ m (β (keyOf info)) := do
-  let key := keyOf info
-  -- return previous output if already built
-  if let some output ← fetch? key then
-    return output
-  -- detect cyclic builds
-  if parents.contains key then
-    throw <| key :: (parents.partition (· != key)).1 ++ [key]
-  -- build the key recursively
-  let output ← build info <| buildTopCore (key :: parents) keyOf build
-  -- save the output (to prevent repeated builds of the same key)
-  store key output
-  return output
-
-/-- Dependently typed version of `buildTop`. -/
-@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
-(keyOf : ι → κ) (build : DRecBuild ι (β ∘ keyOf) (CycleT κ m))
-(info : ι) : CycleT κ m (β (keyOf info)) :=
-  buildTopCore [] keyOf build info
-
-/--
-Recursively fills a `MonadStore` of key-object pairs by
-building objects topologically (ι.e., via a depth-first search with memoization).
-If a cycle is detected, the list of keys traversed is thrown.
-
-Called a suspending scheduler in "Build systems à la carte".
--/
-@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ α m]
-(keyOf : ι → κ) (build : RecBuild ι α (CycleT κ m)) (info : ι) : CycleT κ m α :=
-  buildDTop (fun _ => α) keyOf build info
diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean
new file mode 100644
index 0000000000..d3bb6a874d
--- /dev/null
+++ b/Lake/Build/Store.lean
@@ -0,0 +1,50 @@
+/-
+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.Data
+import Lake.Build.Topological
+import Lake.Util.StoreInsts
+
+/-!
+# The Lake Build Store
+
+The Lake build store is the map of Lake build keys to build task and/or
+build results that is slowly filled during a recursive build (e.g., via
+topological-based build of an initial key's dependencies).
+-/
+
+namespace Lake
+
+/-- The type of the Lake build store. -/
+abbrev BuildStore :=
+  DRBMap BuildKey BuildData BuildKey.quickCmp
+
+@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
+
+/-- A monad equipped with a Lake build store. -/
+abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
+
+instance (k : ModuleBuildKey f)
+[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
+  eq_dynamic_type := by
+    unfold BuildData
+    simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
+
+@[inline] instance [MonadBuildStore m]
+[DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
+  fetch? k := fetch? k.toBuildKey
+  store k a := store k.toBuildKey a
+
+instance (k : PackageBuildKey f)
+[t : DynamicType PackageData f α] : DynamicType BuildData k α where
+  eq_dynamic_type := by
+    unfold BuildData, BuildKey.isModuleKey
+    have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
+    simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
+
+@[inline] instance [MonadBuildStore m]
+[DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
+  fetch? k := fetch? k.toBuildKey
+  store k a := store k.toBuildKey a
diff --git a/Lake/Build/Topological.lean b/Lake/Build/Topological.lean
new file mode 100644
index 0000000000..9ef29e150b
--- /dev/null
+++ b/Lake/Build/Topological.lean
@@ -0,0 +1,70 @@
+/-
+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.Util.Store
+
+/-!
+# Topological / Suspending Recursive Builder
+
+This module defines a recursive build function that topologically
+(ι.e., via a depth-first search with memoization) builds the elements of
+a build store.
+
+This is called a suspending scheduler in *Build systems à la carte*.
+-/
+
+open Std
+namespace Lake
+
+-- ## Abstractions
+
+/-- A dependently typed object builder. -/
+abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
+  (i : ι) → m (β i)
+
+/-- A dependently typed recursive object builder. -/
+abbrev DRecBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
+  (i : ι) → DBuildFn ι β m → m (β i)
+
+/-- A recursive object builder. -/
+abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m
+
+/-- `ExceptT` for build cycles. -/
+abbrev CycleT (κ) :=
+  ExceptT (List κ)
+
+-- ## Algorithm
+
+/-- Auxiliary function for `buildTop`. -/
+@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]
+(parents : List κ) (keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
+(info : ι) : CycleT κ m (β (keyOf info)) := do
+  let key := keyOf info
+  -- return previous output if already built
+  if let some output ← fetch? key then
+    return output
+  -- detect cyclic builds
+  if parents.contains key then
+    throw <| key :: (parents.partition (· != key)).1 ++ [key]
+  -- build the key recursively
+  let output ← build info <| buildTopCore (key :: parents) keyOf build
+  -- save the output (to prevent repeated builds of the same key)
+  store key output
+  return output
+
+/-- Dependently typed version of `buildTop`. -/
+@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
+(keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
+(info : ι) : CycleT κ m (β (keyOf info)) :=
+  buildTopCore [] keyOf build info
+
+/--
+Recursively fills a `MonadStore` of key-object pairs by
+building objects topologically (ι.e., via a depth-first search with memoization).
+If a cycle is detected, the list of keys traversed is thrown.
+-/
+@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ α m]
+(keyOf : ι → κ) (build : RecBuildFn ι α (CycleT κ m)) (info : ι) : CycleT κ m α :=
+  buildDTop (fun _ => α) keyOf build info
diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean
index 0cdfaf54bb..e2e5916460 100644
--- a/Lake/Config/Resolve.lean
+++ b/Lake/Config/Resolve.lean
@@ -5,10 +5,11 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Git
 import Lake.Util.EStateT
+import Lake.Util.StoreInsts
 import Lake.Config.Load
 import Lake.Config.Manifest
 import Lake.Config.Workspace
-import Lake.Build.Recursive
+import Lake.Build.Topological
 
 open Std System
 open Lean (Name NameMap)
diff --git a/Lake/Util/DynamicType.lean b/Lake/Util/DynamicType.lean
new file mode 100644
index 0000000000..a935de9823
--- /dev/null
+++ b/Lake/Util/DynamicType.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Parser.Command
+
+open Lean
+namespace Lake
+
+class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
+  eq_dynamic_type : Δ a = β
+
+export DynamicType (eq_dynamic_type)
+
+@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
+  cast eq_dynamic_type.symm b
+
+@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
+  cast eq_dynamic_type b
+
+/--
+The syntax:
+
+```lean
+dynamic_data foo : Data 0 := Nat
+```
+
+Declares a new alternative for the dynamic `Data` type via the
+production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
+that uses this axiom for key `0`.
+-/
+scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
+"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
+  let tid := extractMacroScopes dty.getId |>.name
+  if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
+    let app := Syntax.mkApp dty #[key]
+    let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
+    `($[$doc?]? @[simp] axiom $axm : $app = $ty
+    instance : DynamicType $dty $key $ty := ⟨$axm⟩)
+  else
+    Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
diff --git a/Lake/Util/Store.lean b/Lake/Util/Store.lean
new file mode 100644
index 0000000000..686bb919fd
--- /dev/null
+++ b/Lake/Util/Store.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+namespace Lake
+
+/-- A monad equipped with a dependently typed key-value store for a particular key. -/
+class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
+  fetch? : m (Option α)
+  store : α → m PUnit
+
+export MonadStore1 (fetch? store)
+
+/-- A monad equipped with a dependently typed key-object store. -/
+class MonadDStore (κ : Type u) (β : outParam $ κ → Type v) (m : Type v → Type w) where
+  fetch? : (key : κ) → m (Option (β key))
+  store : (key : κ) → β key → m PUnit
+
+instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
+  fetch? := MonadDStore.fetch? k
+  store o := MonadDStore.store k o
+
+/-- A monad equipped with a key-object store. -/
+abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
+
+instance [MonadLiftT m n] [MonadDStore κ β m] : MonadDStore κ β n where
+  fetch? k := liftM (m := m) <| fetch? k
+  store k a := liftM (m := m) <| store k a
diff --git a/Lake/Util/StoreInsts.lean b/Lake/Util/StoreInsts.lean
new file mode 100644
index 0000000000..4774dfa516
--- /dev/null
+++ b/Lake/Util/StoreInsts.lean
@@ -0,0 +1,23 @@
+/-
+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.Util.DRBMap
+import Lake.Util.DynamicType
+import Lake.Util.Store
+
+open Std
+namespace Lake
+
+instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a :=  modify (·.insert k a)
+
+instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
+  fetch? k := return (← get).find? k
+  store k a := modify (·.insert k a)
+
+@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
+  fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
+  store a := store k <| cast t.eq_dynamic_type.symm a