diff --git a/Lake/Build.lean b/Lake/Build.lean
index c25666172a..bdd4371910 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -5,6 +5,5 @@ Authors: Mac Malone
 -/
 import Lake.Build.Monad
 import Lake.Build.Actions
-import Lake.Build.LeanLib
-import Lake.Build.LeanExe
+import Lake.Build.LeanTarget
 import Lake.Build.Imports
diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index a911a6f971..2d0db0a5f8 100644
--- a/Lake/Build/Data.lean
+++ b/Lake/Build/Data.lean
@@ -23,21 +23,20 @@ opaque ModuleData (facet : WfName) : Type
 opaque PackageData (facet : WfName) : Type
 
 /-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
-opaque TargetData (key : BuildKey) : Type
-
+opaque TargetData (facet : WfName) : 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) :=
+abbrev BuildData (key : BuildKey) :=
   if key.isModuleKey then
     ModuleData key.facet
   else if key.isPackageKey then
     PackageData key.facet
   else
-    TargetData key
+    TargetData key.facet
 
 theorem isModuleKey_data {k : BuildKey}
 (h : k.isModuleKey = true) : BuildData k = ModuleData k.facet := by
@@ -52,8 +51,7 @@ instance (k : ModuleBuildKey f)
 theorem isPackageKey_data {k : BuildKey}
 (h : k.isPackageKey = true) : BuildData k = PackageData k.facet := by
   unfold BuildData, BuildKey.isModuleKey
-  have has_pkg := of_decide_eq_true (of_decide_eq_true h |>.1)
-  simp [has_pkg, h]
+  simp [of_decide_eq_true (of_decide_eq_true h |>.1), h]
 
 instance (k : PackageBuildKey f)
 [t : DynamicType PackageData f α] : DynamicType BuildData k α where
@@ -61,6 +59,12 @@ instance (k : PackageBuildKey f)
     have h := isPackageKey_data k.is_package_key
     simp [h, k.facet_eq_fixed, t.eq_dynamic_type]
 
+theorem isTargetKey_data {k : BuildKey}
+(h : k.isTargetKey = true) : BuildData k = TargetData k.facet := by
+  unfold BuildData, BuildKey.isModuleKey, BuildKey.isPackageKey
+  have ⟨has_p, has_t⟩ := of_decide_eq_true h
+  simp [of_decide_eq_true has_p, of_decide_eq_true has_t, h]
+
 /-- Macro for declaring new `PackageData`. -/
 scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do
@@ -74,3 +78,10 @@ scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
   let dty := mkCIdentFrom (← getRef) ``ModuleData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
   `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+
+/-- Macro for declaring new `TargetData`. -/
+scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
+"target_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
index a9a8b52c8f..7a9a4e7025 100644
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@@ -36,7 +36,7 @@ as "Lean-only". Otherwise, also build `.c` files.
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
-    buildPackageFacet self &`extraDep >>= (·.buildOpaque)
+    self.buildFacet &`extraDep >>= (·.buildOpaque)
     return #[]
   else
     -- build local imports from list
@@ -50,9 +50,9 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
         buildModuleTop mod &`lean.c <&> (·.withoutInfo)
     let importTargets ← failOnBuildCycle res
     let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
