diff --git a/Lake/Build/Binary.lean b/Lake/Build/Binary.lean
index 9d0ffb3..99766ec 100644
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Binary.lean
@@ -19,10 +19,9 @@ def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Packag
 def Package.mkStaticLibTarget (lib : LeanLibConfig) (self : Package) : FileTarget :=
   let libFile := self.libDir / lib.staticLibFileName
   BuildTarget.mk' libFile do
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let mods ← self.getLibModuleArray lib
-      let oFileTargets := self.localTargetsOf <| ← buildModuleMap mods &`lean.o
-      staticLibTarget libFile oFileTargets |>.materializeAsync
+    let mods ← self.getLibModuleArray lib
+    let oFileTargets := self.localTargetsOf <| ← buildModuleFacetMap mods &`lean.o
+    staticLibTarget libFile oFileTargets |>.materializeAsync
 
 protected def Package.staticLibTarget (self : Package) : FileTarget :=
   self.mkStaticLibTarget self.builtinLibConfig
@@ -46,11 +45,10 @@ def Package.linkTargetsOf
 def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget :=
   let libFile := self.libDir / lib.sharedLibFileName
   BuildTarget.mk' libFile do
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let mods ← self.getLibModuleArray lib
-      let linkTargets ← self.linkTargetsOf <| ← buildModuleMap mods &`lean.o
-      let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
-      target.materializeAsync
+    let mods ← self.getLibModuleArray lib
+    let linkTargets ← self.linkTargetsOf <| ← buildModuleFacetMap mods &`lean.o
+    let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
+    target.materializeAsync
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
   self.mkSharedLibTarget self.builtinLibConfig
@@ -61,18 +59,17 @@ 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⟩
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let cTargetMap ← buildModuleMap #[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
+    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/Context.lean b/Lake/Build/Context.lean
index 6abff34..5fb2491 100644
--- a/Lake/Build/Context.lean
+++ b/Lake/Build/Context.lean
@@ -22,7 +22,6 @@ abbrev Job := BuildTask BuildTrace
 /-- A Lake context with some additional caching for builds. -/
 structure BuildContext extends Context where
   leanTrace : BuildTrace
-  extraDepJob : Job := pure nilTrace
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 5bf3823..b430211 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -35,110 +35,328 @@ export DynamicType (eq_dynamic_type)
 @[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
   cast eq_dynamic_type b
 
-@[inline]
-instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
-  fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
-  store o := store k <| cast t.eq_dynamic_type.symm o
+/--
+The syntax:
 
--- ## For Facets
+```lean
+dynamic_data foo : Data 0 := Nat
+```
 
-opaque FacetData : WfName → Type
+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}'"
 