-    let externLibTargets := bStore.collectPackageFacetArray &`externSharedLibs
+    let externLibTargets := bStore.collectSharedExternLibs
     importTargets.forM (·.buildOpaque)
     let dynlibs ← dynlibTargets.mapM (·.build)
-    let externLibs ← externLibTargets.concatMapM (·.mapM (·.build))
+    let externLibs ← externLibTargets.mapM (·.build)
     -- Note: Lean wants the external library symbols before module symbols
     return  externLibs ++ dynlibs
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 1b445c81b9..cfb3e1c1a4 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Module1
+import Lake.Build.LeanTarget1
 import Lake.Build.Topological
 import Lake.Util.EStateT
 
@@ -38,6 +39,13 @@ abbrev PackageBuildMap (m : Type → Type v) :=
 
 @[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
 
+/-- A map from target facet names to build functions. -/
+abbrev TargetBuildMap (m : Type → Type v) :=
+  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
+    Package → IndexBuildFn m → m (PackageData k)
+
+@[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
+
 /-!
 ## Build Function Constructor Helpers
 -/
@@ -58,6 +66,14 @@ dynamically typed equivalent.
 [h : DynamicType PackageData facet α] : Package → IndexT m (PackageData facet) :=
   cast (by rw [← h.eq_dynamic_type]) build
 
+/--
+Converts a conveniently typed target build function into its
+dynamically typed equivalent.
+-/
+@[inline] def mkTargetBuild (facet : WfName) (build : IndexT m α)
+[h : DynamicType TargetData facet α] : IndexT m (TargetData facet) :=
+  cast (by rw [← h.eq_dynamic_type]) build
+
 section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 
@@ -127,15 +143,6 @@ the initial set of Lake package facets (e.g., `extraDep`).
         target ← target.mixOpaqueAsync extraDepTarget
     target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
   )
-  -- Build the `extern_lib` targets of the package
-  |>.insert &`externSharedLibs (mkPackageFacetBuild <| fun pkg => do
-    let mut targets := #[]
-    for (_, config) in pkg.externLibConfigs.toList do
-      let target := staticToLeanDynlibTarget config.target
-      targets := targets.push <| ← target.activate
-    return targets
-  )
-
 /-!
 ## Topologically-based Recursive Build Using the Index
 -/
@@ -154,6 +161,16 @@ the initial set of Lake package facets (e.g., `extraDep`).
       build pkg
     else
       error s!"do not know how to build package facet `{facet}`"
+  | .staticLeanLib lib =>
+    mkTargetBuild &`leanLib.static lib.recBuildStatic
+  | .sharedLeanLib lib =>
+    mkTargetBuild &`leanLib.shared lib.recBuildShared
+  | .leanExe exe =>
+    mkTargetBuild &`leanExe exe.recBuild
+  | .staticExternLib lib =>
+    mkTargetBuild &`externLib.static <| lib.target.activate
+  | .sharedExternLib lib =>
+    mkTargetBuild &`externLib.shared <| staticToLeanDynlibTarget (lib.target) |>.activate
   | _ =>
     error s!"do not know how to build `{info.key}`"
 
@@ -171,7 +188,9 @@ 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]
+  have of_data := by
+    unfold BuildData, BuildInfo.key, Package.mkBuildKey
+    simp [h.eq_dynamic_type]
   cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
 
 end
@@ -184,8 +203,7 @@ end
 Recursively build the specified facet of the given package,
 returning the result.
 -/
-def buildPackageFacet
-(pkg : Package) (facet : WfName)
+def Package.buildFacet (self : Package) (facet : WfName)
 [DynamicType PackageData facet α] : BuildM α := do
   failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    buildPackageTop pkg facet
+    buildPackageTop self facet
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index 441c82bcd4..ddadecf0b3 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Data
-import Lake.Config.Module
+import Lake.Config.LeanExe
+import Lake.Config.ExternLib
 import Lake.Util.EquipT
 
 namespace Lake
@@ -17,17 +18,42 @@ namespace Lake
 @[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
   ⟨⟨self.name, none, facet⟩, rfl, rfl⟩
 
+abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanLib.static⟩
+
+abbrev LeanLib.sharedBuildKey (self : LeanLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanLib.shared⟩
+
+abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanExe⟩
+
+abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`externLib.static⟩
+
+abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`externLib.shared⟩
+
 -- # Build Info
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo
 | module (module : Module) (facet : WfName)
 | package (package : Package) (facet : WfName)
+| staticLeanLib (lib : LeanLib)
+| sharedLeanLib (lib : LeanLib)
+| leanExe (exe : LeanExe)
+| staticExternLib (lib : ExternLib)
+| sharedExternLib (lib : ExternLib)
 | 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⟩
+| module m f => m.mkBuildKey f
+| package p f => p.mkBuildKey f
+| staticLeanLib l => l.staticBuildKey
+| sharedLeanLib l => l.sharedBuildKey
+| leanExe x => x.buildKey
+| staticExternLib l => l.staticBuildKey
+| sharedExternLib l => l.sharedBuildKey
 | target p t f => ⟨p.name, t, f⟩
 
 /-- A build function for any element of the Lake build index. -/
@@ -38,15 +64,29 @@ abbrev IndexBuildFn (m : Type → Type v) :=
 /-- A transformer to equip a monad with a build function for the Lake index. -/
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 
-@[inline] def Module.recBuildFacet (mod : Module) (facet : WfName)
+@[inline] def Module.recBuildFacet (self : Module) (facet : WfName)
 [DynamicType ModuleData facet α] : IndexT m α := fun build =>
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.module mod facet
+  let to_data := by
+    unfold BuildData, BuildInfo.key, Module.mkBuildKey
+    simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.module self facet
 
-@[inline] def Package.recBuildFacet (pkg : Package) (facet : WfName)
+@[inline] def Package.recBuildFacet (self : Package) (facet : WfName)
 [DynamicType PackageData facet α] : IndexT m α := fun build =>
+  let to_data := by
+    unfold BuildData, BuildInfo.key, Package.mkBuildKey
+    simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.package self facet
+
+@[inline] def ExternLib.recBuildStatic (self : ExternLib)
+[DynamicType TargetData &`externLib.static α] : IndexT m α := fun build =>
   let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.package pkg facet
+  cast to_data <| build <| BuildInfo.staticExternLib self
+
+@[inline] def ExternLib.recBuildShared (self : ExternLib)
+[DynamicType TargetData &`externLib.shared α] : IndexT m α := fun build =>
+  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.sharedExternLib self
 
 -- # Data Types of Build Results
 
@@ -81,5 +121,19 @@ package_data deps : Array Package
 /-- The package's `extraDepTarget`. -/
 package_data extraDep : ActiveOpaqueTarget
 
-/-- The package's `extern_lib` targets compiled into shared libraries. -/
-package_data externSharedLibs : Array ActiveFileTarget
+-- ## For Target Types
+
+/-- A Lean library's static binary. -/
+target_data leanLib.static : ActiveFileTarget
+
+/-- A Lean library's shared binary. -/
+target_data leanLib.shared : ActiveFileTarget
+
+/-- A Lean binary executable. -/
+target_data leanExe : ActiveFileTarget
+
+/-- A external library's static binary. -/
+target_data externLib.static : ActiveFileTarget
+
+/-- A external library's shared binary. -/
+target_data externLib.shared : ActiveFileTarget
diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean
index 9d50ca92ed..19b768290f 100644
--- a/Lake/Build/Key.lean
+++ b/Lake/Build/Key.lean
@@ -62,6 +62,9 @@ namespace BuildKey
 @[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
   simp [BuildKey.isPackageKey]
 
+@[simp] theorem not_isPackageKey_target : ¬BuildKey.isPackageKey ⟨o, some t, f⟩ := by
+  simp [BuildKey.isPackageKey]
+
 @[inline] def isTargetKey (self : BuildKey) : Bool :=
   self.hasPackage ∧ self.hasTarget
 
diff --git a/Lake/Build/LeanExe.lean b/Lake/Build/LeanExe.lean
deleted file mode 100644
index 551f92a866..0000000000
--- a/Lake/Build/LeanExe.lean
+++ /dev/null
@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-import Lake.Build.LeanLib
-
-namespace Lake
-
--- # Build Package Executable
-
-def LeanExe.target (self : LeanExe) : FileTarget :=
-  BuildTarget.mk' self.file do
-    let cTargetMap ← buildModuleFacetMap #[self.root] &`lean.c
-    let pkgLinkTargets ← self.pkg.linkTargetsOf cTargetMap
-    let linkTargets :=
-      if self.pkg.isLocalModule self.root.name then
-        pkgLinkTargets
-      else
-        let rootTarget := cTargetMap.find? self.root.name |>.get!
-        let rootLinkTarget := self.root.mkOTarget <| Target.active rootTarget
-        #[rootLinkTarget] ++ pkgLinkTargets
-    let target := leanExeTarget self.file linkTargets self.linkArgs
-    target.materializeAsync
-
-protected def Package.exeTarget (self : Package) : FileTarget :=
-  self.builtinExe.target
diff --git a/Lake/Build/LeanLib.lean b/Lake/Build/LeanLib.lean
deleted file mode 100644
index cc3096e8a2..0000000000
--- a/Lake/Build/LeanLib.lean
+++ /dev/null
@@ -1,75 +0,0 @@
-/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-import Lake.Build.Module
-
-open Std System
-open Lean hiding SearchPath
-
-namespace Lake
-
--- # Build Lean Lib
-
-/--
-Build the `extraDepTarget` of a package and its (transitive) dependencies
-and then build the target `facet` of library's modules recursively, constructing
-a single opaque target for the whole build.
--/
-def LeanLib.buildModules (self : LeanLib) (facet : WfName)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
-  let buildMods : BuildM _ := do
-    let mods ← self.getModuleArray
-    let modTargets ← buildModuleFacetArray mods facet
-    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
-  buildMods.catchFailure fun _ => pure <| failure
-
-def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
-  Target.opaque <| self.buildModules &`lean
-
-def Package.libTarget (self : Package) : OpaqueTarget :=
-  self.builtinLib.leanTarget
-
--- # Build Static Lib
-
-def LeanLib.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : LeanLib) : Array (BuildTarget α) :=
-  map.fold (fun a n v => if self.isLocalModule n then a.push (Target.active v) else a) #[]
-
-protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
-  BuildTarget.mk' self.staticLibFile do
-    let mods ← self.getModuleArray
-    let oFileTargets := self.localTargetsOf <| ← buildModuleFacetMap mods &`lean.o
-    staticLibTarget self.staticLibFile oFileTargets |>.materializeAsync
-
-protected def Package.staticLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.staticLibTarget
-
--- # Build Shared Lib
-
-def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
-  map.fold (fun a n v => if self.isLocalModule n then a.push (Target.active v) else a) #[]
-
-def Package.linkTargetsOf
-(targetMap : NameMap ActiveFileTarget) (self : Package) : LakeM (Array FileTarget) := do
-  let collect dep recurse := do
-    let pkg := (← findPackage? dep.name).get!
-    pkg.dependencies.forM fun dep => discard <| recurse dep
-    return pkg.localTargetsOf targetMap ++ pkg.externLibTargets
-  let ⟨x, map⟩ ← EStateT.run (mkRBMap _ _ Name.quickCmp) <|
-    self.dependencies.forM fun dep => discard <| buildTop Dependency.name collect dep
-  match x with
-  | Except.ok _ =>
-    let ts := map.fold (fun acc _ vs => acc ++ vs) #[]
-    return self.localTargetsOf targetMap ++ self.externLibTargets ++ ts
-  | Except.error _ => panic! "dependency cycle emerged after resolution"
-
-protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
-  BuildTarget.mk' self.sharedLibFile do
-    let mods ← self.getModuleArray
-    let linkTargets ← self.pkg.linkTargetsOf <| ← buildModuleFacetMap mods &`lean.o
-    let target := leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs
-    target.materializeAsync
-
-protected def Package.sharedLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.sharedLibTarget
diff --git a/Lake/Build/LeanTarget.lean b/Lake/Build/LeanTarget.lean
new file mode 100644
index 0000000000..40dcffd5f3
--- /dev/null
+++ b/Lake/Build/LeanTarget.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Module
+
+open Std System
+open Lean hiding SearchPath
+
+namespace Lake
+
+-- # Build Lean Lib
+
+/--
+Build the `extraDepTarget` of a package and its (transitive) dependencies
+and then build the target `facet` of library's modules recursively, constructing
+a single opaque target for the whole build.
+-/
+def LeanLib.buildModules (self : LeanLib) (facet : WfName)
+[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
+  let buildMods : BuildM _ := do
+    let mods ← self.getModuleArray
+    let modTargets ← buildModuleFacetArray mods facet
+    (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
+  buildMods.catchFailure fun _ => pure <| failure
+
+def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
+  Target.opaque <| self.buildModules &`lean
+
+def Package.libTarget (self : Package) : OpaqueTarget :=
+  self.builtinLib.leanTarget
+
+-- # Build Static Lib
+
+def LeanLib.buildStatic (self : LeanLib) : BuildM ActiveFileTarget := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
+    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
+    cast of_data <| buildIndexTop <| BuildInfo.staticLeanLib self
+
+protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
+  BuildTarget.mk' self.staticLibFile do self.buildStatic <&> (·.task)
+
+protected def Package.staticLibTarget (self : Package) : FileTarget :=
+  self.builtinLib.staticLibTarget
+
+-- # Build Shared Lib
+
+def LeanLib.buildShared (self : LeanLib) : BuildM ActiveFileTarget := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
+    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
+    cast of_data <| buildIndexTop <| BuildInfo.sharedLeanLib self
+
+protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
+  BuildTarget.mk' self.sharedLibFile do self.buildShared <&> (·.task)
+
+protected def Package.sharedLibTarget (self : Package) : FileTarget :=
+  self.builtinLib.sharedLibTarget
+
+-- # Build Executable
+
+def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget := do
+  failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
+    have of_data := by unfold BuildData, BuildInfo.key; simp; rfl
+    cast of_data <| buildIndexTop <| BuildInfo.leanExe self
+
+def LeanExe.target (self : LeanExe) : FileTarget :=
+  BuildTarget.mk' self.file do self.build <&> (·.task)
+
+protected def Package.exeTarget (self : Package) : FileTarget :=
+  self.builtinExe.target
diff --git a/Lake/Build/LeanTarget1.lean b/Lake/Build/LeanTarget1.lean
new file mode 100644
index 0000000000..e043329364
--- /dev/null
+++ b/Lake/Build/LeanTarget1.lean
@@ -0,0 +1,82 @@
+/-
+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.Info
+import Lake.Build.Store
+import Lake.Build.Targets
+
+namespace Lake
+
+variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
+
+-- # Build Static Lib
+
+/-- Build a library and its imports and collect its local modules' o files. -/
+@[specialize] def LeanLib.recBuildOFiles
+(self : LeanLib) (mods : Array Module) : IndexT m (Array ActiveFileTarget) := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let mut targets := #[]
+  let mut modSet := ModuleSet.empty
+  for mod in mods do
+    let (_, mods) ← mod.recBuildFacet &`lean.imports
+    let mods := mods.push mod
+    for mod in mods do
+      unless modSet.contains mod do
+        if self.isLocalModule mod.name then
+          targets := targets.push <| ← mod.recBuildFacet &`lean.o
+        modSet := modSet.insert mod
+  return targets
+
+protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let oTargets := (← self.recBuildOFiles (← self.getModuleArray)).map Target.active
+  staticLibTarget self.staticLibFile oTargets |>.activate
+
+-- # Build Shared Lib
+
+/-- Build and collect the o files and external libraries of a library and its imports. -/
+@[specialize] def LeanLib.recBuildLinks
+(self : LeanLib) (mods : Array Module) : IndexT m (Array ActiveFileTarget) := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  -- Build and collect modules
+  let mut pkgs := #[]
+  let mut pkgSet := PackageSet.empty
+  let mut modSet := ModuleSet.empty
+  let mut targets := #[]
+  for mod in mods do
+    let (_, mods) ← mod.recBuildFacet &`lean.imports
+    let mods := mods.push mod
+    for mod in mods do
+      unless modSet.contains mod do
+        unless pkgSet.contains mod.pkg do
+            pkgSet := pkgSet.insert mod.pkg
+            pkgs := pkgs.push mod.pkg
+        if self.isLocalModule mod.name then
+          targets := targets.push <| ← mod.recBuildFacet &`lean.o
+        modSet := modSet.insert mod
+  -- Build and collect external library targets
+  for pkg in pkgs do
+    let externLibTargets ← pkg.externLibs.mapM (·.recBuildShared)
+    for target in externLibTargets do
+      targets := targets.push target
+  return targets
+
+protected def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let linkTargets := (← self.recBuildLinks (← self.getModuleArray)).map Target.active
+  leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate
+
+-- # Build Executable
+
+def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do
+  have : MonadLift BuildM m := ⟨liftM⟩
+  let linkTargets := #[Target.active <| ← self.root.recBuildFacet &`lean.o]
+  let (_, imports) ← self.root.recBuildFacet &`lean.imports
+  let mut linkTargets ← imports.foldlM (init := linkTargets) fun a m => do
+    return a.push <| Target.active <| ← m.recBuildFacet &`lean.o
+  let deps := (← self.pkg.recBuildFacet &`deps).push self.pkg
+  for dep in deps do for lib in dep.externLibs do
+    linkTargets := linkTargets.push <| Target.active <| ← lib.recBuildStatic
+  leanExeTarget self.file linkTargets self.linkArgs |>.activate
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index b4a425346c..58952f6f52 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -21,7 +20,9 @@ of the top-level build.
 -/
 @[inline] def buildModuleTop (mod : Module) (facet : WfName)
 [h : DynamicType ModuleData facet α] : CycleT BuildKey m α  :=
-  have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
+  have of_data := by
+    unfold BuildData, BuildInfo.key, Module.mkBuildKey
+    simp [h.eq_dynamic_type]
   cast of_data <| buildIndexTop (m := m) <| BuildInfo.module mod facet
 
 /--
diff --git a/Lake/Build/Module1.lean b/Lake/Build/Module1.lean
index 0a860306ef..44285854c0 100644
--- a/Lake/Build/Module1.lean
+++ b/Lake/Build/Module1.lean
@@ -78,7 +78,7 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
   let mut pkgTargets := #[]
   for pkg in pkgs do
     libDirs := libDirs.push pkg.libDir
-    let externLibTargets ← pkg.recBuildFacet &`externSharedLibs
+    let externLibTargets ← pkg.externLibs.mapM (·.recBuildShared)
     for target in externLibTargets do
       if let some parent := target.info.parent then
         libDirs := libDirs.push parent
diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean
index c1473604da..b7bedc2045 100644
--- a/Lake/Build/Store.lean
+++ b/Lake/Build/Store.lean
@@ -70,3 +70,13 @@ def collectPackageFacetArray (self : BuildStore)
       let of_data := by simp [isPackageKey_data h.1, h.2, eq_dynamic_type]
       res := res.push <| cast of_data v
   return res
+
+/-- Derive an array of built external shared libraries from the store. -/
+def collectSharedExternLibs (self : BuildStore)
+[DynamicType TargetData &`externLib.shared α] : Array α := Id.run do
+  let mut res : Array α := #[]
+  for ⟨k, v⟩ in self do
+    if h : k.isTargetKey ∧ k.facet = &`externLib.shared then
+      let of_data := by simp [isTargetKey_data h.1, h.2, eq_dynamic_type]
+      res := res.push <| cast of_data v
+  return res
diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean
index 5378b3feaa..2203cf3654 100644
--- a/Lake/Config/ExternLib.lean
+++ b/Lake/Config/ExternLib.lean
@@ -25,6 +25,10 @@ structure ExternLib where
 
 namespace ExternLib
 
+/- The library's well-formed name. -/
+@[inline] def name (self : ExternLib) : WfName :=
+  WfName.ofName self.config.name
+
 /-- The external library's user-defined `target`. -/
 @[inline] def target (self : ExternLib) : FileTarget :=
   self.config.target
diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean
index 23dc88cffd..8e0fa98ffd 100644
--- a/Lake/Config/LeanExe.lean
+++ b/Lake/Config/LeanExe.lean
@@ -40,6 +40,10 @@ def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig) : LeanLibConfig where
 
 namespace LeanExe
 
+/- The executable's well-formed name. -/
+@[inline] def name (self : LeanExe) : WfName :=
+  WfName.ofName self.config.name
+
 /-- Converts the executable into a library with a single module (the root). -/
 @[inline] def toLeanLib (self : LeanExe) : LeanLib :=
   ⟨self.pkg, self.config.toLeanLibConfig⟩
diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean
index 97db0f29a5..8085a6445f 100644
--- a/Lake/Config/LeanLib.lean
+++ b/Lake/Config/LeanLib.lean
@@ -30,8 +30,12 @@ structure LeanLib where
 
 namespace LeanLib
 
+/- The library's well-formed name. -/
+@[inline] def name (self : LeanLib) : WfName :=
+  WfName.ofName self.config.name
+
 /- The package's `srcDir` joined with the library's `srcDir`. -/
-def srcDir (self : LeanLib) : FilePath :=
+@[inline] def srcDir (self : LeanLib) : FilePath :=
   self.pkg.srcDir / self.config.srcDir
 
 /-- Whether the given module is considered local to the library. -/
@@ -43,33 +47,33 @@ def srcDir (self : LeanLib) : FilePath :=
   self.config.isBuildableModule mod
 
 /-- The file name of the library's static binary (i.e., `lib{libName}.a`) -/
-def staticLibFileName (self : LeanLib) : FilePath :=
+@[inline] def staticLibFileName (self : LeanLib) : FilePath :=
   s!"lib{self.config.libName}.a"
 
 /-- The path to the static library in the package's `libDir`. -/
-def staticLibFile (self : LeanLib) : FilePath :=
+@[inline] def staticLibFile (self : LeanLib) : FilePath :=
   self.pkg.libDir / self.staticLibFileName
 
 /-- The file name of the library's shared binary (i.e., its `dll`/`dylib`/`so`) . -/
-def sharedLibFileName (self : LeanLib) : FilePath :=
+@[inline] def sharedLibFileName (self : LeanLib) : FilePath :=
   s!"{self.config.libName}.{sharedLibExt}"
 
 /-- The path to the shared library in the package's `libDir`. -/
-def sharedLibFile (self : LeanLib) : FilePath :=
+@[inline] def sharedLibFile (self : LeanLib) : FilePath :=
   self.pkg.libDir / self.sharedLibFileName
 
 /--
 Whether to precompile the library's modules.
 Is true if either the package or the library have `precompileModules` set.
 -/
-def precompileModules (self : LeanLib) : Bool :=
+@[inline] def precompileModules (self : LeanLib) : Bool :=
   self.pkg.precompileModules || self.config.precompileModules
 
 /--
 The arguments to pass to `lean` when compiling the library's Lean files.
 That is, the package's `moreLeanArgs` plus the library's  `moreLeanArgs`.
 -/
-def leanArgs (self : LeanLib) : Array String :=
+@[inline] def leanArgs (self : LeanLib) : Array String :=
   self.pkg.moreLeanArgs ++ self.config.moreLeanArgs
 
 /--
@@ -77,12 +81,12 @@ The arguments to pass to `leanc` when compiling the library's C files.
 That is, `-O3`, `-DNDEBUG`, the package's `moreLeancArgs`, and then the
 library's `moreLeancArgs`.
 -/
-def leancArgs (self : LeanLib) : Array String :=
+@[inline] def leancArgs (self : LeanLib) : Array String :=
   #["-O3", "-DNDEBUG"] ++ self.pkg.moreLeancArgs ++ self.config.moreLeancArgs
 
 /--
 The arguments to pass to `leanc` when linking the shared library.
 That is, the package's `moreLinkArgs` plus the library's  `moreLinkArgs`.
 -/
-def linkArgs (self : LeanLib) : Array String :=
+@[inline] def linkArgs (self : LeanLib) : Array String :=
   self.pkg.moreLinkArgs ++ self.config.moreLinkArgs