-macro "register_facet_data " id:ident " : " ty:term : command =>
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  let axm := mkIdent <| ``FacetData ++ id.getId
-  `(@[simp] axiom $axm : FacetData $key = $ty
-  instance : DynamicType FacetData $key $ty := ⟨$axm⟩)
-
-register_facet_data lean : ActiveOpaqueTarget
-register_facet_data olean : ActiveOpaqueTarget
-register_facet_data ilean : ActiveOpaqueTarget
-register_facet_data lean.c : ActiveFileTarget
-register_facet_data lean.o : ActiveFileTarget
-register_facet_data lean.dynlib : ActiveFileTarget
-register_facet_data lean.imports : Array Module × Array Module
-register_facet_data lean.extraDep : ActiveOpaqueTarget
+@[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
 
-structure ModuleBuildKey where
-  module : WfName
+/-- 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 ModuleBuildKey
+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]
 
-def quickCmp (lhs rhs : ModuleBuildKey) :=
-  match lhs.module.quickCmp rhs.module with
-  | .eq => lhs.facet.quickCmp rhs.facet
+@[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 ⟨m, f⟩ ⟨m', f'⟩
+  intro ⟨p, t, f⟩ ⟨p', t', f'⟩
   unfold quickCmp
+  simp only []
   split
-  next mod_eq =>
-    intro facet_eq
-    let mod_eq := WfName.eq_of_quickCmp mod_eq
-    let facet_eq := WfName.eq_of_quickCmp facet_eq
-    simp only [mod_eq, facet_eq]
+  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 ModuleBuildKey quickCmp where
+instance : EqOfCmp BuildKey quickCmp where
   eq_of_cmp := eq_of_quickCmp
 
-protected def toString (self : ModuleBuildKey) :=
-  s!"{self.module}:{self.facet}"
+end BuildKey
 
-instance : ToString ModuleBuildKey := ⟨(·.toString)⟩
+-- ## Subtypes
 
-end ModuleBuildKey
+/-- 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
 
--- ## Static Keys
+instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
 
-abbrev DModuleBuildKey (facet : WfName) :=
-  {k : ModuleBuildKey // k.facet = facet}
+@[inline] def BuildKey.toModuleKey
+(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
+  ⟨self, h, rfl⟩
 
-def Module.mkBuildKey (facet : WfName) (self : Module) : DModuleBuildKey facet :=
-  ⟨⟨self.name, facet⟩, rfl⟩
+@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
+  self.toBuildKey.module self.is_module_key
 
-abbrev ModuleBuildKeyData (key : ModuleBuildKey) := FacetData key.facet
+/-- 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
 
-@[inline]
-instance [MonadDStore ModuleBuildKey ModuleBuildKeyData m]
-[h : DynamicType FacetData f α] : MonadStore (DModuleBuildKey f) α m where
-  fetch? k :=
-    let of_data := by
-      unfold ModuleBuildKeyData
-      rw [k.property, h.eq_dynamic_type]
-    cast of_data <| MonadDStore.fetch? (m := m) k.val
-  store k o :=
-    let to_data := by
-      unfold ModuleBuildKeyData
-      rw [k.property, h.eq_dynamic_type]
-    MonadDStore.store (m := m) k.val <| cast to_data o
-
--- # Module Build Info
-
-structure ModuleBuildInfo extends Module where
-  facet : WfName
+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
 
-instance : Coe ModuleBuildInfo Module := ⟨(·.toModule)⟩
+/-- The C file built from the Lean file via `lean` -/
+module_data lean.c : ActiveFileTarget
 
-def ModuleBuildInfo.buildKey (self : ModuleBuildInfo) : DModuleBuildKey self.facet :=
-  self.mkBuildKey self.facet
+/-- The object file built from `lean.c` -/
+module_data lean.o : ActiveFileTarget
 
-structure DModuleBuildInfo (facet : WfName) extends ModuleBuildInfo where
-  law : toModuleBuildInfo.facet = facet
+/-- Shared library for `--load-dynlib` -/
+module_data lean.dynlib : ActiveFileTarget
 
-instance : Coe (DModuleBuildInfo k) ModuleBuildInfo := ⟨(·.toModuleBuildInfo)⟩
+/-- The direct × transitive imports of the Lean module. -/
+module_data lean.imports : Array Module × Array Module
 
-abbrev Module.mkFacetInfo (facet : WfName) (self : Module) : DModuleBuildInfo facet :=
-  ⟨⟨self, facet⟩, rfl⟩
+/-- The package's `extraDepTarget`. -/
+package_data extraDep : ActiveOpaqueTarget
 
-abbrev ModuleBuildData (info : ModuleBuildInfo) := FacetData info.facet
+-- # 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
 
@@ -176,50 +394,31 @@ def Module.mkDynlibTarget (linkTargets : Array FileTarget) (self : Module) : Fil
 
 -- # Recursive Building
 
-abbrev ModuleBuild (m) :=
-  DBuild ModuleBuildInfo ModuleBuildData m
-
-abbrev FacetBuildMap (m : Type → Type v) :=
-  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
-    Module → ModuleBuild m → m (FacetData k)
-
-@[inline] def FacetBuildMap.empty : FacetBuildMap m := DRBMap.empty
-
-@[inline] def mkFacetBuild {facet : WfName} (build : Module → ModuleBuild m → m α)
-[h : DynamicType FacetData facet α] : Module → ModuleBuild m → m (FacetData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
-
-@[inline] def buildFacet {m : Type → Type v}
-(mod : Module) (facet : WfName) [DynamicType FacetData facet α]
-(build : (info : ModuleBuildInfo) → m (ModuleBuildData info)) : m α :=
-  cast (by simp only [ModuleBuildData, eq_dynamic_type]) (build ⟨mod, facet⟩)
-
 section
-variable [Monad m] [MonadLiftT BuildM m]
-  [MonadDStore ModuleBuildKey ModuleBuildKeyData m]
+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`.
 -/
-@[inline] def Module.recBuildLeanModule (mod : Module) (c : Bool)
-(recurse : ModuleBuild m) : m ActiveOpaqueTarget := do
+@[specialize] def Module.recBuildLeanModule (mod : Module) (c : Bool)
+(recurse : IndexBuild m) : m ActiveOpaqueTarget := do
   have : MonadLift BuildM m := ⟨liftM⟩
-  let extraDepTarget ← buildFacet mod &`lean.extraDep recurse
-  let (imports, transImports) ← buildFacet mod &`lean.imports recurse
+  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 (buildFacet · &`lean.dynlib recurse)
+        <| ← transImports.mapM (recBuildModuleFacet · &`lean.dynlib recurse)
     else
       pure <| ActiveTarget.nil.withInfo #[]
   let importTarget ←
     if c then
       ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (buildFacet · &`lean.c recurse)
+        <| ← imports.mapM (recBuildModuleFacet · &`lean.c recurse)
     else
       ActiveTarget.collectOpaqueArray
-        <| ← imports.mapM (buildFacet · &`lean recurse)
+        <| ← imports.mapM (recBuildModuleFacet · &`lean recurse)
   let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
     <| ← dynlibsTarget.mixOpaqueAsync importTarget
   let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
@@ -234,18 +433,14 @@ optionally outputting a `.c` file as well if `c` is set to `true`.
     return modTarget
 
 /--
-A facet name to build function map that contains builders
-for the initial set of Lake module facets (i.e. `lean.{imports, c, o, dynlib]`).
+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 facetBuildMap : FacetBuildMap m :=
+@[specialize] def moduleBuildMap : ModuleBuildMap m :=
   have : MonadLift BuildM m := ⟨liftM⟩
-  FacetBuildMap.empty.insert
-  -- Get extra module dependency job (i.e., for package dependencies)
-  &`lean.extraDep (mkFacetBuild <| fun _  _ => do
-    return ActiveTarget.opaque <| (← read).extraDepJob
-  ) |>.insert
+  ModuleBuildMap.empty.insert
   -- Compute unique imports (direct × transitive)
-  &`lean.imports (mkFacetBuild <| fun mod recurse => do
+  &`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
@@ -253,7 +448,7 @@ for the initial set of Lake module facets (i.e. `lean.{imports, c, o, dynlib]`).
     let mut imports := #[]
     let mut transImports := ModuleSet.empty
     for imp in importSet do
-      let (_, impTransImports) ← buildFacet imp &`lean.imports recurse
+      let (_, impTransImports) ← recBuildModuleFacet imp &`lean.imports recurse
       for imp in impTransImports do
         transImports := transImports.insert imp
       transImports := transImports.insert imp
@@ -261,32 +456,33 @@ for the initial set of Lake module facets (i.e. `lean.{imports, c, o, dynlib]`).
     return (imports, transImports.toArray)
   ) |>.insert
   -- Build module (`.olean` and `.ilean`)
-  &`lean (mkFacetBuild <| fun mod recurse => do
+  &`lean (mkModuleBuild <| fun mod recurse => do
     mod.recBuildLeanModule false recurse
   ) |>.insert
-  &`olean (mkFacetBuild <| fun mod recurse => do
-    buildFacet mod &`lean recurse
+  &`olean (mkModuleBuild <| fun mod recurse => do
+    recBuildModuleFacet mod &`lean recurse
   ) |>.insert
-  &`ilean (mkFacetBuild <| fun mod recurse => do
-    buildFacet mod &`lean recurse
+  &`ilean (mkModuleBuild <| fun mod recurse => do
+    recBuildModuleFacet mod &`lean recurse
   ) |>.insert
   -- Build module `.c` (and `.olean` and `.ilean`)
-  &`lean.c (mkFacetBuild <| fun mod recurse => do
+  &`lean.c (mkModuleBuild <| fun mod recurse => do
     mod.recBuildLeanModule true recurse <&> (·.withInfo mod.cFile)
   ) |>.insert
   -- Build module `.o`
-  &`lean.o (mkFacetBuild <| fun mod recurse => do
-    let cTarget ← buildFacet mod &`lean.c recurse
+  &`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 (mkFacetBuild <| fun mod recurse => do
-    let oTarget ← buildFacet mod &`lean.o recurse
-    let dynlibTargets ← if mod.shouldPrecompile then
-      let (_, transImports) ← buildFacet mod &`lean.imports recurse
-      transImports.mapM fun mod => buildFacet mod &`lean.dynlib recurse
-    else
-      pure #[]
+  &`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
@@ -294,84 +490,130 @@ for the initial set of Lake module facets (i.e. `lean.{imports, c, o, dynlib]`).
     mod.mkDynlibTarget linkTargets |>.activate
   )
 
-/-- Recursively builder for module facets. -/
-@[inline] def recBuildModuleFacet : DRecBuild ModuleBuildInfo ModuleBuildData m :=
+/--
+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⟩
-  fun info recurse => do
-    if let some build := facetBuildMap.find? info.facet then
-      build info recurse
+  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 module facet `{info.facet}`"
+      error s!"do not know how to build package facet `{facet}`"
+  | _ =>
+    error s!"do not know how to build `{info.key}`"
 
-/-- Auxiliary function for `buildModuleTop` and `buildModuleTop'`. -/
-@[specialize] def buildModuleTopCore (mod : Module)
-(facet : WfName) : CycleT ModuleBuildKey m (FacetData facet) :=
-  let of_data := by
-    simp [ModuleBuildKeyData, ModuleBuildInfo.buildKey, Module.mkBuildKey]
-  cast of_data <| buildDTop (m := m) ModuleBuildKeyData (·.buildKey)
-    recBuildModuleFacet (ModuleBuildInfo.mk mod facet)
+/--
+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-sort
-based scheduler, storing the results in the monad's store and returning the
-result of the top-level build.
+Build the module's specified facet recursively using a topological-based
+scheduler, storing the results in the monad's store and returning the result
+of the top-level build.
 -/
 @[inline] def buildModuleTop (mod : Module) (facet : WfName)
-[h : DynamicType FacetData facet α] : CycleT ModuleBuildKey m α  :=
-  let of_data := by rw [h.eq_dynamic_type]
-  cast of_data <| buildModuleTopCore mod facet
+[h : DynamicType ModuleData facet α] : CycleT BuildKey m α  :=
+  have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
+  cast of_data <| buildIndexTop (m := m) <| BuildInfo.module mod facet
 
 /--
-Build the module's specified facet recursively using a topological-sort
-based scheduler, storing the results in the monad's store and returning nothing.
+Build the module's specified facet recursively using a topological-based
+scheduler, storing the results in the monad's store and returning nothing.
 -/
-@[inline] def buildModuleTop' (mod : Module) (facet : WfName) : CycleT ModuleBuildKey m PUnit  :=
-  discard <| buildModuleTopCore mod facet
+@[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
 
--- ## Module Map
+-- ## Build Store
+
+abbrev BuildStore :=
+  DRBMap BuildKey BuildData BuildKey.quickCmp
 
-abbrev ModuleFacetMap :=
-  DRBMap ModuleBuildKey ModuleBuildKeyData ModuleBuildKey.quickCmp
+@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
 
-def ModuleFacetMap.empty : ModuleFacetMap := DRBMap.empty
+-- ## Facet Builders
 
--- ## Multi-Module 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
 
 /--
 Recursively build the specified facet of the given module,
 returning the result.
 -/
-def buildModule (mod : Module) (facet : WfName) [DynamicType FacetData facet α] : BuildM α := do
-  failOnBuildCycle <| ← EStateT.run' ModuleFacetMap.empty do
+def buildModuleFacet
+(mod : Module) (facet : WfName)
+[DynamicType ModuleData facet α] : BuildM α := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
     buildModuleTop mod facet
 
 /--
 Recursively build the specified facet of each module,
 returning an `Array`  of the results.
 -/
-def buildModuleArray
+def buildModuleFacetArray
 (mods : Array Module) (facet : WfName)
-[DynamicType FacetData facet α] : BuildM (Array α) := do
-  failOnBuildCycle <|  ← EStateT.run' ModuleFacetMap.empty <| mods.mapM fun mod =>
+[DynamicType ModuleData facet α] : BuildM (Array α) := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty <| mods.mapM fun mod =>
     buildModuleTop mod facet
 
 /--
 Recursively build the specified facet of the given module,
 returning the resulting map of built modules and their results.
 -/
-def buildModuleMap
+def buildModuleFacetMap
 (mods : Array Module) (facet : WfName)
-[DynamicType FacetData facet α] : BuildM (NameMap α) := do
-  let (x, fullMap) ← EStateT.run ModuleFacetMap.empty <| mods.forM fun mod =>
+[DynamicType ModuleData facet α] : BuildM (NameMap α) := do
+  let (x, bStore) ← EStateT.run BuildStore.empty <| mods.forM fun mod =>
     buildModuleTop' mod facet
   failOnBuildCycle x
   let mut res : NameMap α := RBMap.empty
-  for ⟨k, v⟩ in fullMap do
-    if h : k.facet = facet then
+  for ⟨k, v⟩ in bStore do
+    if h : k.isModuleKey ∧ k.facet = facet then
       let of_data := by
-        unfold ModuleBuildKeyData
+        unfold BuildData
         simp [h, eq_dynamic_type]
-      res := res.insert k.module <| cast of_data v
+      res := res.insert (k.module h.1) <| cast of_data v
   return res
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index a5cefbe..22f1a14 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -12,31 +12,9 @@ namespace Lake
 
 -- # Build Packages
 
-/-- Build the `extraDepTarget` of all dependent packages into a single target. -/
-protected def Package.buildExtraDepsTarget (self : Package) : SchedulerM ActiveOpaqueTarget := do
-  let collect pkg depTargets := do
-    let extraDepTarget ← pkg.extraDepTarget.activate
-    let depTarget ← ActiveTarget.collectOpaqueArray depTargets
-    extraDepTarget.mixOpaqueAsync depTarget
-  let build dep recurse := do
-    let pkg := (← findPackage? dep.name).get!
-    let depTargets ← pkg.dependencies.mapM recurse
-    liftM <| collect pkg depTargets
-  let targetsE ← EStateT.run' (mkRBMap _ _ Name.quickCmp) <|
-    self.dependencies.mapM fun dep => buildTop Dependency.name build dep
-  match targetsE with
-  | Except.ok targets => collect self targets
-  | Except.error _ => panic! "dependency cycle emerged after resolution"
-
-/-- Build the `extraDepTarget` of all workspace packages into a single target. -/
-def buildExtraDepsTarget : SchedulerM ActiveOpaqueTarget := do
-  ActiveTarget.collectOpaqueArray <| ← do
-    (← getWorkspace).packageArray.mapM (·.extraDepTarget.activate)
-
 -- # Build Package Modules
 
-def withExtraDepTarget (depTarget : ActiveOpaqueTarget) (act : BuildT m α) : BuildT m α :=
-  fun ctx => act {ctx with extraDepJob := depTarget.task}
+
 
 def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
   return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
@@ -48,13 +26,12 @@ a single opaque target for the whole build.
 -/
 def Package.buildLibModules
 (self : Package) (lib : LeanLibConfig) (facet : WfName)
-[DynamicType FacetData facet (ActiveBuildTarget α)] : SchedulerM Job := do
-  withExtraDepTarget (← self.buildExtraDepsTarget) do
-    let buildMods : BuildM _ := do
-      let mods ← self.getLibModuleArray lib
-      let modTargets ← buildModuleArray mods facet
-      (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
-    buildMods.catchFailure fun _ => pure <| failure
+[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
@@ -65,10 +42,8 @@ def Package.libTarget (self : Package) : OpaqueTarget :=
 -- # Build Specific Modules of the Package
 
 def Module.facetTarget (facet : WfName) (self : Module)
-[DynamicType FacetData facet (ActiveBuildTarget α)] : OpaqueTarget :=
-  BuildTarget.mk' () do
-    withExtraDepTarget (← self.pkg.buildExtraDepsTarget) do
-      return (← buildModule self facet).task
+[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
@@ -104,16 +79,15 @@ 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
-  let depTarget ← self.buildExtraDepsTarget
   if imports.isEmpty then
-    -- wait for deps to finish building
-    depTarget.buildOpaque
+    -- 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 ← buildModuleArray mods &`lean
+      let targets ← buildModuleFacetArray mods &`lean
       targets.forM (·.buildOpaque)
     else
-      let targets ← buildModuleArray mods &`lean.c
+      let targets ← buildModuleFacetArray mods &`lean.c
       targets.forM (·.buildOpaque)
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 2c840a2..0165d08 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -3,7 +3,7 @@ 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 Std.Data.HashMap
+import Lake.Util.Name
 import Lake.Util.String
 import Lake.Build.TargetTypes
 import Lake.Config.Glob
@@ -274,6 +274,8 @@ structure Package where
   dir : FilePath
   /-- The package's configuration. -/
   config : PackageConfig
+  /-- The package's well-formed name. -/
+  name : WfName := WfName.ofName config.name
   /-- Scripts for the package. -/
   scripts : NameMap Script := {}
   /-- Lean library targets for the package. -/
@@ -324,10 +326,6 @@ def IOPackager := (pkgDir : FilePath) → (args : List String) → IO PackageCon
 
 namespace Package
 
-/-- The package's `name` configuration. -/
-def name (self : Package) : Name :=
-  self.config.name
-
 /-- The package's `dependencies` configuration. -/
 def dependencies (self : Package) : Array Dependency :=
   self.config.dependencies
diff --git a/Lake/Util/Compare.lean b/Lake/Util/Compare.lean
index 763df6f..1342c57 100644
--- a/Lake/Util/Compare.lean
+++ b/Lake/Util/Compare.lean
@@ -27,6 +27,12 @@ export EqOfCmpWrt (eq_of_cmp_wrt)
 instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
   eq_of_cmp_wrt h := by rw [eq_of_cmp h]
 
+instance [EqOfCmpWrt α id cmp] : EqOfCmp α cmp where
+  eq_of_cmp h := eq_of_cmp_wrt (f := id) h
+
+instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
+  eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
+
 instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩
 
 theorem eq_of_compareOfLessAndEq
@@ -50,3 +56,19 @@ theorem String.eq_of_compare
 
 instance : EqOfCmp String compare where
   eq_of_cmp h := String.eq_of_compare h
+
+@[inline]
+def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering
+| none,   none    => Ordering.eq
+| none,   some _  => Ordering.lt
+| some _, none    => Ordering.gt
+| some x, some y  => cmp x y
+
+theorem Option.eq_of_compareWith [EqOfCmp α cmp]
+{o o' : Option α} : compareWith cmp o o' = Ordering.eq → o = o' := by
+  unfold compareWith
+  cases o <;> cases o' <;> simp
+  exact eq_of_cmp
+
+instance [EqOfCmp α cmp] : EqOfCmp (Option α) (Option.compareWith cmp) where
+  eq_of_cmp h := Option.eq_of_compareWith h
diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean
index 71bbb31..4f5a80b 100644
--- a/Lake/Util/Name.lean
+++ b/Lake/Util/Name.lean
@@ -127,6 +127,10 @@ def anonymous : WfName :=
 
 instance : Inhabited WfName := ⟨anonymous⟩
 
+def isAnonymous : WfName → Bool
+| ⟨.anonymous, _⟩ => true
+| _ => false
+
 @[inline] def mkStr : WfName → String → WfName
 | ⟨p, h⟩, s => ⟨Name.mkStr p s, Name.WellFormed.strWff h rfl⟩
 
@@ -138,12 +142,20 @@ def ofName : Name → WfName
 | .str p s _ => mkStr (ofName p) s
 | .num p v _ => mkNum (ofName p) v
 
-protected def hash : WfName → UInt64
+@[inline] protected def toString (escape := true) : WfName → String
+| ⟨n, _⟩ => n.toString escape
+
+@[inline] protected def toStringWithSep (sep : String) (escape := true) : WfName → String
+| ⟨n, _⟩ => n.toStringWithSep sep escape
+
+instance : ToString WfName := ⟨(·.toString)⟩
+
+@[inline] protected def hash : WfName → UInt64
 | ⟨n, _⟩ => n.hash
 
 instance : Hashable WfName := ⟨WfName.hash⟩
 
-protected def beq : WfName → WfName → Bool
+@[inline] protected def beq : WfName → WfName → Bool
 | ⟨n, _⟩, ⟨n', _⟩ => n.beq n'
 
 instance : BEq WfName := ⟨WfName.beq⟩
@@ -195,7 +207,7 @@ instance : DecidableEq WfName :=
   | true  => isTrue (eq_of_beq_true h)
   | false => isFalse (ne_of_beq_false h)
 
-def quickCmp : WfName → WfName → Ordering
+@[inline] def quickCmp : WfName → WfName → Ordering
 | ⟨n, _⟩, ⟨n', _⟩ => n.quickCmp n'
 
 theorem eq_of_quickCmp :
diff --git a/Makefile b/Makefile
index 48b69b9..dfa5eea 100644
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,7 @@ clean: clean-build clean-tests clean-examples
 clean-tests: clean-62
 
 clean-examples: clean-init clean-hello clean-io clean-deps\
-	clean-git clean-ffi clean-targets clean-bootstrap
+	clean-git clean-ffi clean-targets clean-precompile clean-bootstrap
 
 .PHONY: all test test-ci test-tests test-examples\
 	clean clean-build clean-tests clean-examples build time-build check-lake\
@@ -95,7 +95,7 @@ clean-targets:
 test-precompile:
 	cd examples/precompile && ./test.sh
 
-clean-targets:
+clean-precompile:
 	cd examples/precompile && ./clean.sh
 
 test-scripts: