diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean
index 77f4d4276c..0a53f4b43b 100644
--- a/src/lake/Lake/Build/Data.lean
+++ b/src/lake/Lake/Build/Data.lean
@@ -15,59 +15,134 @@ namespace Lake
 --------------------------------------------------------------------------------
 
 /--
-The open type family which maps a module facet's name to its build data
-in the Lake build store. For example, a transitive × direct import pair
-for the `lean.imports` facet or an active build target for `lean.c`.
+The open type family which maps a Lake data kind to its associated type.
+For example, `LeanLib.facetKind` maps to `LeanLib`.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `data_type`).
+-/
+opaque DataType (kind : Name) : Type u
+
+/-- A `Name` descriptor of a data type. -/
+class DataKind (α : Type u) where
+  /-- The name which describes `α`. -/
+  name : Name
+  /-- Proof that `α` is the data type described by `name`. -/
+  wf : α = DataType name
+
+/--
+Tries to synthesize a `Name` descriptor of a data type.
+Otherwise uses `Name.anonymous` to indicate none was found.
+-/
+class OptDataKind (α : Type u) where
+  /-- The name which describes `α` (or `Name.anonymous` if none). -/
+  name : Name
+  /-- Proof that `α` is the data type described by `name` (if valid). -/
+  wf (h : ¬ name.isAnonymous) : α = DataType name
+
+@[instance low]
+def OptDataKind.anonymous : OptDataKind α where
+  name := .anonymous
+  wf h := by simp [Name.isAnonymous] at h
+
+@[inline] def OptDataKind.isAnonymous (self : OptDataKind α) : Bool :=
+  self.name.isAnonymous
+
+theorem OptDataKind.eq_data_type
+  {self : OptDataKind α} (h : ¬ self.isAnonymous) : α = DataType self.name
+:= self.wf h
+
+instance [DataKind α] : OptDataKind α where
+  name := DataKind.name α
+  wf _ := DataKind.wf
+
+instance : CoeOut (OptDataKind α) Lean.Name := ⟨(·.name)⟩
+instance : ToString (OptDataKind α) := ⟨(·.name.toString)⟩
+
+@[deprecated DataType (since := "2025-03-26")] abbrev TargetData := DataType
+
+/--
+The open type family which maps a Lake facet to its output type.
+For example, a `FilePath` for the `module.olean` facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `facet_data`).
+-/
+opaque FacetOut (facet : Name) : Type
+
+/--
+The open type family which maps a Lake facet kind and name to its output type.
+For example, a `FilePath` for the `module` `olean` facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `facet_data`).
+-/
+abbrev FacetData (kind facet : Name) := FacetOut (kind ++ facet)
+
+instance [h : FamilyDef FacetOut (kind ++ facet) α] : FamilyDef (FacetData kind) facet α :=
+  ⟨h.fam_eq⟩
+
+instance [h :  FamilyDef (FacetData kind) facet α] : FamilyDef FacetOut (kind ++ facet) α :=
+  ⟨h.fam_eq⟩
+
+/--
+The open type family which maps a module facet's name to its output type.
+For example, a `FilePath` for the module `olean` facet.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `module_data`).
 -/
-opaque ModuleData (facet : Name) : Type
+abbrev ModuleData := FacetData Module.facetKind
 
 /--
-The open type family which maps a package facet's name to its build data
-in the Lake build store. For example, a transitive dependencies of the package
-for the facet `deps`.
+The open type family which maps a package facet's name to output type.
+For example, an `Arrry Package` of direct dependencies for the `deps` facet.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `package_data`).
 -/
-opaque PackageData (facet : Name) : Type
+abbrev PackageData := FacetData Package.facetKind
+
+/-- The kind identifier for facets of a Lean library. -/
+@[match_pattern] abbrev LeanLib.facetKind : Name := `lean_lib
 
 /--
-The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
-facet to its associated build data. For example, an active build target for
-the `externLib.static` facet.
-
-It is an open type, meaning additional mappings can be add lazily
-as needed (via `target_data`).
--/
-opaque TargetData (facet : Name) : Type
-
-/-
-The open type family which maps a library facet's name to its build data
-in the Lake build store. For example, an active build target for the `static`
-facet.
+The open type family which maps a Lean library facet's name to its output type.
+For example, the `FilePath` pf the generated static library for the `static` facet.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `library_data`).
 -/
-abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
+abbrev LibraryData := FacetData LeanLib.facetKind
 
-instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α :=
-  ⟨by simp [h.family_key_eq_type]⟩
+@[inherit_doc LibraryData]
+abbrev LeanLibData := LibraryData
 
-instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
-  ⟨h.family_key_eq_type⟩
+/-- The kind identifier for facets of a Lean executable. -/
+@[match_pattern] abbrev LeanExe.facetKind : Name := `lean_exe
+
+/-- The kind identifier for facets of an external library. -/
+@[match_pattern] abbrev ExternLib.facetKind : Name := `extern_lib
 
 /--
-The open type family which maps a custom target (package × target name) to
-its build data in the Lake build store.
+The open type family which maps a custom package target
+(package × target name) to its output type.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `custom_data`).
 -/
-opaque CustomData (target : Name × Name) : Type
+opaque CustomOut (target : Name × Name) : Type
+
+/--
+The open type family which maps a custom package targetto its output type.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `custom_data`).
+-/
+abbrev CustomData (package target : Name) := CustomOut (package, target)
+
+instance [h : FamilyDef CustomOut (p, t) α] : FamilyDef (CustomData p) t α :=
+  ⟨h.fam_eq⟩
 
 --------------------------------------------------------------------------------
 /-! ## Build Data                                                             -/
@@ -79,55 +154,119 @@ It is a simple type function composed of the separate open type families for
 modules facets, package facets, Lake target facets, and custom targets.
 -/
 abbrev BuildData : BuildKey → Type
-| .moduleFacet _ f => ModuleData f
-| .packageFacet _ f => PackageData f
-| .targetFacet _ _ f => TargetData f
-| .customTarget p t => CustomData (p, t)
+| .module _ => DataType Module.facetKind
+| .package _ => DataType Package.facetKind
+| .packageTarget p t => CustomData p t
+| .facet _ f => FacetOut f
 
-instance (priority := low) : FamilyDef BuildData k (BuildData k) := ⟨rfl⟩
-instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
-instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
-instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
-instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.packageTarget p t) (CustomData p t) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.facet t f) (FacetOut f) := ⟨rfl⟩
+
+instance [FamilyOut (CustomData p) t α]
+: FamilyDef BuildData (.packageTarget p t) α where
+  fam_eq := by unfold BuildData; simp
+
+instance [FamilyOut DataType Module.facetKind α]
+: FamilyDef BuildData (.module k) α where
+  fam_eq := by unfold BuildData; simp
+
+instance [FamilyOut DataType Package.facetKind α]
+: FamilyDef BuildData (.package k) α where
+  fam_eq := by unfold BuildData; simp
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/
 --------------------------------------------------------------------------------
 
+open Parser Command
+
+/-- Macro for declaring new `DatayType`. -/
+scoped macro (name := dataTypeDecl)
+  doc?:optional(docComment) "data_type " kind:ident " : " ty:term
+: command => do
+  let fam := mkCIdentFrom (← getRef) ``DataType
+  let kindName := Name.quoteFrom kind kind.getId
+  let id := mkIdentFrom kind (canonical := true) <|
+    kind.getId.modifyBase (kind.getId ++ ·)
+  `($[$doc?]? family_def $id : $fam $kindName := $ty
+    instance : DataKind $ty := ⟨$kindName, by simp⟩)
+
+/-- Internal macro for declaring new facet within Lake. -/
+scoped macro (name := builtinFacetCommand)
+  doc?:optional(docComment) tk:"builtin_facet "
+  id?:optional(atomic(group(ident " @ "))) name:ident " : " ns:ident " => " ty:term
+: command => withRef tk do
+  let fam := mkCIdentFrom tk ``FacetOut
+  let kindName ← match ns.getId with
+    | `Package => pure Package.facetKind
+    | `Module => pure Module.facetKind
+    | `LeanLib => pure LeanLib.facetKind
+    | `LeanExe => pure LeanExe.facetKind
+    | `ExternLib => pure ExternLib.facetKind
+    | _ => Macro.throwErrorAt ns "unknown facet kind"
+  let nameLit := Name.quoteFrom name name.getId (canonical := id?.isSome)
+  let kindLit := Name.quoteFrom ns kindName (canonical := true)
+  let facet := kindName ++ name.getId
+  let facetId := mkIdentFrom tk facet (canonical := true)
+  let facetLit := Name.quoteFrom tk facet
+  let id ←
+    if let some id := id? then
+      let id := id.raw[0]
+      pure <| mkIdentFrom id (ns.getId ++ id.getId) (canonical := true)
+    else
+      match name.getId with
+      | .str .anonymous n => pure <| mkIdentFrom name (ns.getId.str s!"{n}Facet") (canonical := true)
+      | _ =>  Macro.throwErrorAt name "cannot generate facet declaration name from facet name"
+  `(
+    $[$doc?]? abbrev $id := $facetLit
+    family_def $facetId : $fam $facetLit := $ty
+    instance : FamilyDef FacetOut ($kindLit ++ $nameLit) $ty :=
+      inferInstanceAs (FamilyDef FacetOut $facetLit $ty)
+  )
+
+/-- Macro for declaring new `FacetData`. -/
+scoped macro (name := facetDataDecl)
+  doc?:optional(docComment) tk:"facet_data " kind:ident name:ident " : " ty:term
+: command => withRef tk do
+  let fam := mkCIdentFrom tk ``FacetOut
+  let kindLit := Name.quoteFrom kind kind.getId
+  let nameLit := Name.quoteFrom name name.getId
+  let facet := kind.getId ++ name.getId
+  let facetLit := Name.quoteFrom tk facet
+  let id := mkIdentFrom tk facet (canonical := true)
+  `($[$doc?]? family_def $id : $fam $facetLit := $ty
+    instance : FamilyDef FacetOut ($kindLit ++ $nameLit) $ty :=
+      inferInstanceAs (FamilyDef FacetOut $facetLit $ty))
+
 /-- 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 := Name.quoteFrom id id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+scoped macro (name := packageDataDecl)
+  doc?:optional(docComment) tk:"package_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk Package.facetKind) $facet : $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 := Name.quoteFrom id id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+scoped macro (name := moduleDataDecl)
+  doc?:optional(docComment) tk:"module_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk Module.facetKind) $facet : $ty)
 
-/-- Macro for declaring new `TargetData` for libraries. -/
-scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment)
-"library_data " id:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``TargetData
-  let key := Name.quoteFrom id id.getId
-  let id := mkIdentFrom id (canonical := true) <| id.getId.modifyBase (`leanLib ++ ·)
-  `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
+/-- Macro for declaring new `LibraryData`. -/
+scoped macro (name := libraryDataDecl)
+  doc?:optional(docComment) tk:"library_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk LeanLib.facetKind) $facet : $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 := Name.quoteFrom id id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+scoped macro (name := targetDataDecl)
+  doc?:optional(docComment) tk:"target_data " id:ident " : " ty:term
+: command => withRef tk do
+  let fam := mkCIdentFrom (← getRef) ``TargetData
+  let idx := Name.quoteFrom id id.getId
+  `($[$doc?]? family_def $id : $fam $idx := $ty)
 
 /-- Macro for declaring new `CustomData`. -/
-scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
-"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``CustomData
+scoped macro (name := customDataDecl)
+  doc?:optional(docComment) tk:"custom_data " pkg:ident tgt:ident " : " ty:term
+: command => withRef tk do
+  let fam := mkCIdentFrom (← getRef) ``CustomOut
   let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
   let pkg := Name.quoteFrom pkg pkg.getId
   let tgt := Name.quoteFrom pkg tgt.getId
-  `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)
+  `($[$doc?]? family_def $id : $fam ($pkg, $tgt) := $ty)
diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean
index 9a278ff343..1a773e6c6c 100644
--- a/src/lake/Lake/Build/Executable.lean
+++ b/src/lake/Lake/Build/Executable.lean
@@ -22,12 +22,32 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
   -/
   let mut linkJobs := #[]
   for facet in self.root.nativeFacets self.supportInterpreter do
-    linkJobs := linkJobs.push <| ← fetch <| self.root.facet facet.name
+    linkJobs := linkJobs.push <| ← facet.fetch self.root
   let imports ← (← self.root.transImports.fetch).await
   for mod in imports do
     for facet in mod.nativeFacets self.supportInterpreter do
-      linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
+      linkJobs := linkJobs.push <| ← facet.fetch mod
   let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch
   buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean
+
+/-- The facet configuration for the builtin `LeanExe.exeFacet`. -/
+def LeanExe.exeFacetConfig : LeanExeFacetConfig exeFacet :=
+  mkFacetJobConfig recBuildExe
+
+def LeanExe.recBuildDefault (lib : LeanExe) : FetchM (Job FilePath) :=
+  lib.exe.fetch
+
+/-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
+def LeanExe.defaultFacetConfig : LeanExeFacetConfig defaultFacet :=
+  mkFacetJobConfig recBuildDefault
+
+/--
+A name-configuration map for the initial set of
+Lean executable facets (e.g., `exe`).
+-/
+def LeanExe.initFacetConfigs : DNameMap LeanExeFacetConfig :=
+  DNameMap.empty
+  |>.insert defaultFacet defaultFacetConfig
+  |>.insert exeFacet exeFacetConfig
diff --git a/src/lake/Lake/Build/ExternLib.lean b/src/lake/Lake/Build/ExternLib.lean
new file mode 100644
index 0000000000..77b48d820d
--- /dev/null
+++ b/src/lake/Lake/Build/ExternLib.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Build.Common
+
+/-! # External Library Build
+Build function definitions for external libraries.
+-/
+
+open System (FilePath)
+
+namespace Lake
+
+def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
+  withRegisterJob s!"{lib.staticTargetName.toString}:static" do
+  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
+
+/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
+def ExternLib.staticFacetConfig : ExternLibFacetConfig staticFacet :=
+  mkFacetJobConfig recBuildStatic
+
+def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
+  withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
+  buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
+
+/-- The facet configuration for the builtin `ExternLib.sharedFacet`. -/
+def ExternLib.sharedFacetConfig : ExternLibFacetConfig sharedFacet :=
+  mkFacetJobConfig recBuildShared
+
+def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
+  withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
+  computeDynlibOfShared (← lib.shared.fetch)
+
+/-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
+def ExternLib.dynlibFacetConfig : ExternLibFacetConfig dynlibFacet :=
+  mkFacetJobConfig recComputeDynlib
+
+def ExternLib.recBuildDefault (lib : ExternLib) : FetchM (Job FilePath) :=
+  lib.static.fetch
+
+/-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
+def ExternLib.defaultFacetConfig : ExternLibFacetConfig defaultFacet :=
+  mkFacetJobConfig recBuildDefault
+
+/--
+A name-configuration map for the initial set of
+external library facets (e.g., `static`, `shared`).
+-/
+def ExternLib.initFacetConfigs : DNameMap ExternLibFacetConfig :=
+  DNameMap.empty
+  |>.insert defaultFacet defaultFacetConfig
+  |>.insert staticFacet staticFacetConfig
+  |>.insert sharedFacet sharedFacetConfig
+  |>.insert dynlibFacet dynlibFacetConfig
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index b084c5ff5e..2c9f2f76c2 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -34,22 +34,21 @@ structure ModuleFacet (α) where
   /-- The name of the module facet. -/
   name : Name
   /-- Proof that module's facet build result is of type α. -/
-  data_eq : ModuleData name = α
+  data_eq : FacetOut name = α
   deriving Repr
 
-instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
+instance (facet : ModuleFacet α) : FamilyDef FacetOut facet.name α :=
   ⟨facet.data_eq⟩
 
-instance [FamilyOut ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
-  ⟨facet, FamilyOut.family_key_eq_type⟩
+instance [FamilyOut FacetOut facet α] : CoeDep Name facet (ModuleFacet α) :=
+  ⟨facet, FamilyOut.fam_eq⟩
 
 /--
 The facet which builds all of a module's dependencies
 (i.e., transitive local imports and `--load-dynlib` shared libraries).
 Returns the list of shared libraries to load along with their search path.
 -/
-abbrev Module.depsFacet := `deps
-module_data deps : ModuleDeps
+builtin_facet deps : Module => ModuleDeps
 
 /--
 The core build facet of a Lean file.
@@ -57,59 +56,47 @@ Elaborates the Lean file via `lean` and produces all the Lean artifacts
 of the module (i.e., `olean`, `ilean`, `c`).
 Its trace just includes its dependencies.
 -/
-abbrev Module.leanArtsFacet := `leanArts
-module_data leanArts : Unit
+builtin_facet leanArts : Module => Unit
 
 /-- The `olean` file produced by `lean`. -/
-abbrev Module.oleanFacet := `olean
-module_data olean : FilePath
+builtin_facet olean : Module => FilePath
 
 /-- The `ilean` file produced by `lean`. -/
-abbrev Module.ileanFacet := `ilean
-module_data ilean : FilePath
+builtin_facet ilean : Module => FilePath
 
 /-- The C file built from the Lean file via `lean`. -/
-abbrev Module.cFacet := `c
-module_data c : FilePath
+builtin_facet c : Module => FilePath
 
 /-- The LLVM BC file built from the Lean file via `lean`. -/
-abbrev Module.bcFacet := `bc
-module_data bc : FilePath
+builtin_facet bc : Module => FilePath
 
 /--
 The object file `.c.o` built from `c`.
 On Windows, this is `c.o.noexport`, on other systems it is `c.o.export`).
 -/
-abbrev Module.coFacet := `c.o
-module_data c.o : FilePath
+builtin_facet coFacet @ c.o : Module => FilePath
 
 /-- The object file `.c.o.export` built from `c` (with `-DLEAN_EXPORTING`). -/
-abbrev Module.coExportFacet := `c.o.export
-module_data c.o.export : FilePath
+builtin_facet coExportFacet @ c.o.export : Module => FilePath
 
 /-- The object file `.c.o.noexport` built from `c` (without `-DLEAN_EXPORTING`). -/
-abbrev Module.coNoExportFacet := `c.o.noexport
-module_data c.o.noexport : FilePath
+builtin_facet coNoExportFacet @ c.o.noexport : Module => FilePath
 
 /-- The object file `.bc.o` built from `bc`. -/
-abbrev Module.bcoFacet := `bc.o
-module_data bc.o : FilePath
+builtin_facet bcoFacet @ bc.o : Module => FilePath
 
 /--
 The object file built from `c`/`bc`.
 On Windows with the C backend, no Lean symbols are exported.
 On every other configuration, symbols are exported.
 -/
-abbrev Module.oFacet := `o
-module_data o : FilePath
+builtin_facet o : Module => FilePath
 
 /-- The object file built from `c`/`bc` (with Lean symbols exported). -/
-abbrev Module.oExportFacet := `o.export
-module_data o.export : FilePath
+builtin_facet oExportFacet @ o.export : Module => FilePath
 
 /-- The object file built from `c`/`bc` (without Lean symbols exported). -/
-abbrev Module.oNoExportFacet := `o.noexport
-module_data o.noexport : FilePath
+builtin_facet oNoExportFacet @ o.noexport : Module => FilePath
 
 
 /-! ## Package Facets -/
@@ -118,36 +105,31 @@ module_data o.noexport : FilePath
 A package's *optional* cached build archive (e.g., from Reservoir or GitHub).
 Will NOT cause the whole build to fail if the archive cannot be fetched.
 -/
-abbrev Package.optBuildCacheFacet := `optCache
-package_data optCache : Bool
+builtin_facet optBuildCacheFacet @ optCache : Package => Bool
 
 /--
 A package's cached build archive (e.g., from Reservoir or GitHub).
 Will cause the whole build to fail if the archive cannot be fetched.
 -/
-abbrev Package.buildCacheFacet := `cache
-package_data cache : Unit
+builtin_facet buildCacheFacet @ cache : Package => Unit
 
 /--
 A package's *optional* build archive from Reservoir.
 Will NOT cause the whole build to fail if the barrel cannot be fetched.
 -/
-abbrev Package.optReservoirBarrelFacet := `optBarrel
-package_data optBarrel : Bool
+builtin_facet optReservoirBarrelFacet @ optBarrel : Package => Bool
 
 /--
 A package's Reservoir build archive from Reservoir.
 Will cause the whole build to fail if the barrel cannot be fetched.
 -/
-abbrev Package.reservoirBarrelFacet := `barrel
-package_data barrel : Unit
+builtin_facet reservoirBarrelFacet @ barrel : Package => Unit
 
 /--
 A package's *optional* build archive from a GitHub release.
 Will NOT cause the whole build to fail if the release cannot be fetched.
 -/
-abbrev Package.optGitHubReleaseFacet := `optRelease
-package_data optRelease : Bool
+builtin_facet optGitHubReleaseFacet @ optRelease : Package => Bool
 
 @[deprecated optGitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.optReleaseFacet := optGitHubReleaseFacet
@@ -156,25 +138,24 @@ abbrev Package.optReleaseFacet := optGitHubReleaseFacet
 A package's build archive from a GitHub release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
-abbrev Package.gitHubReleaseFacet := `release
-package_data release : Unit
+builtin_facet gitHubReleaseFacet @ release : Package => Unit
 
 @[deprecated gitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.releaseFacet := gitHubReleaseFacet
 
 /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
-abbrev Package.extraDepFacet := `extraDep
-package_data extraDep : Unit
+builtin_facet extraDep : Package => Unit
 
 /-! ## Target Facets -/
 
+/-- The library's default facets (as specified by its `defaultFacets` configuration). . -/
+builtin_facet default : LeanLib => Unit
+
 /-- A Lean library's Lean artifacts (i.e., `olean`, `ilean`, `c`). -/
-abbrev LeanLib.leanArtsFacet := `leanArts
-library_data leanArts : Unit
+builtin_facet leanArts : LeanLib => Unit
 
 /-- A Lean library's static artifact. -/
-abbrev LeanLib.staticFacet := `static
-library_data static : FilePath
+builtin_facet static : LeanLib => FilePath
 
 /--
 A Lean library's static artifact (with exported symbols).
@@ -184,29 +165,28 @@ Such libraries are usually used as part of the local build process of some
 shared artifact and not publicly distributed. Standard static libraries are
 much better for distribution.
 -/
-abbrev LeanLib.staticExportFacet := `static.export
-library_data static.export : FilePath
+builtin_facet staticExportFacet @ static.export : LeanLib => FilePath
 
 /-- A Lean library's shared artifact. -/
-abbrev LeanLib.sharedFacet := `shared
-library_data shared : FilePath
+builtin_facet shared : LeanLib => FilePath
 
 /-- A Lean library's `extraDepTargets` mixed with its package's. -/
-abbrev LeanLib.extraDepFacet := `extraDep
-library_data extraDep : Unit
+builtin_facet extraDep : LeanLib => Unit
+
+/-- The executable's default facet (i.e., an alias for `exe`) -/
+builtin_facet default : LeanExe => FilePath
 
 /-- A Lean binary executable. -/
-abbrev LeanExe.exeFacet := `leanExe
-target_data leanExe : FilePath
+builtin_facet exe : LeanExe => FilePath
+
+/-- The external library's default facet (i.e., an alias for `static`) -/
+builtin_facet default : ExternLib => FilePath
 
 /-- A external library's static binary. -/
-abbrev ExternLib.staticFacet := `externLib.static
-target_data externLib.static : FilePath
+builtin_facet static : ExternLib => FilePath
 
 /-- A external library's shared binary. -/
-abbrev ExternLib.sharedFacet := `externLib.shared
-target_data externLib.shared : FilePath
+builtin_facet shared : ExternLib => FilePath
 
 /-- A external library's dynlib. -/
-abbrev ExternLib.dynlibFacet := `externLib.dynlib
-target_data externLib.dynlib : Dynlib
+builtin_facet dynlib : ExternLib => Dynlib
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 4d9c3864c0..fd1f89231e 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -80,3 +80,7 @@ abbrev FetchM := FetchT LogIO
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)
+
+/-- Fetch the result of this facet of a module. -/
+protected def ModuleFacet.fetch (self : ModuleFacet α) (mod : Module) : FetchM (Job α) :=
+  fetch <| mod.facetCore self.name
diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean
index e03c0acef4..669d8458ac 100644
--- a/src/lake/Lake/Build/Index.lean
+++ b/src/lake/Lake/Build/Index.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Build.Executable
+import Lake.Config.Monad
 import Lake.Build.Topological
 
 /-!
@@ -16,66 +16,32 @@ Lake build functions, which is used by Lake to build any Lake build info.
 This module leverages the index to perform topologically-based recursive builds.
 -/
 
-open Lean
-namespace Lake
+open Lean (Name)
 open System (FilePath)
 
-/--
-Converts a conveniently-typed target facet build function into its
-dynamically-typed equivalent.
--/
-@[macro_inline] def mkTargetFacetBuild
-  (facet : Name) (build : FetchM (Job α))
-  [h : FamilyOut TargetData facet α]
-: FetchM (Job (TargetData facet)) :=
-  cast (by rw [← h.family_key_eq_type]) build
-
-def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
-  withRegisterJob s!"{lib.staticTargetName.toString}:static" do
-  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
-
-def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
-  withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
-  buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
-
-def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
-  withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
-  computeDynlibOfShared (← lib.shared.fetch)
-
-/-!
-## Topologically-based Recursive Build Using the Index
--/
+namespace Lake
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
-| .moduleFacet mod facet => do
-  if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-    config.fetchFn mod
-  else
-    error s!"do not know how to fetch module facet `{facet}`"
-| .packageFacet pkg facet => do
-  if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-    config.fetchFn pkg
-  else
-    error s!"do not know how to fetch package facet `{facet}`"
-| .target pkg target =>
-  if let some config := pkg.findTargetConfig? target then
-    config.fetchFn pkg
-  else
-    error s!"could not fetch `{target}` of `{pkg.name}` -- target not found"
-| .libraryFacet lib facet => do
-  if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
-    config.fetchFn lib
-  else
-    error s!"do not know how to fetch library facet `{facet}`"
-| .leanExe exe =>
-  mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
-| .staticExternLib lib =>
-  mkTargetFacetBuild ExternLib.staticFacet lib.recBuildStatic
-| .sharedExternLib lib =>
-  mkTargetFacetBuild ExternLib.sharedFacet lib.recBuildShared
-| .dynlibExternLib lib =>
-  mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
+def recBuildWithIndex (info : BuildInfo) : FetchM (Job (BuildData info.key)) :=
+  match info with
+  | .target pkg target => do
+    if let some decl := pkg.findTargetDecl? target then
+      if h : decl.kind.isAnonymous then
+        (decl.targetConfig h).fetchFn pkg
+      else
+        let kind := ⟨decl.kind, by simp [decl.target_eq_type h]⟩
+        let job := Job.pure (kind := kind) <| decl.mkConfigTarget pkg
+        return cast (by simp [decl.data_eq_target h]) job
+    else
+      error s!"invalid target '{info}': target not found in package"
+  | .facet _ kind data facet => do
+    if let some config := (← getWorkspace).findFacetConfig? facet then
+      if h : config.kind = kind then
+        config.fetchFn <| cast (by simp [h]) data
+      else
+        error s!"invalid target '{info}': target is of kind '{kind}', but facet expects '{config.kind}'"
+    else
+      error s!"invalid target '{info}': unknown facet '{facet}'"
 
 /-- Recursive build function with memoization. -/
 def recFetchWithIndex : (info : BuildInfo) → RecBuildM (Job (BuildData info.key)) :=
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index 6c33fb2359..33ac477003 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -21,14 +21,8 @@ open Lean (Name)
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo
-| moduleFacet (module : Module) (facet : Name)
-| packageFacet (package : Package) (facet : Name)
-| libraryFacet (lib : LeanLib) (facet : Name)
-| leanExe (exe : LeanExe)
-| staticExternLib (lib : ExternLib)
-| sharedExternLib (lib : ExternLib)
-| dynlibExternLib (lib : ExternLib)
 | target (package : Package) (target : Name)
+| facet (target : BuildKey) (kind : Name) (data : DataType.{0} kind) (facet : Name)
 
 --------------------------------------------------------------------------------
 /-! ## Build Info & Keys                                                      -/
@@ -36,79 +30,74 @@ inductive BuildInfo
 
 /-! ### Build Key Helper Constructors -/
 
+abbrev Module.buildKey (self : Module) : BuildKey :=
+  .module self.keyName
+
 abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey :=
   .moduleFacet self.keyName facet
 
+abbrev Package.buildKey (self : Package) : BuildKey :=
+  .package self.name
+
 abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
   .packageFacet self.name facet
 
-abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
-  .customTarget self.name target
+abbrev Package.targetBuildKey
+  (target : Name) (self : Package)
+: BuildKey := .packageTarget self.name target
+
+abbrev LeanLib.buildKey (self : LeanLib) : BuildKey :=
+  .packageTarget self.pkg.name self.name
 
 abbrev LeanLib.facetBuildKey (self : LeanLib) (facet : Name) : BuildKey :=
-  .targetFacet self.pkg.name self.name (`leanLib ++ facet)
+  .targetFacet self.pkg.name self.name facet
 
 abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
+  .packageTarget self.pkg.name self.name
+
+abbrev LeanExe.exeBuildKey (self : LeanExe) : BuildKey :=
   .targetFacet self.pkg.name self.name exeFacet
 
+abbrev ExternLib.buildKey (self : ExternLib) : BuildKey :=
+  .packageTarget self.pkg.name self.name
+
+abbrev ExternLib.facetBuildKey (facet : Name) (self : ExternLib) : BuildKey :=
+  .targetFacet self.pkg.name self.name facet
+
 abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name staticFacet
+  self.facetBuildKey staticFacet
 
 abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name sharedFacet
+  self.facetBuildKey sharedFacet
 
 abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name dynlibFacet
+  self.facetBuildKey dynlibFacet
 
 /-! ### Build Info to Key -/
 
 /-- The key that identifies the build in the Lake build store. -/
 @[reducible] def BuildInfo.key : (self : BuildInfo) → BuildKey
-| moduleFacet m f => m.facetBuildKey f
-| packageFacet p f => p.facetBuildKey f
-| libraryFacet l f => l.facetBuildKey f
-| leanExe x => x.buildKey
-| staticExternLib l => l.staticBuildKey
-| sharedExternLib l => l.sharedBuildKey
-| dynlibExternLib l => l.dynlibBuildKey
 | target p t => p.targetBuildKey t
+| facet (target := t) (facet := f) .. => .facet t f
+
+instance : ToString BuildInfo := ⟨(toString ·.key)⟩
 
 /-! ### Instances for deducing data types of `BuildInfo` keys -/
 
-instance [FamilyOut ModuleData f α]
-: FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyOut PackageData f α]
-: FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
 instance (priority := low) {p : NPackage n} : FamilyDef BuildData
-  (.customTarget p.toPackage.name t) (CustomData (n,t)) := ⟨by simp⟩
+  (.customTarget p.toPackage.name t) (CustomData n t) := ⟨by simp⟩
 
-instance {p : NPackage n} [FamilyOut CustomData (n, t) α]
+instance {p : NPackage n} [FamilyOut (CustomData n) t α]
 : FamilyDef BuildData (BuildInfo.key (.target p.toPackage t)) α where
-  family_key_eq_type := by unfold BuildData; simp
+  fam_eq := by unfold BuildData; simp
 
-instance [FamilyOut TargetData (`leanLib ++ f) α]
-: FamilyDef BuildData (BuildInfo.key (.libraryFacet l f)) α where
-  family_key_eq_type := by unfold BuildData; simp
+instance {p : NPackage n} [FamilyOut BuildData (.packageTarget n t) α]
+: FamilyDef BuildData (BuildInfo.key (.target p.toPackage t)) α where
+  fam_eq := by unfold BuildInfo.key Package.targetBuildKey; simp
 
-instance [FamilyOut TargetData LeanExe.exeFacet α]
-: FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyOut TargetData ExternLib.staticFacet α]
-: FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyOut TargetData ExternLib.sharedFacet α]
-: FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyOut TargetData ExternLib.dynlibFacet α]
-: FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where
-  family_key_eq_type := by unfold BuildData; simp
+instance [FamilyOut FacetOut f α]
+: FamilyDef BuildData (BuildInfo.key (.facet t k d f)) α where
+  fam_eq := by unfold BuildData; simp
 
 --------------------------------------------------------------------------------
 /-! ## Build Info & Facets                                                    -/
@@ -123,33 +112,32 @@ These are defined here because they need configuration definitions
 definitions.
 -/
 
+data_type module : Module
+data_type package : Package
+data_type lean_lib : LeanLib
+data_type lean_exe : LeanExe
+data_type extern_lib : ExternLib
+
 /-- The direct local imports of the Lean module. -/
-abbrev Module.importsFacet := `imports
-module_data imports : Array Module
+builtin_facet imports : Module => Array Module
 
 /-- The transitive local imports of the Lean module. -/
-abbrev Module.transImportsFacet := `transImports
-module_data transImports : Array Module
+builtin_facet transImports : Module => Array Module
 
 /-- The transitive local imports of the Lean module. -/
-abbrev Module.precompileImportsFacet := `precompileImports
-module_data precompileImports : Array Module
+builtin_facet precompileImports : Module => Array Module
 
 /-- Shared library for `--load-dynlib`. -/
-abbrev Module.dynlibFacet := `dynlib
-module_data dynlib : Dynlib
+builtin_facet dynlib : Module => Dynlib
 
 /-- A Lean library's Lean modules. -/
-abbrev LeanLib.modulesFacet := `modules
-library_data modules : Array Module
+builtin_facet modules : LeanLib => Array Module
 
 /-- The package's array of dependencies. -/
-abbrev Package.depsFacet := `deps
-package_data deps : Array Package
+builtin_facet deps : Package => Array Package
 
 /-- The package's complete array of transitive dependencies. -/
-abbrev Package.transDepsFacet := `transDeps
-package_data transDeps : Array Package
+builtin_facet transDeps : Package => Array Package
 
 /-!
 ### Facet Build Info Helper Constructors
@@ -158,155 +146,226 @@ Definitions to easily construct `BuildInfo` values for module, package,
 and target facets.
 -/
 
+/--
+Build info for applying the specified facet to the module.
+It is the user's obiligation to ensure the facet in question is a module facet.
+-/
+abbrev Module.facetCore (facet : Name) (self : Module) : BuildInfo :=
+  .facet self.buildKey facetKind (toFamily self) facet
+
+/-- Build info for a module facet. -/
+abbrev Module.facet (facet : Name) (self : Module) : BuildInfo :=
+  self.facetCore (Module.facetKind ++ facet)
+
+@[deprecated Module.facetCore (since := "2025-03-04")]
+abbrev BuildInfo.moduleFacet (module : Module) (facet : Name) : BuildInfo :=
+  module.facetCore facet
+
 namespace Module
 
-/-- Build info for the module's specified facet. -/
-abbrev facet (facet : Name) (self : Module) : BuildInfo :=
-  .moduleFacet self facet
-
 @[inherit_doc importsFacet] abbrev imports (self : Module) :=
-  self.facet importsFacet
+  self.facetCore importsFacet
 
 @[inherit_doc transImportsFacet] abbrev transImports (self : Module) :=
-  self.facet transImportsFacet
+  self.facetCore transImportsFacet
 
 @[inherit_doc precompileImportsFacet] abbrev precompileImports (self : Module) :=
-  self.facet precompileImportsFacet
+  self.facetCore precompileImportsFacet
 
 @[inherit_doc depsFacet] abbrev deps  (self : Module) :=
-  self.facet depsFacet
+  self.facetCore depsFacet
 
 @[inherit_doc leanArtsFacet] abbrev leanArts  (self : Module) :=
-  self.facet leanArtsFacet
+  self.facetCore leanArtsFacet
 
 @[inherit_doc oleanFacet] abbrev olean (self : Module) :=
-  self.facet oleanFacet
+  self.facetCore oleanFacet
 
 @[inherit_doc ileanFacet] abbrev ilean (self : Module)  :=
-  self.facet ileanFacet
+  self.facetCore ileanFacet
 
 @[inherit_doc cFacet] abbrev c (self : Module) :=
-  self.facet cFacet
+  self.facetCore cFacet
 
 @[inherit_doc cFacet] abbrev bc (self : Module) :=
-  self.facet bcFacet
+  self.facetCore bcFacet
 
 @[inherit_doc oFacet] abbrev o (self : Module) :=
-  self.facet oFacet
+  self.facetCore oFacet
 
 @[inherit_doc oExportFacet] abbrev oExport (self : Module) :=
-  self.facet oExportFacet
+  self.facetCore oExportFacet
 
 @[inherit_doc oNoExportFacet] abbrev oNoExport (self : Module) :=
-  self.facet oNoExportFacet
+  self.facetCore oNoExportFacet
 
 @[inherit_doc coFacet] abbrev co (self : Module) :=
-  self.facet coFacet
+  self.facetCore coFacet
 
 @[inherit_doc coExportFacet] abbrev coExport (self : Module) :=
-  self.facet coExportFacet
+  self.facetCore coExportFacet
 
 @[inherit_doc coNoExportFacet] abbrev coNoExport (self : Module) :=
-  self.facet coNoExportFacet
+  self.facetCore coNoExportFacet
 
 @[inherit_doc bcoFacet] abbrev bco (self : Module) :=
-  self.facet bcoFacet
+  self.facetCore bcoFacet
 
 @[inherit_doc dynlibFacet] abbrev dynlib (self : Module) :=
-  self.facet dynlibFacet
+  self.facetCore dynlibFacet
 
 end Module
 
-/-- Build info for the package's specified facet. -/
-abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
-  .packageFacet self facet
-
-@[inherit_doc buildCacheFacet]
-abbrev Package.buildCache (self : Package) : BuildInfo :=
-  self.facet buildCacheFacet
-
-@[inherit_doc optBuildCacheFacet]
-abbrev Package.optBuildCache (self : Package) : BuildInfo :=
-  self.facet optBuildCacheFacet
-
-@[inherit_doc reservoirBarrelFacet]
-abbrev Package.reservoirBarrel (self : Package) : BuildInfo :=
-  self.facet reservoirBarrelFacet
-
-@[inherit_doc optReservoirBarrelFacet]
-abbrev Package.optReservoirBarrel (self : Package) : BuildInfo :=
-  self.facet optReservoirBarrelFacet
-
-@[inherit_doc gitHubReleaseFacet]
-abbrev Package.gitHubRelease (self : Package) : BuildInfo :=
-  self.facet gitHubReleaseFacet
-
-@[inherit_doc optGitHubReleaseFacet]
-abbrev Package.optGitHubRelease (self : Package) : BuildInfo :=
-  self.facet optGitHubReleaseFacet
-
-@[deprecated gitHubRelease (since := "2024-09-27")]
-abbrev Package.release := @gitHubRelease
-
-@[deprecated optGitHubRelease (since := "2024-09-27")]
-abbrev Package.optRelease := @optGitHubRelease
-
-@[inherit_doc extraDepFacet]
-abbrev Package.extraDep (self : Package) : BuildInfo :=
-  self.facet extraDepFacet
-
-@[inherit_doc depsFacet]
-abbrev Package.deps (self : Package) : BuildInfo :=
-  self.facet depsFacet
-
-@[inherit_doc transDepsFacet]
-abbrev Package.transDeps (self : Package) : BuildInfo :=
-  self.facet transDepsFacet
-
-/-- Build info for a custom package target. -/
+/-- Build info for a package target (e.g., a library, executable, or custom target). -/
 abbrev Package.target (target : Name) (self : Package) : BuildInfo :=
   .target self target
 
-/-- Build info of the Lean library's Lean binaries. -/
-abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
-  .libraryFacet self facet
+/-
+Build info for applying the specified facet to the package.
+It is the user's obiligation to ensure the facet in question is a package facet.
+-/
+abbrev Package.facetCore (facet : Name) (self : Package) : BuildInfo :=
+  .facet self.buildKey facetKind (toFamily self) facet
 
-@[inherit_doc modulesFacet]
-abbrev LeanLib.modules (self : LeanLib) : BuildInfo :=
-  self.facet modulesFacet
+/-- Build info for a package facet. -/
+abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
+  self.facetCore (Package.facetKind ++ facet)
 
-@[inherit_doc leanArtsFacet]
-abbrev LeanLib.leanArts (self : LeanLib) : BuildInfo :=
-  self.facet leanArtsFacet
+@[deprecated Package.facetCore (since := "2025-03-04")]
+abbrev BuildInfo.packageFacet (package : Package) (facet : Name) : BuildInfo :=
+  package.facetCore facet
 
-@[inherit_doc staticFacet]
-abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
-  self.facet staticFacet
+namespace Package
 
-@[inherit_doc staticExportFacet]
-abbrev LeanLib.staticExport (self : LeanLib) : BuildInfo :=
-  self.facet staticExportFacet
+@[inherit_doc buildCacheFacet]
+abbrev buildCache (self : Package) : BuildInfo :=
+  self.facetCore buildCacheFacet
 
-@[inherit_doc sharedFacet]
-abbrev LeanLib.shared (self : LeanLib) : BuildInfo :=
-  self.facet sharedFacet
+@[inherit_doc optBuildCacheFacet]
+abbrev optBuildCache (self : Package) : BuildInfo :=
+  self.facetCore optBuildCacheFacet
+
+@[inherit_doc reservoirBarrelFacet]
+abbrev reservoirBarrel (self : Package) : BuildInfo :=
+  self.facetCore reservoirBarrelFacet
+
+@[inherit_doc optReservoirBarrelFacet]
+abbrev optReservoirBarrel (self : Package) : BuildInfo :=
+  self.facetCore optReservoirBarrelFacet
+
+@[inherit_doc gitHubReleaseFacet]
+abbrev gitHubRelease (self : Package) : BuildInfo :=
+  self.facetCore gitHubReleaseFacet
+
+@[inherit_doc optGitHubReleaseFacet]
+abbrev optGitHubRelease (self : Package) : BuildInfo :=
+  self.facetCore optGitHubReleaseFacet
+
+@[deprecated gitHubRelease (since := "2024-09-27")]
+abbrev release := @gitHubRelease
+
+@[deprecated optGitHubRelease (since := "2024-09-27")]
+abbrev optRelease := @optGitHubRelease
 
 @[inherit_doc extraDepFacet]
-abbrev LeanLib.extraDep (self : LeanLib) : BuildInfo :=
-  self.facet extraDepFacet
+abbrev extraDep (self : Package) : BuildInfo :=
+  self.facetCore extraDepFacet
+
+@[inherit_doc depsFacet]
+abbrev deps (self : Package) : BuildInfo :=
+  self.facetCore depsFacet
+
+@[inherit_doc transDepsFacet]
+abbrev transDeps (self : Package) : BuildInfo :=
+  self.facetCore transDepsFacet
+
+end Package
+
+/-
+Build info for applying the specified facet to the library.
+It is the user's obiligation to ensure the facet in question is a library facet.
+-/
+abbrev LeanLib.facetCore (facet : Name) (self : LeanLib) : BuildInfo :=
+  .facet self.buildKey facetKind (toFamily self) facet
+
+/-- Build info for a facet of a Lean library. -/
+abbrev LeanLib.facet (facet : Name) (self : LeanLib) : BuildInfo :=
+  self.facetCore (LeanLib.facetKind ++ facet)
+
+@[deprecated LeanLib.facetCore (since := "2025-03-04")]
+abbrev BuildInfo.libraryFacet (lib : LeanLib) (facet : Name) : BuildInfo :=
+  lib.facetCore facet
+
+namespace LeanLib
+
+@[inherit_doc modulesFacet]
+abbrev modules (self : LeanLib) : BuildInfo :=
+  self.facetCore modulesFacet
+
+@[inherit_doc leanArtsFacet]
+abbrev leanArts (self : LeanLib) : BuildInfo :=
+  self.facetCore leanArtsFacet
+
+@[inherit_doc staticFacet]
+abbrev static (self : LeanLib) : BuildInfo :=
+  self.facetCore staticFacet
+
+@[inherit_doc staticExportFacet]
+abbrev staticExport (self : LeanLib) : BuildInfo :=
+  self.facetCore staticExportFacet
+
+@[inherit_doc sharedFacet]
+abbrev shared (self : LeanLib) : BuildInfo :=
+  self.facetCore sharedFacet
+
+@[inherit_doc extraDepFacet]
+abbrev extraDep (self : LeanLib) : BuildInfo :=
+  self.facetCore extraDepFacet
+
+end LeanLib
+
+/-
+Build info for applying the specified facet to the executable.
+It is the user's obiligation to ensure the facet in question is the executable facet.
+-/
+abbrev LeanExe.facetCore (facet : Name) (self : LeanExe) : BuildInfo :=
+  .facet self.buildKey facetKind (toFamily self) facet
 
 /-- Build info of the Lean executable. -/
 abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=
-  .leanExe self
+  self.facetCore LeanExe.exeFacet
+
+@[deprecated LeanExe.exe (since := "2025-03-04")]
+abbrev BuildInfo.leanExe (exe : LeanExe) : BuildInfo :=
+  exe.exe
+
+/-
+Build info for applying the specified facet to the external library.
+It is the user's obiligation to ensure the facet in question is an external library facet.
+-/
+abbrev ExternLib.facetCore (facet : Name) (self : ExternLib) : BuildInfo :=
+  .facet self.buildKey facetKind (toFamily self) facet
 
 /-- Build info of the external library's static binary. -/
 abbrev ExternLib.static (self : ExternLib) : BuildInfo :=
-  .staticExternLib self
+  self.facetCore ExternLib.staticFacet
+
+@[deprecated ExternLib.static (since := "2025-03-04")]
+abbrev BuildInfo.staticExternLib (lib : ExternLib) : BuildInfo :=
+  lib.facetCore ExternLib.staticFacet
 
 /-- Build info of the external library's shared binary. -/
 abbrev ExternLib.shared (self : ExternLib) : BuildInfo :=
-  .sharedExternLib self
+  self.facetCore ExternLib.sharedFacet
+
+@[deprecated ExternLib.shared (since := "2025-03-04")]
+abbrev BuildInfo.sharedExternLib (lib : ExternLib) : BuildInfo :=
+  lib.facetCore  ExternLib.sharedFacet
 
 /-- Build info of the external library's dynlib. -/
 abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo :=
-  .dynlibExternLib self
+  self.facetCore ExternLib.dynlibFacet
+
+@[deprecated ExternLib.dynlib (since := "2025-03-04")]
+abbrev BuildInfo.dynlibExternLib (lib : ExternLib) : BuildInfo :=
+  lib.facetCore ExternLib.dynlibFacet
diff --git a/src/lake/Lake/Build/InitFacets.lean b/src/lake/Lake/Build/InitFacets.lean
new file mode 100644
index 0000000000..8dbdd3d21b
--- /dev/null
+++ b/src/lake/Lake/Build/InitFacets.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Build.Module
+import Lake.Build.Package
+import Lake.Build.Library
+import Lake.Build.Executable
+import Lake.Build.ExternLib
+
+/-! # Initial Facets -/
+
+namespace Lake
+
+/-- The initial set of Lake facets. -/
+def initFacetConfigs : DNameMap FacetConfig :=
+  DNameMap.empty
+  |> insert Module.initFacetConfigs
+  |> insert Package.initFacetConfigs
+  |> insert LeanLib.initFacetConfigs
+  |> insert LeanExe.initFacetConfigs
+  |> insert ExternLib.initFacetConfigs
+where
+  insert {k} (group : DNameMap (KFacetConfig k)) map :=
+    group.fold (init := map) fun m k v => m.insert k v.toFacetConfig
diff --git a/src/lake/Lake/Build/Job/Basic.lean b/src/lake/Lake/Build/Job/Basic.lean
index 7f34072d39..d7d9b0bd13 100644
--- a/src/lake/Lake/Build/Job/Basic.lean
+++ b/src/lake/Lake/Build/Job/Basic.lean
@@ -8,6 +8,7 @@ import Lake.Util.Log
 import Lake.Util.Task
 import Lake.Util.Opaque
 import Lake.Build.Trace
+import Lake.Build.Data
 
 /-! # Job Primitives
 
@@ -16,7 +17,7 @@ it defines `OpaqueJob`, which is needed for `BuildContext`. More complex
 utilities are defined in `Lake.Build.Job.Monad`, which depends on `BuildContext`.
 -/
 
-open System
+open System Lean
 
 namespace Lake
 
@@ -88,9 +89,11 @@ abbrev JobTask α := BaseIOTask (JobResult α)
 /-! ## Job -/
 
 /-- A Lake job. -/
-structure Job (α : Type u)  where
+structure Job (α : Type u) where
   /-- The Lean `Task` object for the job. -/
   task : JobTask α
+   /-- The kind of data this job produces. -/
+  [kind : OptDataKind α]
   /--
   A caption for the job in Lake's build monitor.
   Will be formatted like `✔ [3/5] Ran <caption>`.
@@ -98,18 +101,28 @@ structure Job (α : Type u)  where
   caption : String
   /-- Whether this job failing should cause the build to fail. -/
   optional : Bool := false
-  deriving Inhabited
+
+instance : Inhabited (Job α) := ⟨{task := default, caption := default, kind := .anonymous}⟩
 
 namespace Job
 
-@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
+protected def cast (self : Job α) (h : ¬ self.kind.isAnonymous) : Job (DataType self.kind) :=
+  let h := by
+    match kind_eq:self.kind with
+    | ⟨_, wf⟩ =>
+      simp only
+      simp only [OptDataKind.isAnonymous, kind_eq] at h
+      rw [wf h]
+  cast h self
+
+@[inline] def ofTask [OptDataKind α] (task : JobTask α) (caption := "") : Job α :=
   {task, caption}
 
-@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
-  {task := Task.pure (.error 0 {log}), caption}
+@[inline] protected def error [OptDataKind α] (log : Log := {}) (caption := "") : Job α :=
+  .ofTask (Task.pure (.error 0 {log})) caption
 
-@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
-  {task := Task.pure (.ok a {log}), caption}
+@[inline] protected def pure [kind : OptDataKind α] (a : α) (log : Log := {}) (caption := "") : Job α :=
+  .ofTask (Task.pure (.ok a {log})) caption
 
 instance : Pure Job := ⟨Job.pure⟩
 
@@ -128,12 +141,12 @@ instance : Pure Job := ⟨Job.pure⟩
   if job.caption.isEmpty then {job with caption} else job
 
 @[inline] def mapResult
-  (f : JobResult α → JobResult β) (self : Job α)
+  [OptDataKind β] (f : JobResult α → JobResult β) (self : Job α)
   (prio := Task.Priority.default) (sync := false)
-: Job β := {self with task := self.task.map f prio sync}
+: Job β := {self with task := self.task.map f prio sync, kind := inferInstance}
 
 @[inline] def mapOk
-  (f : α → JobState → JobResult β) (self : Job α)
+  [OptDataKind β] (f : α → JobState → JobResult β) (self : Job α)
   (prio := Task.Priority.default) (sync := false)
 : Job β :=
   self.mapResult (prio := prio) (sync := sync) fun
@@ -141,7 +154,7 @@ instance : Pure Job := ⟨Job.pure⟩
     | .error e s => .error e s
 
 @[inline] protected def map
-  (f : α → β) (self : Job α)
+  [OptDataKind β] (f : α → β) (self : Job α)
   (prio := Task.Priority.default) (sync := false)
 : Job β := self.mapResult (·.map f) prio sync
 
@@ -151,15 +164,24 @@ end Job
 
 /-! ## OpaqueJob -/
 
+/-- A Lake job task with an opaque value in `Type`. -/
+abbrev OpaqueJobTask := JobTask Opaque
+
+@[inline] private unsafe def JobTask.toOpaqueImpl (self : JobTask α) : OpaqueJobTask :=
+  unsafeCast self
+
+/-- Forget the value of a job task. Implemented as a no-op cast. -/
+@[implemented_by toOpaqueImpl]
+def JobTask.toOpaque (self : JobTask α) : OpaqueJobTask :=
+  self.map (·.map Opaque.mk)
+
+instance : CoeOut (JobTask α) OpaqueJobTask := ⟨.toOpaque⟩
+
 /-- A Lake job with an opaque value in `Type`. -/
 abbrev OpaqueJob := Job Opaque
 
-@[inline] private unsafe def Job.toOpaqueImpl (job : Job α) : OpaqueJob :=
-  unsafeCast job
-
-/-- Forget the value of a job. Implemented as a no-op cast. -/
-@[implemented_by toOpaqueImpl]
+/-- Forget the value of a job. Implemented as a no-op cast on the task. -/
 def Job.toOpaque (job : Job α) : OpaqueJob :=
-  {job with task := job.task.map (·.map Opaque.mk)}
+  {job with task := job.task.toOpaque, kind := .anonymous}
 
 instance : CoeOut (Job α) OpaqueJob := ⟨.toOpaque⟩
diff --git a/src/lake/Lake/Build/Job/Monad.lean b/src/lake/Lake/Build/Job/Monad.lean
index bac2e2c748..d503fe76e2 100644
--- a/src/lake/Lake/Build/Job/Monad.lean
+++ b/src/lake/Lake/Build/Job/Monad.lean
@@ -101,13 +101,14 @@ example : MonadLiftT SpawnM FetchM := inferInstance
 
 namespace Job
 
-@[inline] def bindTask [Monad m]
+@[inline] def bindTask
+  [Monad m] [OptDataKind β]
   (f : JobTask α → m (JobTask β)) (self : Job α)
-: m (Job β) := return {self with task := ← f self.task}
+: m (Job β) := return {self with task := ← f self.task, kind := inferInstance}
 
 /-- Spawn a job that asynchronously performs `act`. -/
 @[inline] protected def async
-  (act : JobM α) (prio := Task.Priority.default) (caption := "")
+  [OptDataKind α] (act : JobM α) (prio := Task.Priority.default) (caption := "")
 : SpawnM (Job α) := fun fetch stack store ctx => .ofTask (caption := caption) <$> do
   BaseIO.asTask (prio := prio) do (withLoggedIO act) fetch stack store ctx {}
 
@@ -133,7 +134,7 @@ Logs the job's log and throws if there was an error.
 
 /-- Apply `f` asynchronously to the job's output. -/
 protected def mapM
-  (self : Job α) (f : α → JobM β)
+  [OptDataKind β] (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) :=
   fun fetch stack store ctx trace => do
@@ -146,7 +147,7 @@ protected def mapM
 
 @[deprecated Job.mapM (since := "2024-12-06")]
 protected abbrev bindSync
-  (self : Job α) (f : α → JobM β)
+  [OptDataKind β] (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) := self.mapM f prio sync
 
@@ -155,7 +156,7 @@ Apply `f` asynchronously to the job's output
 and asynchronously await the resulting job.
 -/
 def bindM
-  (self : Job α) (f : α → JobM (Job β))
+  [OptDataKind β] (self : Job α) (f : α → JobM (Job β))
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) :=
   fun fetch stack store ctx trace => do
@@ -173,7 +174,7 @@ def bindM
 
 @[deprecated bindM (since := "2024-12-06")]
 protected abbrev bindAsync
-  (self : Job α) (f : α → SpawnM (Job β))
+  [OptDataKind β] (self : Job α) (f : α → SpawnM (Job β))
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) := self.bindM (fun a => f a) prio sync
 
@@ -182,7 +183,7 @@ protected abbrev bindAsync
 results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 -/
 @[inline] def zipResultWith
-  (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
+  [OptDataKind γ] (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
   (prio := Task.Priority.default) (sync := true)
 : Job γ := Job.ofTask $
   self.task.bind (prio := prio) (sync := true) fun rx =>
@@ -194,7 +195,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 -/
 @[inline] def zipWith
-  (f : α → β → γ) (self : Job α) (other : Job β)
+  [OptDataKind γ] (f : α → β → γ) (self : Job α) (other : Job β)
   (prio := Task.Priority.default) (sync := true)
 : Job γ :=
   self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
@@ -203,6 +204,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 
 /-- Merges this job with another, discarding its output and trace. -/
 def add (self : Job α) (other : Job β) : Job α :=
+  have : OptDataKind α := self.kind
   self.zipResultWith (other := other) fun
   | .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
   | ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
@@ -221,11 +223,11 @@ def mixArray (jobs : Array (Job α)) : Job Unit :=
 
 /-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
 def collectList (jobs : List (Job α)) : Job (List α) :=
-  jobs.foldr (zipWith List.cons) (pure [])
+  jobs.foldr (zipWith List.cons) (.pure [])
 
 /-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
 def collectArray (jobs : Array (Job α)) : Job (Array α) :=
-  jobs.foldl (zipWith Array.push) (pure (Array.mkEmpty jobs.size))
+  jobs.foldl (zipWith Array.push) (.pure (Array.mkEmpty jobs.size))
 
 end Job
 
@@ -252,27 +254,27 @@ abbrev nil : BuildJob Unit :=
   Job.pure ()
 
 @[deprecated Job.map (since := "2024-12-06")]
-protected abbrev pure (a : α) : BuildJob α :=
+protected abbrev pure [OptDataKind α] (a : α) : BuildJob α :=
   Job.pure a
 
 instance : Pure BuildJob := ⟨Job.pure⟩
 
 @[deprecated Job.map (since := "2024-12-06")]
-protected abbrev map (f : α → β) (self : BuildJob α) : BuildJob β :=
+protected abbrev map [OptDataKind β] (f : α → β) (self : BuildJob α) : BuildJob β :=
   self.toJob.map f
 
 instance : Functor BuildJob where
   map := Job.map
 
 @[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
-def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
+def mapWithTrace [OptDataKind β] (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
   self.toJob.mapOk fun a s =>
     let (b, trace) := f a s.trace
     .ok b {s with trace}
 
 @[inline, deprecated Job.mapM (since := "2024-12-06")]
 protected def bindSync
-  (self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
+  [OptDataKind β] (self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
   (prio : Task.Priority := .default) (sync := false)
 : SpawnM (Job β) :=
   self.toJob.mapM (prio := prio) (sync := sync) fun a => do
@@ -282,7 +284,7 @@ protected def bindSync
 
 @[inline, deprecated Job.bindM (since := "2024-12-06")]
 protected def bindAsync
-  (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
+  [OptDataKind β] (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
   (prio : Task.Priority := .default) (sync := false)
  : SpawnM (Job β)  :=
   self.toJob.bindM (prio := prio) (sync := sync) fun a => do
@@ -310,7 +312,7 @@ abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
 
 @[deprecated Job.zipWith (since := "2024-12-06")]
 abbrev zipWith
-  (f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
+  [OptDataKind γ] (f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
 : BuildJob γ :=
   self.toJob.zipWith f other.toJob
 
diff --git a/src/lake/Lake/Build/Job/Register.lean b/src/lake/Lake/Build/Job/Register.lean
index 18102c87e9..a418994438 100644
--- a/src/lake/Lake/Build/Job/Register.lean
+++ b/src/lake/Lake/Build/Job/Register.lean
@@ -42,7 +42,7 @@ Registers the job for the top-level build monitor,
 
 /-- Wraps stray I/O, logs, and errors in `x` into the produced job.  -/
 def ensureJob
-  (x : FetchM (Job α))
+  [OptDataKind α] (x : FetchM (Job α))
 : FetchM (Job α) := fun fetch stack store ctx log => do
   let iniPos := log.endPos
   match (← (withLoggedIO x) fetch stack store ctx log) with
@@ -64,7 +64,7 @@ Registers the produced job for the top-level build monitor
 Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
 -/
 def withRegisterJob
-  (caption : String) (x : FetchM (Job α)) (optional := false)
+  [OptDataKind α] (caption : String) (x : FetchM (Job α)) (optional := false)
 : FetchM (Job α) := do
   let job ← ensureJob x
   registerJob caption job optional
diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean
index 97b6329fe8..7d8f4eec15 100644
--- a/src/lake/Lake/Build/Key.lean
+++ b/src/lake/Lake/Build/Key.lean
@@ -11,108 +11,106 @@ open Lean (Name)
 
 /-- The type of keys in the Lake build store. -/
 inductive BuildKey
-| moduleFacet (module : Name) (facet : Name)
-| packageFacet (package : Name) (facet : Name)
-| targetFacet (package : Name) (target : Name) (facet : Name)
-| customTarget (package : Name) (target : Name)
+| module (module : Name)
+| package (package : Name)
+| packageTarget (package target : Name)
+| facet (target : BuildKey) (facet : Name)
 deriving Inhabited, Repr, DecidableEq, Hashable
 
+/-- The kind identifier for facets of a package. -/
+@[match_pattern] abbrev Package.facetKind : Name := `package
+
+/-- The kind identifier for facets of a (Lean) module. -/
+@[match_pattern] abbrev Module.facetKind : Name := `module
+
 namespace BuildKey
 
+@[match_pattern] abbrev moduleFacet (module facet : Name) : BuildKey :=
+  .facet (.module module) facet
+
+@[match_pattern] abbrev packageFacet (package facet : Name) : BuildKey :=
+  .facet (.package package) facet
+
+@[match_pattern] abbrev targetFacet (package target facet : Name) : BuildKey :=
+  .facet (.packageTarget package target) facet
+
+@[match_pattern] abbrev customTarget (package target : Name) : BuildKey :=
+  .packageTarget package target
+
 def toString : (self : BuildKey) → String
-| moduleFacet m f => s!"+{m}:{f}"
-| packageFacet p f => s!"@{p}:{f}"
-| targetFacet p t f => s!"{p}/{t}:{f}"
-| customTarget p t => s!"{p}/{t}"
+| module m => s!"+{m}"
+| package p => s!"@{p}"
+| packageTarget p t => s!"{p}/{t}"
+| facet t f => s!"{toString t}:{Name.eraseHead f}"
 
 /-- Like the default `toString`, but without disambiguation markers. -/
 def toSimpleString : (self : BuildKey) → String
-| moduleFacet m f => s!"{m}:{f}"
-| packageFacet p f => s!"{p}:{f}"
-| targetFacet p t f => s!"{p}/{t}:{eraseHead f}"
-| customTarget p t => s!"{p}/{t}"
-where
-  eraseHead : Name → Name
-    | .anonymous | .str .anonymous _  | .num .anonymous _  => .anonymous
-    | .str p s => .str (eraseHead p) s
-    | .num p s => .num (eraseHead p) s
+| module m => s!"{m}"
+| package p => s!"{p}"
+| packageTarget p t => s!"{p}/{t}"
+| facet t f => s!"{toSimpleString t}:{Name.eraseHead f}"
 
 instance : ToString BuildKey := ⟨(·.toString)⟩
 
 def quickCmp (k k' : BuildKey) : Ordering :=
   match k with
-  | moduleFacet m f =>
+  | module m =>
     match k' with
-    | moduleFacet m' f' =>
-      match m.quickCmp m' with
-      | .eq => f.quickCmp f'
-      | ord => ord
+    | module m' => m.quickCmp m'
     | _ => .lt
-  | packageFacet p f =>
+  | package p =>
     match k' with
-    | moduleFacet .. => .gt
-    | packageFacet p' f' =>
-      match p.quickCmp p' with
-      | .eq => f.quickCmp f'
-      | ord => ord
+    | module .. => .gt
+    | package p' => p.quickCmp p'
     | _ => .lt
-  | targetFacet p t f =>
+  | packageTarget p t =>
     match k' with
-    | customTarget .. => .lt
-    | targetFacet p' t' f' =>
-      match p.quickCmp p' with
-      | .eq =>
-        match t.quickCmp t' with
-        | .eq => f.quickCmp f'
-        | ord => ord
-      | ord => ord
-    | _=> .gt
-  | customTarget p t =>
-    match k' with
-    | customTarget p' t' =>
+    | facet .. => .lt
+    | packageTarget p' t' =>
       match p.quickCmp p' with
       | .eq => t.quickCmp t'
       | ord => ord
+    | _=> .gt
+  | facet t f =>
+    match k' with
+    | facet t' f' =>
+      match t.quickCmp t' with
+      | .eq => f.quickCmp f'
+      | ord => ord
     | _ => .gt
 
-theorem eq_of_quickCmp {k k' : BuildKey}  :
-quickCmp k k' = Ordering.eq → k = k' := by
-  unfold quickCmp
-  cases k with
-  | moduleFacet m f =>
-    cases k'
-    case moduleFacet m' f' =>
-      dsimp only; split
-      next m_eq => intro f_eq; rw [eq_of_cmp m_eq, eq_of_cmp f_eq]
-      next => intro; contradiction
+theorem eq_of_quickCmp :
+  quickCmp k k' = Ordering.eq → k = k'
+:= by
+  revert k'
+  induction k with
+  | module m =>
+    unfold quickCmp
+    intro k'; cases k'
+    case module m' => simp
     all_goals (intro; contradiction)
-  | packageFacet p f =>
-    cases k'
-    case packageFacet p' f' =>
-      dsimp only; split
-      next p_eq => intro f_eq; rw [eq_of_cmp p_eq, eq_of_cmp f_eq]
-      next => intro; contradiction
+  | package p =>
+    unfold quickCmp
+    intro k'; cases k'
+    case package p' => simp
     all_goals (intro; contradiction)
-  | targetFacet p t f =>
-    cases k'
-    case targetFacet p' t' f' =>
-      dsimp only; split
-      next p_eq =>
-        split
-        next t_eq =>
-          intro f_eq
-          rw [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp f_eq]
-        next => intro; contradiction
-      next => intro; contradiction
-    all_goals (intro; contradiction)
-  | customTarget p t =>
-    cases k'
-    case customTarget p' t' =>
+  | packageTarget p t =>
+    unfold quickCmp
+    intro k'; cases k'
+    case packageTarget p' t' =>
       dsimp only; split
       next p_eq => intro t_eq; rw [eq_of_cmp p_eq, eq_of_cmp t_eq]
       next => intro; contradiction
     all_goals (intro; contradiction)
+  | facet t f ih =>
+    unfold quickCmp
+    intro k'; cases k'
+    case facet t' f'' =>
+      dsimp only; split
+      next t_eq => intro f_eq; rw [ih t_eq, eq_of_cmp f_eq]
+      next => intro; contradiction
+    all_goals (intro; contradiction)
 
 instance : LawfulCmpEq BuildKey quickCmp where
   eq_of_cmp := eq_of_quickCmp
-  cmp_rfl {k} := by cases k <;> simp [quickCmp]
+  cmp_rfl {k} := by induction k <;> simp_all [quickCmp]
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 3d7c76887f..46dc47ed9a 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -63,7 +63,7 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
   withRegisterJob s!"{self.name}:static{suffix}" do
   let mods ← (← self.modules.fetch).await
   let oJobs ← mods.flatMapM fun mod =>
-    mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
+    mod.nativeFacets shouldExport |>.mapM (·.fetch mod)
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
   /-
   Static libraries with explicit exports are built as thin libraries.
@@ -80,7 +80,6 @@ def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
 def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet :=
   mkFacetJobConfig (LeanLib.recBuildStatic · true)
 
-
 /-! ## Build Shared Lib -/
 
 protected def LeanLib.recBuildShared
@@ -88,7 +87,7 @@ protected def LeanLib.recBuildShared
   withRegisterJob s!"{self.name}:shared" do
   let mods ← (← self.modules.fetch).await
   let oJobs ← mods.flatMapM fun mod =>
-    mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
+    mod.nativeFacets true |>.mapM (·.fetch mod)
   let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
   let externJobs ← pkgs.flatMapM (·.externLibs.mapM (·.shared.fetch))
   buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.weakLinkArgs self.linkArgs
@@ -108,16 +107,30 @@ def LeanLib.recBuildExtraDepTargets (self : LeanLib) : FetchM (Job Unit) := do
 def LeanLib.extraDepFacetConfig : LibraryFacetConfig extraDepFacet :=
   mkFacetJobConfig LeanLib.recBuildExtraDepTargets
 
-open LeanLib in
+/-- Build the default facets for the library. -/
+def LeanLib.recBuildDefaultFacets (self : LeanLib) : FetchM (Job Unit) := do
+  Job.mixArray <$> self.defaultFacets.mapM fun facet => do
+    let job ← (self.facetCore facet).fetch
+    return job.toOpaque
+
+/-- The `LibraryFacetConfig` for the builtin `defaultFacet`. -/
+def LeanLib.defaultFacetConfig : LibraryFacetConfig defaultFacet :=
+  mkFacetJobConfig LeanLib.recBuildDefaultFacets
+
 /--
-A library facet name to build function map that contains builders for
-the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`).
+A name-configuration map for the initial set of
+Lean library facets (e.g., `lean`, `static`, `shared`).
 -/
-def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
+def LeanLib.initFacetConfigs : DNameMap LeanLibFacetConfig :=
   DNameMap.empty
+  |>.insert defaultFacet defaultFacetConfig
   |>.insert modulesFacet modulesFacetConfig
   |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert staticFacet staticFacetConfig
   |>.insert staticExportFacet staticExportFacetConfig
   |>.insert sharedFacet sharedFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
+
+@[inherit_doc LeanLib.initFacetConfigs]
+abbrev initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
+  LeanLib.initFacetConfigs
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 83b622750e..c7c0129bf1 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -315,7 +315,7 @@ def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) :=
   withRegisterJob s!"{mod.name}:dynlib" do
 
   -- Fetch object files
-  let linkJobs ← mod.nativeFacets true |>.mapM (fetch <| mod.facet ·.name)
+  let linkJobs ← mod.nativeFacets true |>.mapM (·.fetch mod)
   let linksJob := Job.collectArray linkJobs
 
   -- Fetch dependencies' dynlibs
@@ -355,12 +355,11 @@ def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) :=
 def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
   mkFacetJobConfig Module.recBuildDynlib
 
-open Module in
 /--
 A name-configuration map for the initial set of
-Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
+Lake module facets (e.g., `imports`, `c`, `o`, `dynlib`).
 -/
-def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
+def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   DNameMap.empty
   |>.insert importsFacet importsFacetConfig
   |>.insert transImportsFacet transImportsFacetConfig
@@ -379,3 +378,6 @@ def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert oExportFacet oExportFacetConfig
   |>.insert oNoExportFacet oNoExportFacetConfig
   |>.insert dynlibFacet dynlibFacetConfig
+
+@[inherit_doc Module.initFacetConfigs]
+abbrev initModuleFacetConfigs := Module.initFacetConfigs
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index 95bb5628c3..96a9287678 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -37,7 +37,7 @@ def Package.recComputeTransDeps (self : Package) : FetchM (Job (Array Package))
     let some dep ← findPackage? cfg.name
       | error s!"{self.name}: package not found for dependency '{cfg.name}' \
         (this is likely a bug in Lake)"
-    let depDeps ← (← fetch <| dep.facet `transDeps).await
+    let depDeps ← (← fetch <| dep.transDeps).await
     return depDeps.foldl (·.insert ·) deps |>.insert dep
 
 /-- The `PackageFacetConfig` for the builtin `transDepsFacet`. -/
@@ -159,7 +159,7 @@ def Package.fetchBuildArchive
 private def Package.mkOptBuildArchiveFacetConfig
   {facet : Name} (archiveFile : Package → FilePath)
   (getUrl : Package → JobM String) (headers : Array String := #[])
-  [FamilyDef PackageData facet Bool]
+  [FamilyDef FacetOut facet Bool]
 : PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
   withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
   try
@@ -173,12 +173,12 @@ private def Package.mkOptBuildArchiveFacetConfig
 @[inline]
 private def Package.mkBuildArchiveFacetConfig
   {facet : Name} (optFacet : Name) (what : String)
-  [FamilyDef PackageData facet Unit]
-  [FamilyDef PackageData optFacet Bool]
+  [FamilyDef FacetOut facet Unit]
+  [FamilyDef FacetOut optFacet Bool]
 : PackageFacetConfig facet :=
   mkFacetJobConfig fun pkg =>
-    withRegisterJob s!"{pkg.name}:{facet}" do
-      (← fetch <| pkg.facet optFacet).mapM fun success => do
+    withRegisterJob s!"{pkg.name}:{Name.eraseHead facet}" do
+      (← fetch <| pkg.facetCore optFacet).mapM fun success => do
         unless success do
           error s!"failed to fetch {what}{← pkg.optFacetDetails optFacet}"
 
@@ -238,12 +238,11 @@ def Package.afterBuildCacheSync (self : Package) (build : JobM α) : FetchM (Job
 @[deprecated afterBuildCacheSync (since := "2024-09-27")]
 def Package.afterReleaseSync := @afterBuildCacheSync
 
-open Package in
 /--
-A package facet name to build function map that contains builders for
-the initial set of Lake package facets (e.g., `extraDep`).
+A name-configuration map for the initial set of
+Lake package facets (e.g., `extraDep`).
 -/
-def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
+def Package.initFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
   |>.insert transDepsFacet transDepsFacetConfig
@@ -254,3 +253,6 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   |>.insert reservoirBarrelFacet barrelFacetConfig
   |>.insert optGitHubReleaseFacet optGitHubReleaseFacetConfig
   |>.insert gitHubReleaseFacet gitHubReleaseFacetConfig
+
+@[inherit_doc Package.initFacetConfigs]
+abbrev initPackageFacetConfigs := Package.initFacetConfigs
diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean
index b6c68b0c9b..c0c947d016 100644
--- a/src/lake/Lake/Build/Run.lean
+++ b/src/lake/Lake/Build/Run.lean
@@ -6,6 +6,7 @@ Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 prelude
 import Lake.Util.Lock
 import Lake.Build.Index
+import Lake.Build.Job
 
 /-! # Build Runner
 
@@ -105,7 +106,7 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
 def reportJob (job : OpaqueJob) : MonitorM PUnit := do
   let {jobNo, totalJobs, ..} ← get
   let {failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
-  let {task, caption, optional} := job
+  let {task, caption, optional, ..} := job
   let {log, action, ..} := task.get.state
   let maxLv := log.maxLv
   let failed := log.hasEntries ∧ maxLv ≥ failLv
diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean
index 7b53e46f31..e173527744 100644
--- a/src/lake/Lake/Build/Store.lean
+++ b/src/lake/Lake/Build/Store.lean
@@ -32,7 +32,7 @@ namespace BuildStore
 
 /-- Derive an array of built module facets from the store. -/
 def collectModuleFacetArray
-  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+  (self : BuildStore) (facet : Name) [FamilyOut FacetOut facet α]
 : Array (Job α) := Id.run do
   let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
@@ -46,7 +46,7 @@ def collectModuleFacetArray
 
 /-- Derive a map of module names to built facets from the store. -/
 def collectModuleFacetMap
-  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+  (self : BuildStore) (facet : Name) [FamilyOut FacetOut facet α]
 : NameMap (Job α) := Id.run do
   let mut res := Lean.mkNameMap (Job α)
   for ⟨k, v⟩ in self do
@@ -60,12 +60,12 @@ def collectModuleFacetMap
 
 /-- Derive an array of built package facets from the store. -/
 def collectPackageFacetArray
-  (self : BuildStore) (facet : Name) [FamilyOut PackageData facet α]
+  (self : BuildStore) (facet : Name) [FamilyOut FacetOut facet α]
 : Array (Job α) := Id.run do
   let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
-    | .packageFacet _ f =>
+    | .packageFacet p f =>
       if h : f = facet then
         have of_data := by unfold BuildData; simp [h]
         res := res.push <| cast of_data v
@@ -74,19 +74,19 @@ def collectPackageFacetArray
 
 /-- Derive an array of built target facets from the store. -/
 def collectTargetFacetArray
-  (self : BuildStore) (facet : Name) [FamilyOut TargetData facet α]
+  (self : BuildStore) (facet : Name) [FamilyOut FacetOut facet α]
 : Array (Job α) := Id.run do
   let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .targetFacet _ _ f =>
-      if h : f = facet then
-        have of_data := by unfold BuildData; simp [h]
+      if hf : f = facet then
+        have of_data := by unfold BuildData; simp [hf]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built external shared libraries from the store. -/
 def collectSharedExternLibs
-  (self : BuildStore) [FamilyOut TargetData `externLib.shared α]
+  (self : BuildStore) [FamilyOut FacetOut `externLib.shared α]
 : Array (Job α) := self.collectTargetFacetArray `externLib.shared
diff --git a/src/lake/Lake/Build/Target/Fetch.lean b/src/lake/Lake/Build/Target/Fetch.lean
index 7af559acb3..23b6b7aff1 100644
--- a/src/lake/Lake/Build/Target/Fetch.lean
+++ b/src/lake/Lake/Build/Target/Fetch.lean
@@ -9,29 +9,31 @@ import Lake.Config.Monad
 
 namespace Lake
 
-protected def BuildKey.fetch (self : BuildKey) [h : FamilyOut BuildData self α] : FetchM (Job α) := do
-  match self_eq:self with
-  | moduleFacet modName facetName =>
+private def BuildKey.fetchCore (self : BuildKey) : FetchM (Job (BuildData self)) := do
+  match self with
+  | module modName =>
     let some mod ← findModule? modName
       | error s!"invalid target '{self}': module '{modName}' not found in workspace"
-    have : FamilyOut BuildData (mod.facet facetName).key α :=
-      ⟨by simpa [self_eq] using h.family_key_eq_type⟩
-    fetch <| mod.facet facetName
-  | packageFacet pkgName facetName =>
+    return Job.pure <| toFamily mod
+  | package pkgName =>
     let some pkg ← findPackage? pkgName
       | error s!"invalid target '{self}': package '{pkgName}' not found in workspace"
-    have : FamilyOut BuildData (pkg.facet facetName).key α :=
-      ⟨by simpa [self_eq] using h.family_key_eq_type⟩
-    fetch <| pkg.facet facetName
-  | targetFacet pkgName targetName facetName =>
-    -- TODO: Support this
-    error s!"unsupported target {self}: fetching builtin targets by key is not currently supported"
-  | customTarget pkgName targetName =>
+    return Job.pure <| toFamily pkg.toPackage
+  | packageTarget pkgName target =>
     let some pkg ← findPackage? pkgName
       | error s!"invalid target '{self}': package '{pkgName}' not found in workspace"
-    have : FamilyOut BuildData (pkg.target targetName).key α :=
-      ⟨by simpa [self_eq] using h.family_key_eq_type⟩
-    fetch <| pkg.target targetName
+    fetch <| pkg.target target
+  | facet target facetName =>
+      let job ← target.fetchCore
+      let kind := job.kind
+      if h : kind.isAnonymous then
+        error s!"invalid target '{self}': targets of opaque data kinds do not support facets"
+      else
+        (job.cast h).bindM fun data => fetch (.facet target kind data facetName)
+
+@[inline] protected def BuildKey.fetch
+  (self : BuildKey) [FamilyOut BuildData self α] : FetchM (Job α)
+:= cast (by simp) self.fetchCore
 
 @[inline] protected def Target.fetch (self : Target α) : FetchM (Job α) := do
  have := self.data_def; self.key.fetch
diff --git a/src/lake/Lake/Build/Targets.lean b/src/lake/Lake/Build/Targets.lean
index 14b7e522a1..f690f477be 100644
--- a/src/lake/Lake/Build/Targets.lean
+++ b/src/lake/Lake/Build/Targets.lean
@@ -10,10 +10,11 @@ import Lake.Config.Monad
 Utilities for fetching package, library, module, and executable targets and facets.
 -/
 
-namespace Lake
 open Lean (Name)
 open System (FilePath)
 
+namespace Lake
+
 /-! ## Package Facets & Targets -/
 
 /-- Fetch the build job of the specified package target. -/
@@ -25,7 +26,7 @@ def Package.fetchTargetJob
 /-- Fetch the build result of a target. -/
 protected def TargetDecl.fetch
   (self : TargetDecl)
-  [FamilyOut CustomData (self.pkg, self.name) α]
+  [FamilyOut (CustomData self.pkg) self.name α]
 : FetchM (Job α) := do
   let some pkg ← findPackage? self.pkg
     | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
@@ -39,8 +40,8 @@ def TargetDecl.fetchJob (self : TargetDecl) : FetchM OpaqueJob :=  do
 
 /-- Fetch the build result of a package facet. -/
 @[inline] protected def PackageFacetDecl.fetch
-  (pkg : Package) (self : PackageFacetDecl) [FamilyOut PackageData self.name α]
-: FetchM (Job α) := fetch <| pkg.facet self.name
+  (pkg : Package) (self : PackageFacetDecl) [FamilyOut FacetOut self.name α]
+: FetchM (Job α) := fetch <| pkg.facetCore self.name
 
 /-- Fetch the build job of a package facet. -/
 @[deprecated "Deprecated without replacement." (since := "2025-03-17")]
@@ -58,8 +59,8 @@ def Package.fetchFacetJob
 
 /-- Fetch the build result of a module facet. -/
 @[inline] protected def ModuleFacetDecl.fetch
-  (mod : Module) (self : ModuleFacetDecl) [FamilyOut ModuleData self.name α]
-: FetchM (Job α) := fetch <| mod.facet self.name
+  (mod : Module) (self : ModuleFacetDecl) [FamilyOut FacetOut self.name α]
+: FetchM (Job α) := fetch <| mod.facetCore self.name
 
 /-- Fetch the build job of a module facet. -/
 @[deprecated "Deprecated without replacement." (since := "2025-03-17")]
@@ -83,8 +84,8 @@ def Module.fetchFacetJob (name : Name) (self : Module) : FetchM OpaqueJob :=
 
 /-- Fetch the build result of a library facet. -/
 @[inline] protected def LibraryFacetDecl.fetch
-  (lib : LeanLib) (self : LibraryFacetDecl) [FamilyOut LibraryData self.name α]
-: FetchM (Job α) := fetch <| lib.facet self.name
+  (lib : LeanLib) (self : LibraryFacetDecl) [FamilyOut FacetOut self.name α]
+: FetchM (Job α) := fetch <| lib.facetCore self.name
 
 /-- Fetch the build job of a library facet. -/
 @[deprecated "Deprecated without replacement," (since := "2025-03-17")]
diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean
index 732a0a5f42..7d7595f72e 100644
--- a/src/lake/Lake/CLI/Actions.lean
+++ b/src/lake/Lake/CLI/Actions.lean
@@ -6,6 +6,7 @@ Authors: Mac Malone
 prelude
 import Lake.Build.Run
 import Lake.Build.Targets
+import Lake.Build.Common
 import Lake.CLI.Build
 
 namespace Lake
diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean
index 84ae95263f..6f56e2c00f 100644
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@@ -24,11 +24,12 @@ structure BuildSpec where
 : BuildSpec where
   info
   buildable := true
-  format := h.family_key_eq_type ▸ formatQuery
+  format := h.fam_eq ▸ formatQuery
 
 @[inline] def mkConfigBuildSpec
   (info : BuildInfo)
-  (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+  (config : FacetConfig facet)
+  (h : BuildData info.key = FacetOut facet)
 : BuildSpec where
   info
   buildable := config.buildable
@@ -65,11 +66,37 @@ def resolveModuleTarget
   (ws : Workspace) (mod : Module) (facet : Name)
 : Except CliError BuildSpec :=
   if facet.isAnonymous then
-    return mkBuildSpec (mod.facet leanArtsFacet)
-  else if let some config := ws.findModuleFacetConfig? facet then do
-    return mkConfigBuildSpec (mod.facet facet) config rfl
+    return mkBuildSpec mod.leanArts
   else
-    throw <| CliError.unknownFacet "module" facet
+    let facet := Module.facetKind ++ facet
+    if let some config := ws.findModuleFacetConfig? facet then do
+      return mkConfigBuildSpec (mod.facetCore config.name) config.toFacetConfig rfl
+    else
+      throw <| CliError.unknownFacet "module" facet
+
+def resolveCustomTarget
+  (pkg : Package) (name facet : Name) (config : TargetConfig pkg.name name)
+: Except CliError BuildSpec :=
+  if !facet.isAnonymous then
+    throw <| CliError.invalidFacet name facet
+  else do
+    return {info := pkg.target name, format := config.format}
+
+def resolveConfigDeclTarget
+  (ws : Workspace) (pkg : Package)
+  {target : Name} (decl : NConfigDecl pkg.name target) (facet : Name)
+: Except CliError (Array BuildSpec) := do
+  if h : decl.kind.isAnonymous then
+    Array.singleton <$> resolveCustomTarget pkg target facet (decl.targetConfig h)
+  else
+    let facet := if facet.isAnonymous then `default else facet
+    if let some config := ws.findFacetConfig? (decl.kind ++ facet) then
+      let tgt := decl.mkConfigTarget pkg
+      let tgt := cast (by simp [decl.target_eq_type h]) tgt
+      let info := BuildInfo.facet (.packageTarget pkg.name decl.name) decl.kind tgt config.name
+      return #[mkConfigBuildSpec info config rfl]
+    else
+      throw <| CliError.unknownFacet decl.kind.toString facet
 
 def resolveLibTarget
   (ws : Workspace) (lib : LeanLib) (facet : Name := .anonymous)
@@ -77,11 +104,11 @@ def resolveLibTarget
   if facet.isAnonymous then
     lib.defaultFacets.mapM (resolveFacet ·)
   else
-    Array.singleton <$> resolveFacet facet
+    Array.singleton <$> resolveFacet (LeanLib.facetKind ++ facet)
 where
   resolveFacet facet :=
     if let some config := ws.findLibraryFacetConfig? facet then do
-      return mkConfigBuildSpec (lib.facet facet) config rfl
+      return mkConfigBuildSpec (lib.facetCore config.name) config.toFacetConfig rfl
     else
       throw <| CliError.unknownFacet "library" facet
 
@@ -103,26 +130,11 @@ def resolveExternLibTarget
   else
     throw <| CliError.unknownFacet "external library" facet
 
-set_option linter.unusedVariables false in
-def resolveCustomTarget
-  (pkg : Package) (name facet : Name) (config : TargetConfig pkg.name name)
-: Except CliError BuildSpec :=
-  if !facet.isAnonymous then
-    throw <| CliError.invalidFacet name facet
-  else do
-    return {info := pkg.target name, format := config.format}
-
 def resolveTargetInPackage
   (ws : Workspace) (pkg : Package) (target facet : Name)
-: Except CliError (Array BuildSpec) :=
-  if let some config := pkg.findTargetConfig? target then
-    Array.singleton <$> resolveCustomTarget pkg target facet config
-  else if let some exe := pkg.findLeanExe? target then
-    Array.singleton <$> resolveExeTarget exe facet
-  else if let some lib := pkg.findExternLib? target then
-    Array.singleton <$> resolveExternLibTarget lib facet
-  else if let some lib := pkg.findLeanLib? target then
-    resolveLibTarget ws lib facet
+: Except CliError (Array BuildSpec) := do
+  if let some decl := pkg.findTargetDecl? target then
+    resolveConfigDeclTarget ws pkg decl facet
   else if let some mod := pkg.findTargetModule? target then
     Array.singleton <$> resolveModuleTarget ws mod facet
   else
@@ -138,22 +150,18 @@ def resolvePackageTarget
 : Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
-  else if let some config := ws.findPackageFacetConfig? facet then do
-    return #[mkConfigBuildSpec (pkg.facet facet) config rfl]
   else
-    throw <| CliError.unknownFacet "package" facet
+    let facet := Package.facetKind ++ facet
+    if let some config := ws.findPackageFacetConfig? facet then do
+      return #[mkConfigBuildSpec (pkg.facetCore config.name) config.toFacetConfig rfl]
+    else
+      throw <| CliError.unknownFacet "package" facet
 
 def resolveTargetInWorkspace
   (ws : Workspace) (target : Name) (facet : Name)
 : Except CliError (Array BuildSpec) :=
-  if let some ⟨pkg, config⟩ := ws.findTargetConfig? target then
-    Array.singleton <$> resolveCustomTarget pkg target facet config
-  else if let some exe := ws.findLeanExe? target then
-    Array.singleton <$> resolveExeTarget exe facet
-  else if let some lib := ws.findExternLib? target then
-    Array.singleton <$> resolveExternLibTarget lib facet
-  else if let some lib := ws.findLeanLib? target then
-    resolveLibTarget ws lib facet
+  if let some ⟨pkg, decl⟩ := ws.findTargetDecl? target then
+    resolveConfigDeclTarget ws pkg decl facet
   else if let some pkg := ws.findPackage? target then
     resolvePackageTarget ws pkg facet
   else if let some mod := ws.findTargetModule? target then
diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 17116f5b0e..9abc2bd2c9 100644
--- a/src/lake/Lake/CLI/Translate/Lean.lean
+++ b/src/lake/Lake/CLI/Translate/Lean.lean
@@ -253,6 +253,6 @@ def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
   open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)
   $(pkgConfig.mkCommand):command
   $[$(pkg.depConfigs.map (·.mkRequire)):command]*
-  $[$(pkg.mkTargetCommands defaultTargets `lean_lib LeanLibConfig.mkCommand):command]*
-  $[$(pkg.mkTargetCommands defaultTargets `lean_exe LeanExeConfig.mkCommand):command]*
+  $[$(pkg.mkTargetCommands defaultTargets LeanLib.configKind LeanLibConfig.mkCommand):command]*
+  $[$(pkg.mkTargetCommands defaultTargets LeanExe.configKind LeanExeConfig.mkCommand):command]*
   )
diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean
index b149cdc7d8..ae2eba5993 100644
--- a/src/lake/Lake/CLI/Translate/Toml.lean
+++ b/src/lake/Lake/CLI/Translate/Toml.lean
@@ -20,6 +20,11 @@ open Lean System Toml
 private local instance : BEq FilePath where
   beq a b := a.normalize == b.normalize
 
+class EncodeField (σ : Type u) (name : Name) (α : Type u) where
+  encodeField : α → Value
+
+instance [ToToml α] : EncodeField σ name α := ⟨toToml⟩
+
 class InsertField (σ : Type u) (name : Name) where
   insertField : σ → Table → Table
 
@@ -30,8 +35,8 @@ abbrev Toml.Table.insertField
 instance [SmartInsert α] [field : ConfigField σ name α] : InsertField σ name where
   insertField cfg t := t.smartInsert name (field.get cfg)
 
-instance [ToToml α] [BEq α] [field : ConfigField σ name α] : InsertField σ name where
-  insertField cfg t := t.insertD name (field.get cfg) (field.mkDefault cfg)
+instance [enc : EncodeField σ name α] [BEq α] [field : ConfigField σ name α] : InsertField σ name where
+  insertField cfg t := t.insertD name (field.get cfg) (field.mkDefault cfg) (enc := ⟨enc.encodeField⟩)
 
 /-! ## Value Encoders -/
 
@@ -69,6 +74,11 @@ def smartInsertVerTags (pat : StrPat) (t : Table) : Table :=
 instance : InsertField (PackageConfig n) `versionTags where
   insertField cfg := smartInsertVerTags cfg.versionTags
 
+def encodeFacets (facets : Array Name) : Value :=
+  toToml <| facets.map (toToml <| Name.eraseHead ·)
+
+instance : EncodeField (LeanLibConfig n) `defaultFacets (Array Name) := ⟨encodeFacets⟩
+
 /-! ## Dependency Configuration Encoders -/
 
 protected def Dependency.toToml (dep : Dependency) (t : Table  := {}) : Table :=
@@ -127,11 +137,11 @@ local macro "gen_toml_encoders%" : command => do
 
 gen_toml_encoders%
 
-@[inline] def Toml.Table.insertTargets
+@[inline] def Package.mkTomlTargets
   (pkg : Package) (kind : Name)
-  (toToml : {n : Name} → ConfigType kind pkg.name n → Table) (t : Table)
-: Table :=
-  t.smartInsert kind <| pkg.targetDecls.filterMap (·.config? kind |>.map toToml)
+  (toToml : {n : Name} → ConfigType kind pkg.name n → Table)
+: Array Table :=
+  pkg.targetDecls.filterMap (·.config? kind |>.map toToml)
 
 /-! ## Root Encoder -/
 
@@ -142,5 +152,5 @@ def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
   cfg.toToml t
   |>.smartInsert `defaultTargets pkg.defaultTargets
   |>.smartInsert `require pkg.depConfigs
-  |>.insertTargets pkg `lean_lib LeanLibConfig.toToml
-  |>.insertTargets pkg `lean_exe LeanExeConfig.toToml
+  |>.smartInsert LeanLib.keyword (pkg.mkTomlTargets LeanLib.configKind LeanLibConfig.toToml)
+  |>.smartInsert LeanExe.keyword (pkg.mkTomlTargets LeanExe.configKind LeanExeConfig.toToml)
diff --git a/src/lake/Lake/Config/ConfigDecl.lean b/src/lake/Lake/Config/ConfigDecl.lean
index e005939a76..5aad70c170 100644
--- a/src/lake/Lake/Config/ConfigDecl.lean
+++ b/src/lake/Lake/Config/ConfigDecl.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2022 Mac Malone. All rights reserved.
+Copyright (c) 2025 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
@@ -13,78 +13,121 @@ open Lean (Name)
 
 namespace Lake
 
+/-- The keyword for Lean library configurations. -/
+abbrev LeanLib.keyword : Name := `lean_lib
+
+/-- The type kind for Lean library configurations. -/
+@[match_pattern] abbrev LeanLib.configKind := facetKind
+
+/-- The keyword for Lean executable configurations. -/
+abbrev LeanExe.keyword : Name := `lean_exe
+
+/-- The type kind for Lean executable configurations. -/
+@[match_pattern] abbrev LeanExe.configKind := facetKind
+
+/-- The keyword for external library configurations. -/
+abbrev ExternLib.keyword : Name := `extern_lib
+
+/-- The type kind for external library configurations. -/
+@[match_pattern] abbrev ExternLib.configKind := facetKind
+
 abbrev ConfigType (kind : Name) (pkgName name : Name) : Type :=
   match kind with
-  | `lean_lib => LeanLibConfig name
-  | `lean_exe => LeanExeConfig name
-  | `extern_lib => ExternLibConfig pkgName name
+  | LeanLib.configKind => LeanLibConfig name
+  | LeanExe.configKind => LeanExeConfig name
+  | ExternLib.configKind => ExternLibConfig pkgName name
   | .anonymous => OpaqueTargetConfig pkgName name
   | _ => Empty
 
+/-- Forward declared `ConfigTarget` to work around recursion issues (e.g., with `Package`). -/
+opaque OpaqueConfigTarget (kind : Name) : Type
+
 structure ConfigDecl where
   pkg : Name
   name : Name
   kind : Name
   config : ConfigType kind pkg name
+  wf_data : ¬ kind.isAnonymous → CustomData pkg name = DataType kind ∧ DataType kind = OpaqueConfigTarget kind
   deriving TypeName
 
 structure PConfigDecl (p : Name) extends ConfigDecl where
-  pkg_eq : toConfigDecl.pkg = p
+  pkg_eq : toConfigDecl.pkg = p := by rfl
 
 structure NConfigDecl (p n : Name) extends PConfigDecl p where
-  name_eq : toConfigDecl.name = n
+  name_eq : toConfigDecl.name = n := by rfl
 
 structure KConfigDecl (k : Name) extends ConfigDecl where
-  kind_eq : toConfigDecl.kind = k
+  kind_eq : toConfigDecl.kind = k := by rfl
+
+instance : Nonempty (NConfigDecl pkg name) :=
+  ⟨{pkg, name, kind := .anonymous, config := Classical.ofNonempty, wf_data := by simp [Name.isAnonymous]}⟩
+
+@[inline] def PConfigDecl.config' (self : PConfigDecl p) : ConfigType self.kind p self.name :=
+  cast (by rw [self.pkg_eq]) self.config
+
+@[inline] def NConfigDecl.config' (self : NConfigDecl p n) : ConfigType self.kind p n :=
+  cast (by rw [self.name_eq]) self.toPConfigDecl.config'
+
+theorem NConfigDecl.target_eq_type (self : NConfigDecl p n)
+  (h : ¬ self.kind.isAnonymous) : DataType self.kind = OpaqueConfigTarget self.kind
+:= self.wf_data h |>.2
+
+theorem NConfigDecl.data_eq_target (self : NConfigDecl p n)
+  (h : ¬ self.kind.isAnonymous) : CustomData p n = OpaqueConfigTarget self.kind
+:= by simpa [self.pkg_eq, self.name_eq, self.target_eq_type h] using (self.wf_data h).1
 
 @[inline] def ConfigDecl.config? (kind : Name) (self : ConfigDecl) : Option (ConfigType kind self.pkg self.name) :=
   if h : self.kind = kind then
-    some <| cast (by simp [h]) self.config
+    some <| cast (by rw [h]) self.config
   else
     none
 
 @[inline] def PConfigDecl.config? (kind : Name) (self : PConfigDecl p) : Option (ConfigType kind p self.name) :=
-  cast (by simp [self.pkg_eq]) (self.toConfigDecl.config? kind)
+  cast (by rw [self.pkg_eq]) (self.toConfigDecl.config? kind)
 
 @[inline] def NConfigDecl.config? (kind : Name) (self : NConfigDecl p n) : Option (ConfigType kind p n) :=
-  cast (by simp [self.name_eq]) (self.toPConfigDecl.config? kind)
+  cast (by rw [self.name_eq]) (self.toPConfigDecl.config? kind)
 
 @[inline] def ConfigDecl.leanLibConfig? (self : ConfigDecl) : Option (LeanLibConfig self.name) :=
-  self.config? `lean_lib
+  self.config? LeanLib.configKind
 
 @[inline] def NConfigDecl.leanLibConfig? (self : NConfigDecl p n) : Option (LeanLibConfig n) :=
-  self.config? `lean_lib
+  self.config? LeanLib.configKind
 
 /-- A  Lean library declaration from a configuration written in Lean. -/
-abbrev LeanLibDecl := KConfigDecl `lean_lib
+abbrev LeanLibDecl := KConfigDecl LeanLib.configKind
 
 @[inline] def ConfigDecl.leanExeConfig? (self : ConfigDecl) : Option (LeanExeConfig self.name) :=
-  self.config? `lean_exe
+  self.config? LeanExe.configKind
 
 @[inline] def NConfigDecl.leanExeConfig? (self : NConfigDecl p n) : Option (LeanExeConfig n) :=
-  self.config? `lean_exe
+  self.config? LeanExe.configKind
 
 /-- A Lean executable declaration from a configuration written in Lean. -/
-abbrev LeanExeDecl := KConfigDecl `lean_exe
+abbrev LeanExeDecl := KConfigDecl LeanExe.configKind
 
 @[inline] def PConfigDecl.externLibConfig? (self : PConfigDecl p) : Option (ExternLibConfig p self.name) :=
-  self.config? `extern_lib
+  self.config? ExternLib.configKind
 
 @[inline] def NConfigDecl.externLibConfig? (self : NConfigDecl p n) : Option (ExternLibConfig p n) :=
-  self.config? `extern_lib
+  self.config? ExternLib.configKind
 
 /-- An external library declaration from a configuration written in Lean. -/
-abbrev ExternLibDecl := KConfigDecl `extern_lib
+abbrev ExternLibDecl := KConfigDecl ExternLib.configKind
+
+@[inline] def PConfigDecl.opaqueTargetConfig (self : PConfigDecl p) (h : self.kind.isAnonymous) : OpaqueTargetConfig p self.name :=
+  cast (by rw [self.pkg_eq, Name.eq_anonymous_of_isAnonymous h, ConfigType]) self.config
+
+@[inline] def NConfigDecl.opaqueTargetConfig (self : NConfigDecl p n) (h : self.kind.isAnonymous) : OpaqueTargetConfig p n :=
+  cast (by rw [self.name_eq]) (self.toPConfigDecl.opaqueTargetConfig h)
 
 @[inline] def PConfigDecl.opaqueTargetConfig? (self : PConfigDecl p) : Option (OpaqueTargetConfig p self.name) :=
   if h : self.kind.isAnonymous then
-    have h : self.kind = .anonymous := by
-      revert h; cases self.kind <;> simp [Name.isAnonymous]
-    some <| cast (by simp [self.pkg_eq, h, ConfigType]) self.config
+    some <| self.opaqueTargetConfig h
   else
     none
 
 @[inline] def NConfigDecl.opaqueTargetConfig? (self : NConfigDecl p n) : Option (OpaqueTargetConfig p n) :=
-  cast (by simp [self.name_eq]) self.toPConfigDecl.opaqueTargetConfig?
+  cast (by rw [self.name_eq]) self.toPConfigDecl.opaqueTargetConfig?
 
 deriving instance TypeName for LeanLibDecl, LeanExeDecl
diff --git a/src/lake/Lake/Config/ConfigTarget.lean b/src/lake/Lake/Config/ConfigTarget.lean
new file mode 100644
index 0000000000..7e7af93d14
--- /dev/null
+++ b/src/lake/Lake/Config/ConfigTarget.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Config.Package
+
+open Lean
+
+namespace Lake
+
+/--
+A user-configured target -- its package and its configuration.
+This is the general structure from which `LeanLib`, `LeanExe`, etc. are derived.
+-/
+structure ConfigTarget (kind : Name) where
+  /-- The package the target belongs to. -/
+  pkg : Package
+  /-- The target's name. -/
+  name : Name
+  /-- The target's user-defined configuration. -/
+  config : ConfigType kind pkg.name name
+
+@[simp] axiom OpaqueConfigTarget.def {k : Name} : OpaqueConfigTarget k = ConfigTarget k
+
+@[inline] def PConfigDecl.mkConfigTarget (pkg : Package) (self : PConfigDecl pkg.name) : ConfigTarget self.kind :=
+  ConfigTarget.mk pkg self.name self.config'
+
+/-- Returns the package targets of the specified kind (as an `Array`). -/
+@[inline] def Package.configTargets (kind : Name) (self : Package) : Array (ConfigTarget kind) :=
+  self.targetDecls.foldl (init := #[]) fun a t =>
+    let {name, kind := k, config, pkg_eq, ..} := t
+    if kind_eq : k = kind then
+      a.push ⟨self, name, kind_eq ▸ pkg_eq ▸ config⟩
+    else
+      a
+
+/-- Try to find a package target of the given name and kind. -/
+@[inline] def Package.findConfigTarget? (kind : Name) (name : Name) (self : Package) : Option (ConfigTarget kind) :=
+  self.findTargetDecl? name |>.bind fun t =>
+    let {name, kind := k, config, pkg_eq, ..} := t
+    if kind_eq : k = kind then
+      some ⟨self, name, kind_eq ▸ pkg_eq ▸ config⟩
+    else
+      none
diff --git a/src/lake/Lake/Config/ExternLib.lean b/src/lake/Lake/Config/ExternLib.lean
index 5355eeb4a3..58db6e8592 100644
--- a/src/lake/Lake/Config/ExternLib.lean
+++ b/src/lake/Lake/Config/ExternLib.lean
@@ -4,32 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Config.Package
+import Lake.Config.ConfigTarget
 
 namespace Lake
 open Lean (Name)
 
 /-- An external library -- its package plus its configuration. -/
-structure ExternLib where
-  /-- The package the library belongs to. -/
-  pkg : Package
-  /-- The external library's name. -/
-  name : Name
-  /-- The library's user-defined configuration. -/
-  config : ExternLibConfig pkg.name name
+abbrev ExternLib := ConfigTarget ExternLib.configKind
 
 /-- The external libraries of the package (as an Array). -/
 @[inline] def Package.externLibs (self : Package) : Array ExternLib :=
-  self.targetDecls.foldl (init := #[]) fun a t =>
-    if let some cfg := t.externLibConfig? then a.push ⟨self, t.name, cfg⟩ else a
+  self.configTargets ExternLib.configKind
 
 /-- Try to find a external library in the package with the given name. -/
 @[inline] def Package.findExternLib? (name : Name) (self : Package) : Option ExternLib :=
-  self.targetDeclMap.find? name |>.bind fun t => t.externLibConfig?.map fun cfg =>
-    ⟨self, name, cfg⟩
+  self.findConfigTarget? ExternLib.configKind name
 
 namespace ExternLib
 
+/-- The library's user-defined configuration. -/
+@[inline] nonrec def config (self : ExternLib) : ExternLibConfig self.pkg.name self.name :=
+  self.config
+
 /--
 The arguments to pass to `leanc` when linking the external library.
 That is, the package's `moreLinkArgs`.
diff --git a/src/lake/Lake/Config/ExternLibConfig.lean b/src/lake/Lake/Config/ExternLibConfig.lean
index eb41317785..884f872602 100644
--- a/src/lake/Lake/Config/ExternLibConfig.lean
+++ b/src/lake/Lake/Config/ExternLibConfig.lean
@@ -13,5 +13,5 @@ open Lean System
 /-- A external library's declarative configuration. -/
 structure ExternLibConfig (pkgName name : Name) where
   /-- The library's build data. -/
-  getPath : Job (CustomData (pkgName, .str name "static")) → Job FilePath
+  getPath : Job (CustomData pkgName (.str name "static")) → Job FilePath
   deriving Inhabited
diff --git a/src/lake/Lake/Config/FacetConfig.lean b/src/lake/Lake/Config/FacetConfig.lean
index c11fbd3812..b4349127f2 100644
--- a/src/lake/Lake/Config/FacetConfig.lean
+++ b/src/lake/Lake/Config/FacetConfig.lean
@@ -11,25 +11,51 @@ namespace Lake
 open Lean (Name)
 
 /-- A facet's declarative configuration. -/
-structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where
+structure FacetConfig (name : Name) : Type where
+  /-- The facet kind (i.e., the kind of targets that support this facet). -/
+  kind : Name
   /-- The facet's fetch function. -/
-  fetchFn : ι → FetchM (Job (DataFam name))
+  fetchFn : DataType kind → FetchM (Job (FacetOut name))
   /-- Is this facet compatible with the `lake build` CLI? -/
   buildable : Bool := true
   /-- Format this facet's output (e.g., for `lake query`). -/
-  format : OutFormat → DataFam name → String
+  format : OutFormat → FacetOut name → String
   deriving Inhabited
 
-protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
+protected abbrev FacetConfig.name (_ : FacetConfig name) := name
+
+structure KFacetConfig (k : Name) (name : Name) extends FacetConfig name where
+  kind := k
+  kind_eq : toFacetConfig.kind = k := by rfl
+
+abbrev FacetConfig.toKind
+  {kind : Name} (self : FacetConfig name) (h : self.kind = kind)
+: KFacetConfig kind name := KFacetConfig.mk self h
+
+def FacetConfig.toKind? (kind : Name) (self : FacetConfig name) : Option (KFacetConfig kind name) :=
+  if h : self.kind = kind then
+    some (self.toKind h)
+  else
+    none
+
+/-- Run the facet configuration's fetch function. -/
+@[inline] def KFacetConfig.run
+  [FamilyOut DataType kind α]
+  [FamilyOut FacetOut facet β]
+  (self : KFacetConfig kind facet) (info : α)
+: FetchM (Job β) :=
+  cast (by simp) <| self.fetchFn <| cast (by simp [self.kind_eq]) info
 
 /-- A smart constructor for facet configurations that generate jobs for the CLI. -/
 @[inline] def mkFacetJobConfig
-  [FormatQuery α] [h : FamilyOut Fam facet α]
-  (build : ι → FetchM (Job α)) (buildable := true)
-: FacetConfig Fam ι facet where
+  [FormatQuery β]
+  [i : FamilyOut DataType kind α]
+  [o : FamilyOut FacetOut facet β]
+  (build : α → FetchM (Job β)) (buildable := true)
+: KFacetConfig kind facet where
   buildable
-  fetchFn := h.family_key_eq_type ▸ build
-  format := h.family_key_eq_type ▸ formatQuery
+  fetchFn := i.fam_eq ▸ o.fam_eq ▸ build
+  format := o.fam_eq ▸ formatQuery
 
 /-- A dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where
@@ -37,22 +63,31 @@ structure NamedConfigDecl (β : Name → Type u) where
   config : β name
 
 /-- A module facet's declarative configuration. -/
-abbrev ModuleFacetConfig := FacetConfig ModuleData Module
+abbrev ModuleFacetConfig := KFacetConfig Module.facetKind
 
 /-- A module facet declaration from a configuration file. -/
 abbrev ModuleFacetDecl := NamedConfigDecl ModuleFacetConfig
 
 /-- A package facet's declarative configuration. -/
-abbrev PackageFacetConfig := FacetConfig PackageData Package
+abbrev PackageFacetConfig := KFacetConfig Package.facetKind
 
 /-- A package facet declaration from a configuration file. -/
 abbrev PackageFacetDecl := NamedConfigDecl PackageFacetConfig
 
 /-- A library facet's declarative configuration. -/
-abbrev LibraryFacetConfig := FacetConfig LibraryData LeanLib
+abbrev LibraryFacetConfig := KFacetConfig LeanLib.facetKind
 
 /-- A library facet declaration from a configuration file. -/
 abbrev LibraryFacetDecl := NamedConfigDecl LibraryFacetConfig
 
 deriving instance TypeName for
   ModuleFacetDecl, PackageFacetDecl, LibraryFacetDecl
+
+/-- A library facet's declarative configuration. -/
+abbrev LeanLibFacetConfig := LibraryFacetConfig
+
+/-- A Lean executable facet's declarative configuration. -/
+abbrev LeanExeFacetConfig := KFacetConfig LeanExe.facetKind
+
+/-- An external library facet's declarative configuration. -/
+abbrev ExternLibFacetConfig := KFacetConfig ExternLib.facetKind
diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean
index 3bcad0b588..eece5a2e3b 100644
--- a/src/lake/Lake/Config/LeanExe.lean
+++ b/src/lake/Lake/Config/LeanExe.lean
@@ -10,23 +10,15 @@ namespace Lake
 open Lean System
 
 /-- A Lean executable -- its package plus its configuration. -/
-structure LeanExe where
-  /-- The package the executable belongs to. -/
-  pkg : Package
-  /-- The executable's name. -/
-  name : Name
-  /-- The executable's user-defined configuration. -/
-  config : LeanExeConfig name
+abbrev LeanExe := ConfigTarget LeanExe.configKind
 
 /-- The Lean executables of the package (as an Array). -/
 @[inline] def Package.leanExes (self : Package) : Array LeanExe :=
-  self.targetDecls.foldl (init := #[]) fun a t =>
-    if let some cfg := t.leanExeConfig? then a.push ⟨self, t.name, cfg⟩ else a
+  self.configTargets LeanExe.configKind
 
 /-- Try to find a Lean executable in the package with the given name. -/
 @[inline] def Package.findLeanExe? (name : Name) (self : Package) : Option LeanExe :=
-  self.targetDeclMap.find? name |>.bind fun t => t.leanExeConfig?.map fun cfg =>
-    ⟨self, name, cfg⟩
+  self.findConfigTarget? LeanExe.configKind name
 
 /--
 Converts the executable configuration into a library
@@ -42,6 +34,10 @@ def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig n) : LeanLibConfig n whe
 
 namespace LeanExe
 
+/-- The executable's user-defined configuration. -/
+@[inline] nonrec def config (self : LeanExe) : LeanExeConfig self.name :=
+  self.config
+
 /-- Converts the executable into a library with a single module (the root). -/
 @[inline] def toLeanLib (self : LeanExe) : LeanLib :=
   ⟨self.pkg, self.name, self.config.toLeanLibConfig⟩
diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean
index 0794329c84..817e9d7934 100644
--- a/src/lake/Lake/Config/LeanLib.lean
+++ b/src/lake/Lake/Config/LeanLib.lean
@@ -4,32 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Config.Package
+import Lake.Config.ConfigTarget
 
 namespace Lake
 open Lean System
 
 /-- A Lean library -- its package plus its configuration. -/
-structure LeanLib where
-  /-- The package the library belongs to. -/
-  pkg : Package
-  /-- The library's name. -/
-  name : Name
-   /-- The library's user-defined configuration. -/
-  config : LeanLibConfig name
+abbrev LeanLib := ConfigTarget LeanLib.configKind
 
 /-- The Lean libraries of the package (as an Array). -/
 @[inline] def Package.leanLibs (self : Package) : Array LeanLib :=
-  self.targetDecls.foldl (init := #[]) fun a t =>
-    if let some cfg := t.leanLibConfig? then a.push ⟨self, t.name, cfg⟩ else a
+  self.configTargets LeanLib.configKind
 
 /-- Try to find a Lean library in the package with the given name. -/
 @[inline] def Package.findLeanLib? (name : Name) (self : Package) : Option LeanLib :=
-  self.targetDeclMap.find? name |>.bind fun t => t.leanLibConfig?.map fun cfg =>
-    ⟨self, name, cfg⟩
+  self.findConfigTarget? LeanLib.configKind name
 
 namespace LeanLib
 
+/-- The library's user-defined configuration. -/
+@[inline] nonrec def config (self : LeanLib) : LeanLibConfig self.name :=
+  self.config
+
 /-- The package's `srcDir` joined with the library's `srcDir`. -/
 @[inline] def srcDir (self : LeanLib) : FilePath :=
   self.pkg.srcDir / self.config.srcDir
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 3dbc1a344e..45e72e1d4a 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -636,6 +636,10 @@ namespace Package
 @[inline] def irDir (self : Package) : FilePath :=
   self.buildDir / self.config.irDir
 
+/-- Try to find a target configuration in the package with the given name. -/
+def findTargetDecl? (name : Name) (self : Package) : Option (NConfigDecl self.name name) :=
+  self.targetDeclMap.find? name
+
 /-- Whether the given module is considered local to the package. -/
 def isLocalModule (mod : Name) (self : Package) : Bool :=
   self.targetDecls.any (·.leanLibConfig?.any (·.isLocalModule mod))
diff --git a/src/lake/Lake/Config/TargetConfig.lean b/src/lake/Lake/Config/TargetConfig.lean
index 514a49f9a2..681be75dbb 100644
--- a/src/lake/Lake/Config/TargetConfig.lean
+++ b/src/lake/Lake/Config/TargetConfig.lean
@@ -14,21 +14,24 @@ namespace Lake
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's fetch function. -/
-  fetchFn : (pkg : NPackage pkgName) → FetchM (Job (CustomData (pkgName, name)))
+  fetchFn : (pkg : NPackage pkgName) → FetchM (Job (CustomData pkgName name))
   /-- Format the target's output (e.g., for `lake query`). -/
-  format : OutFormat → CustomData (pkgName, name) → String
+  format : OutFormat → CustomData pkgName name → String
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-  [FormatQuery α] [h : FamilyOut CustomData (pkgName, name) α]
+  [FormatQuery α] [h : FamilyOut (CustomData pkgName) name α]
   (fetch : (pkg : NPackage pkgName) → FetchM (Job α))
 : TargetConfig pkgName name where
-  fetchFn := h.family_key_eq_type ▸ fetch
-  format := h.family_key_eq_type ▸ formatQuery
+  fetchFn := h.fam_eq ▸ fetch
+  format := h.fam_eq ▸ formatQuery
 
 hydrate_opaque_type OpaqueTargetConfig TargetConfig pkgName name
 
+@[inline] def NConfigDecl.targetConfig (self : NConfigDecl p n) (h : self.kind.isAnonymous) : TargetConfig p n :=
+  self.opaqueTargetConfig h |>.get
+
 @[inline] def NConfigDecl.targetConfig? (self : NConfigDecl p n) : Option (TargetConfig p n) :=
   self.opaqueTargetConfig?.map (·.get)
 
diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean
index 4d6dea3331..f8421a4a39 100644
--- a/src/lake/Lake/Config/Workspace.lean
+++ b/src/lake/Lake/Config/Workspace.lean
@@ -31,12 +31,8 @@ structure Workspace : Type where
   packages : Array Package := {}
   /-- Name-package map of packages within the workspace. -/
   packageMap : DNameMap NPackage := {}
-  /-- Name-configuration map of module facets defined in the workspace. -/
-  moduleFacetConfigs : DNameMap ModuleFacetConfig
-  /-- Name-configuration map of package facets defined in the workspace. -/
-  packageFacetConfigs : DNameMap PackageFacetConfig
-  /-- Name-configuration map of library facets defined in the workspace. -/
-  libraryFacetConfigs : DNameMap LibraryFacetConfig
+  /-- Configuration map of facets defined in the workspace. -/
+  facetConfigs : DNameMap FacetConfig := {}
 
 instance : Nonempty Workspace :=
   have : Inhabited Package := Classical.inhabited_of_nonempty inferInstance
@@ -122,29 +118,41 @@ protected def findExternLib? (name : Name) (self : Workspace) : Option ExternLib
 def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) :=
   self.packages.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
 
+/-- Try to find a target declaration in the workspace with the given name.  -/
+def findTargetDecl? (name : Name) (self : Workspace) : Option ((pkg : Package) × NConfigDecl pkg.name name) :=
+  self.packages.findSome? fun pkg => pkg.findTargetDecl? name <&> (⟨pkg, ·⟩)
+
+/-- Add a facet to the workspace. -/
+def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
+  {self with facetConfigs := self.facetConfigs.insert name cfg}
+
+/-- Try to find a facet configuration in the workspace with the given name. -/
+def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
+  self.facetConfigs.find? name
+
 /-- Add a module facet to the workspace. -/
 def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
-  {self with moduleFacetConfigs := self.moduleFacetConfigs.insert name cfg}
+  self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
 def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
-  self.moduleFacetConfigs.find? name
+  self.findFacetConfig? name |>.bind (·.toKind? Module.facetKind)
 
 /-- Add a package facet to the workspace. -/
 def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
-  {self with packageFacetConfigs := self.packageFacetConfigs.insert name cfg}
+  self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
 def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
-  self.packageFacetConfigs.find? name
+  self.findFacetConfig? name |>.bind (·.toKind? Package.facetKind)
 
 /-- Add a library facet to the workspace. -/
 def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
-  {self with libraryFacetConfigs := self.libraryFacetConfigs.insert cfg.name cfg}
+  self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a library facet configuration in the workspace with the given name. -/
 def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
-  self.libraryFacetConfigs.find? name
+  self.findFacetConfig? name |>.bind (·.toKind? LeanLib.facetKind)
 
 /-- The workspace's binary directories (which are added to `Path`). -/
 def binPath (self : Workspace) : SearchPath :=
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index 7ba28917d9..58fbdb11f5 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -5,7 +5,9 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.DSL.DeclUtil
-import Lake.Build.Index
+import Lake.Config.FacetConfig
+import Lake.Config.TargetConfig
+import Lake.Build.Job
 
 /-! # DSL for Targets & Facets
 Macros for declaring Lake targets and facets.
@@ -25,9 +27,9 @@ syntax buildDeclSig :=
 
 abbrev mkModuleFacetDecl
   (α) (facet : Name)
-  [FormatQuery α] [FamilyDef ModuleData facet α]
+  [OptDataKind α] [FormatQuery α] [FamilyDef ModuleData facet α]
   (f : Module → FetchM (Job α))
-: ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do
+: ModuleFacetDecl := .mk (Module.facetKind ++ facet) <| mkFacetJobConfig fun mod => do
   withRegisterJob (mod.facet facet |>.key.toSimpleString)
     (f mod)
 
@@ -64,9 +66,9 @@ def expandModuleFacetDecl : Macro := fun stx => do
 
 abbrev mkPackageFacetDecl
   (α) (facet : Name)
-  [FormatQuery α] [FamilyDef PackageData facet α]
+  [OptDataKind α] [FormatQuery α] [FamilyDef PackageData facet α]
   (f : Package → FetchM (Job α))
-: PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do
+: PackageFacetDecl := .mk (Package.facetKind ++ facet) <| mkFacetJobConfig fun pkg => do
   withRegisterJob (pkg.facet facet |>.key.toSimpleString)
     (f pkg)
 
@@ -103,9 +105,9 @@ def expandPackageFacetDecl : Macro := fun stx => do
 
 abbrev mkLibraryFacetDecl
   (α) (facet : Name)
-  [FormatQuery α] [FamilyDef LibraryData facet α]
+  [OptDataKind α] [FormatQuery α] [FamilyDef LibraryData facet α]
   (f : LeanLib → FetchM (Job α))
-: LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do
+: LibraryFacetDecl := .mk (LeanLib.facetKind ++ facet) <| mkFacetJobConfig fun lib => do
   withRegisterJob (lib.facet facet |>.key.toSimpleString)
     (f lib)
 
@@ -147,13 +149,13 @@ def expandLibraryFacetDecl : Macro := fun stx => do
 
 abbrev mkTargetDecl
   (α) (pkgName target : Name)
-  [FormatQuery α] [FamilyDef CustomData (pkgName, target) α]
+  [OptDataKind α] [FormatQuery α] [FamilyDef (CustomData pkgName) target α]
   (f : NPackage pkgName → FetchM (Job α))
 : TargetDecl :=
   let cfg := mkTargetJobConfig fun pkg => do
     withRegisterJob (pkg.target target |>.key.toSimpleString)
       (f pkg)
-  .mk (.mk pkgName target .anonymous (.mk cfg)) rfl
+  .mk (.mk pkgName target .anonymous (.mk cfg) (by simp [Name.isAnonymous])) rfl
 
 /--
 Define a new custom target for the package. Has one form:
@@ -180,9 +182,9 @@ def expandTargetCommand : Macro := fun stx => do
   let attr ← `(Term.attrInstance| «target»)
   let attrs := #[attr] ++ expandAttrs attrs?
   let name := Name.quoteFrom id id.getId
-  let pkgName := mkIdentFrom id `_package.name
+  let pkgName := mkIdentFrom id (packageDeclName.str "name")
   let pkg ← expandOptSimpleBinder pkg?
-  `(family_def $id : CustomData ($pkgName, $name) := $ty
+  `(family_def $id : CustomOut ($pkgName, $name) := $ty
     $[$doc?]? abbrev $id :=
       Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
     $[$wds?:whereDecls]?
@@ -192,8 +194,16 @@ def expandTargetCommand : Macro := fun stx => do
 /-! ## Lean Library & Executable Target Declarations -/
 --------------------------------------------------------------------------------
 
-def mkConfigDecl
-  (tyName kind : Name)
+abbrev mkConfigDecl
+  (pkg name kind : Name)
+  (config : ConfigType kind pkg name)
+  [FamilyDef (CustomData pkg) name (ConfigTarget kind)]
+  [FamilyDef DataType kind (ConfigTarget kind)]
+: KConfigDecl kind :=
+  {pkg, name, kind, config, wf_data := fun _ => by simp, kind_eq := rfl}
+
+def mkConfigDeclDef
+  (tyName attr kind : Name)
   [ConfigInfo tyName] [delTyName : TypeName (KConfigDecl kind)]
   (doc? : Option DocComment) (attrs? : Option Attributes)
   (nameStx? : Option IdentOrStr) (cfg : OptConfig)
@@ -203,18 +213,16 @@ def mkConfigDecl
   let name := Name.quoteFrom id id.getId
   let ty := Syntax.mkCApp tyName #[name]
   elabConfig tyName configId ty cfg
-  let kindId ← mkIdentFromRef kind
+  let attrId ← mkIdentFromRef attr
   let targetAttr ← `(Term.attrInstance| «target»)
-  let kindAttr ← `(Term.attrInstance| $kindId:ident)
+  let kindAttr ← `(Term.attrInstance| $attrId:ident)
   let attrs := #[targetAttr, kindAttr] ++ expandAttrs attrs?
   let pkg ← mkIdentFromRef (packageDeclName.str "name")
   let declTy ← mkIdentFromRef delTyName.typeName
   let kind := Name.quoteFrom (← getRef) kind
-  `(
-    $[$doc?]? abbrev $id : $declTy := {
-        pkg := $pkg, name := $name, config := $configId
-        kind := $kind, kind_eq := rfl
-    }
+  `(family_def $id : CustomOut ($pkg, $name) := ConfigTarget $kind
+    $[$doc?]? abbrev $id : $declTy :=
+      Lake.DSL.mkConfigDecl $pkg $name $kind $configId
     @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl
   )
 
@@ -237,7 +245,7 @@ def elabLeanLibCommand : CommandElab := fun stx => do
   let `(leanLibCommand|$(doc?)? $(attrs?)? lean_lib%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed lean_lib declaration"
   withRef kw do
-  let cmd ← mkConfigDecl ``LeanLibConfig `lean_lib doc? attrs? nameStx? cfg
+  let cmd ← mkConfigDeclDef ``LeanLibConfig LeanLib.keyword LeanLib.configKind doc? attrs? nameStx? cfg
   withMacroExpansion stx cmd <| elabCommand cmd
 
 @[inherit_doc leanLibCommand] abbrev LeanLibCommand := TSyntax ``leanLibCommand
@@ -264,7 +272,7 @@ def elabLeanExeCommand : CommandElab := fun stx => do
   let `(leanExeCommand|$(doc?)? $(attrs?)? lean_exe%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed lean_exe declaration"
   withRef kw do
-  let cmd ← mkConfigDecl ``LeanExeConfig `lean_exe doc? attrs? nameStx? cfg
+  let cmd ← mkConfigDeclDef ``LeanExeConfig LeanExe.keyword LeanExe.configKind doc? attrs? nameStx? cfg
   withMacroExpansion stx cmd <| elabCommand cmd
 
 @[inherit_doc leanExeCommand] abbrev LeanExeCommand := TSyntax ``leanExeCommand
@@ -278,9 +286,10 @@ instance : Coe LeanExeCommand Command where
 
 abbrev mkExternLibDecl
   (pkgName name : Name)
-  [FamilyDef CustomData (pkgName, .str name "static")  FilePath]
+  [FamilyDef (CustomData pkgName) (.str name "static") FilePath]
+  [FamilyDef (CustomData pkgName) name (ConfigTarget ExternLib.configKind)]
 : ExternLibDecl :=
-  .mk (.mk pkgName name `extern_lib {getPath := cast (by simp)}) rfl
+  mkConfigDecl pkgName name ExternLib.configKind {getPath := cast (by simp)}
 
 syntax externLibDeclSpec :=
   identOrStr (ppSpace simpleBinder)? declValSimple
@@ -316,7 +325,9 @@ def expandExternLibCommand : Macro := fun stx => do
   let pkgName := mkIdentFrom kw (packageDeclName.str "name")
   let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
   let name := Name.quoteFrom id id.getId
+  let kind := Name.quoteFrom kw ExternLib.configKind
   `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
+    family_def $id : CustomOut ($pkgName, $name) := ConfigTarget $kind
     $[$doc?:docComment]? def $id : ExternLibDecl :=
       Lake.DSL.mkExternLibDecl $pkgName $name
     @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl)
diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean
index 9f8a4474da..c1a565c76b 100644
--- a/src/lake/Lake/Load/Toml.lean
+++ b/src/lake/Lake/Load/Toml.lean
@@ -219,6 +219,12 @@ instance : DecodeField (PackageConfig n) `versionTags where
 -- for `platformIndependent`, `releaseRepo`, `buildArchive`, etc.
 instance [DecodeToml α] : DecodeToml (Option α) := ⟨(some <$> decodeToml ·)⟩
 
+def decodeFacets (kind : Name) (val : Value) : EDecodeM (Array Name) := do
+  return (← val.decodeArray).map (kind ++ ·)
+
+instance : DecodeField (LeanLibConfig n) `defaultFacets where
+  decodeField := decodeFieldCore `defaultFacets (decodeFacets LeanLib.facetKind)
+
 /-! ## Dependency Configuration Decoders -/
 
 protected def DependencySrc.decodeToml (t : Table) (ref := Syntax.missing) : EDecodeM DependencySrc := do
@@ -303,15 +309,15 @@ local macro "gen_toml_decoders%" : command => do
 gen_toml_decoders%
 
 def decodeTargetDecls
-  (p : Name) (t : Table)
-: DecodeM (Array (PConfigDecl p) × DNameMap (NConfigDecl p)) := do
+  (pkg : Name) (t : Table)
+: DecodeM (Array (PConfigDecl pkg) × DNameMap (NConfigDecl pkg)) := do
   let r := (#[], {})
-  let r ← go r `lean_lib LeanLibConfig.decodeToml
-  let r ← go r `lean_exe LeanExeConfig.decodeToml
+  let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
+  let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
   return r
 where
-  go r k (decode : {n : Name} → Table → DecodeM (ConfigType k p n)) := do
-    let some tableArrayVal := t.find? k | return r
+  go r kw kind (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
+    let some tableArrayVal := t.find? kw | return r
     let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
     vals.foldlM (init := r) fun r val => do
       let some t ← tryDecode? val.decodeTable | return r
@@ -320,13 +326,15 @@ where
       let (decls, map) := r
       if let some orig := map.find? name then
         modify fun es => es.push <| .mk val.ref s!"\
-          {p}: target '{name}' was already defined as a '{orig.kind}', \
-          but then redefined as a '{k}'"
+          {pkg}: target '{name}' was already defined as a '{orig.kind}', \
+          but then redefined as a '{kind}'"
         return (decls, map)
       else
-        let cfg ← @decode name t
-        let decl := .mk (.mk p name k cfg) rfl
-        return (decls.push decl, map.insert name (.mk decl rfl))
+        let config ← @decode name t
+        let decl : NConfigDecl pkg name :=
+          -- Safety: By definition, config kind = facet kind for declarative configurations.
+          unsafe {pkg, name, kind, config, wf_data := lcProof}
+        return (decls.push decl.toPConfigDecl, map.insert name decl)
 
 /-! ## Root Loader -/
 
diff --git a/src/lake/Lake/Load/Workspace.lean b/src/lake/Lake/Load/Workspace.lean
index 252e2cb608..4684012a4f 100644
--- a/src/lake/Lake/Load/Workspace.lean
+++ b/src/lake/Lake/Load/Workspace.lean
@@ -5,9 +5,7 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Load.Resolve
-import Lake.Build.Module
-import Lake.Build.Package
-import Lake.Build.Library
+import Lake.Build.InitFacets
 
 /-! # Workspace Loader
 
@@ -29,9 +27,7 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
     root
     lakeEnv := config.lakeEnv
     lakeArgs? := config.lakeArgs?
-    moduleFacetConfigs := initModuleFacetConfigs
-    packageFacetConfigs := initPackageFacetConfigs
-    libraryFacetConfigs := initLibraryFacetConfigs
+    facetConfigs := initFacetConfigs
   }
   if let some env := env? then
     IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts
diff --git a/src/lake/Lake/Toml/Encode.lean b/src/lake/Lake/Toml/Encode.lean
index e3e425df43..e874e79f74 100644
--- a/src/lake/Lake/Toml/Encode.lean
+++ b/src/lake/Lake/Toml/Encode.lean
@@ -32,6 +32,7 @@ instance : ToToml Nat := ⟨fun n => .integer .missing (.ofNat n)⟩
 instance : ToToml Float := ⟨.float .missing⟩
 instance : ToToml Bool := ⟨.boolean .missing⟩
 instance [ToToml α] : ToToml (Array α) := ⟨(.array .missing <| ·.map toToml)⟩
+instance : ToToml (Array Value) := ⟨(.array .missing <| ·)⟩
 instance : ToToml Table := ⟨.table .missing⟩
 
 /-- Insert a value into a table unless it represents a nullish value. -/
diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean
index f7dc01b6aa..34ac2adbb7 100644
--- a/src/lake/Lake/Util/Family.lean
+++ b/src/lake/Lake/Util/Family.lean
@@ -9,55 +9,61 @@ import Lean.Parser.Command
 /-!
 # Open Type Families in Lean
 
-This module contains utilities for defining **open type families** in Lean.
+This module contains utilities for defining **open families** in Lean.
 
-The concept of type families originated in Haskell with the paper
+The concept of families originated in Haskell with the paper
 [*Type checking with open type functions*][1] by Schrijvers *et al.* and
 is essentially just a fancy name for a function from an input *index* to an
-output type. However, it tends to imply some additional restrictions on syntax
-or functionality as opposed to a proper type function.The design here has some
-such limitations so the name was similarly adopted.
+output type. However, the concept implies some additional restrictions on
+the syntax and/or functionality versus a proper function. The design here has
+similar limitations, hence the adaption of the name.
 
-Type families come in two forms: open and closed.
-A *closed* type family is an ordinary total function.
-An *open* type family, on the other hand, is a partial function that allows
+Families come in two forms: open and closed.
+A *closed* family is an ordinary total function.
+An *open* family is a partial function that allows
 additional input to output mappings to be defined as needed.
 
-Lean does not (currently) directly support open type families.
+Lean does not (currently) directly support open families.
 However, it does support type class *functional dependencies* (via `outParam`),
-and simple open type families can be modeled through functional dependencies,
+and simple open families can be modeled through functional dependencies,
 which is what we do here.
 
 [1]: https://doi.org/10.1145/1411204.1411215
 
 ## Defining Families
 
-In this approach, to define an open type family, one first defines an `opaque`
-type function with a single argument that serves as the key:
+In this approach, to define an open family, one first defines an `opaque`
+function with a single argument that serves as the index:
 
 ```lean
-opaque FooFam (key : Name) : Type
+opaque FooFam (idx : Name) : Type
 ```
 
-Note that, unlike Haskell, the key need not be a type. Lean's dependent type
-theory does not have Haskell's strict separation of types and data and thus
-we can use data as an index as well.
+Note that, unlike Haskell, the index need not be a type. Lean's dependent type
+theory does not have Haskell's strict separation of types and data, enabling
+this generalization.
 
-Then, to add a mapping to this family, one defines an axioms:
+Similarly, the output of a family need not be a type. In such a case, though,
+the family must be marked `noncomputable`:
+
+```lean
+noncomputable opaque fooFam (idx : Name) : Name
+```
+
+To add a mapping to a family, one first defines an axiom:
 
 ```lean
 axiom FooFam.bar : FooFam `bar = Nat
 ```
 
-To finish, one also defines an instance of the `FamilyDef` type class
-defined in this module using the axiom like so:
+Then defines an instance of the `FamilyDef` type class using the axiom:
 
 ```lean
 instance : FamilyDef FooFam `bar Nat := ⟨FooFam.bar⟩
 ```
 
-This module provides a `family_def` macro to define both the axiom and the
-instance in one go like so:
+This module also provides a `family_def` macro to define both the axiom
+and the instance in one go:
 
 ```lean
 family_def bar : FooFam `bar := Nat
@@ -71,12 +77,12 @@ The signature of the type class `FamilyDef` is
 FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop
 ```
 
-The key part being that `β` is an `outParam` so Lean's type class synthesis will
-smartly infer the defined type `Nat` when given the key of `` `bar``. Thus, if
-we have a function define like so:
+The index part being that `β` is an `outParam` so Lean's type class synthesis
+will smartly infer the defined type `Nat` when given the index of `` `bar``.
+Thus, if we have a function define like so:
 
 ```
-def foo (key : α) [FamilyDef FooFam key β] : β := ...
+def foo (idx : α) [FamilyDef FooFam idx β] : β := ...
 ```
 
 Lean will smartly infer that the type of ``foo `bar`` is `Nat`.
@@ -92,13 +98,13 @@ and `ofFamily : Fam a → β`, to help with this conversion.
 Putting this all together, one can do something like the following:
 
 ```lean
-opaque FooFam (key : Name) : Type
+opaque FooFam (idx : Name) : Type
 
 abbrev FooMap := DRBMap Name FooFam Name.quickCmp
-def FooMap.insert (self : FooMap) (key : Name) [FamilyDef FooFam key α] (a : α) : FooMap :=
-  DRBMap.insert self key (toFamily a)
-def FooMap.find? (self : FooMap) (key : Name) [FamilyDef FooFam key α] : Option α :=
-  ofFamily <$> DRBMap.find? self key
+def FooMap.insert (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] (a : α) : FooMap :=
+  DRBMap.insert self idx (toFamily a)
+def FooMap.find? (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] : Option α :=
+  ofFamily <$> DRBMap.find? self idx
 
 family_def bar : FooFam `bar := Nat
 family_def baz : FooFam `baz := String
@@ -115,55 +121,59 @@ def foo := Id.run do
 
 In order to maintain type safety, `a = b → Fam a = Fam b` must actually hold.
 That is, one must not define mappings to two different types with equivalent
-keys. Since mappings are defined through axioms, Lean WILL NOT catch violations
-of this rule itself, so extra care must be taken when defining mappings.
+indices. Since mappings are defined through axioms, Lean WILL NOT catch
+violations of this rule itself, so extra care must be taken when defining
+mappings.
 
 In Lake, this is solved by having its open type families be indexed by a
 `Lean.Name` and defining each mapping using a name literal `name` and the
 declaration ``axiom Fam.name : Fam `name = α``. This causes a name clash
-if two keys overlap and thereby produces an error.
+if two indices overlap and thereby produces an error.
 -/
 
-open Lean
-
 namespace Lake
 
 /-! ## API -/
 
 /--
-Defines a single mapping of the **open type family** `Fam`, namely `Fam a = β`.
+Defines a single mapping of the **open family** `f`, namely `f a = b`.
 See the module documentation of `Lake.Util.Family` for details on what an open
-type family is in Lake.
+family is in Lake.
 -/
-class FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : semiOutParam $ Type v) : Prop where
-  family_key_eq_type : Fam a = β
+class FamilyDef {α : Type u} {β : Type v} (f : α → β) (a : α) (b : semiOutParam β) : Prop where
+  fam_eq : f a = b
 
-/-- Like `FamilyDef`, but `β` is an `outParam`. -/
-class FamilyOut {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
-  family_key_eq_type : Fam a = β
+@[deprecated fam_eq (since := "2025-02-22")] abbrev FamilyDef.family_key_eq_type := @FamilyDef.fam_eq
+
+/-- Like `FamilyDef`, but `b` is an `outParam`. -/
+class FamilyOut {α : Type u} {β : Type v} (f : α → β) (a : α) (b : outParam β) : Prop where
+  fam_eq : f a = b
+
+@[deprecated fam_eq (since := "2025-02-22")] abbrev FamilyOut.family_key_eq_type := @FamilyOut.fam_eq
 
 -- Simplifies proofs involving open type families
-attribute [simp] FamilyOut.family_key_eq_type
+attribute [simp] FamilyOut.fam_eq
 
-instance [FamilyDef Fam a β] : FamilyOut Fam a β where
-  family_key_eq_type := FamilyDef.family_key_eq_type
+instance [FamilyDef f a b] : FamilyOut f a b where
+  fam_eq := FamilyDef.fam_eq
 
 /-- The identity relation. -/
-@[default_instance 0] instance : FamilyDef Fam a (Fam a) where
-  family_key_eq_type := rfl
+@[default_instance 0] instance (priority := 0) : FamilyDef f a (f a) where
+  fam_eq := rfl
 
 /-- The constant type family. -/
-instance : FamilyDef (fun _ => β) a β where
-  family_key_eq_type := rfl
+instance : FamilyDef (fun _ => b) a b where
+  fam_eq := rfl
 
-/-- Cast a datum from its individual type to its general family. -/
-@[macro_inline] def toFamily [FamilyOut Fam a β] (b : β) : Fam a :=
-  cast FamilyOut.family_key_eq_type.symm b
+/-- Cast a datum from its specific type to a general type family. -/
+@[macro_inline] def toFamily [FamilyOut F a β] (b : β) : F a :=
+  cast FamilyOut.fam_eq.symm b
 
-/-- Cast a datum from its general family to its individual type. -/
-@[macro_inline] def ofFamily [FamilyOut Fam a β] (b : Fam a) : β :=
-  cast FamilyOut.family_key_eq_type b
+/-- Cast a datum from a general type family to its specific type. -/
+@[macro_inline] def ofFamily [FamilyOut F a β] (b : F a) : β :=
+  cast FamilyOut.fam_eq b
 
+open Lean in
 /--
 The syntax:
 
@@ -171,17 +181,19 @@ The syntax:
 family_def foo : Fam 0 := Nat
 ```
 
-Declares a new mapping for the open type family `Fam` type via the
-production of an axiom `Fam.foo : Data 0 = Nat` and an instance of `FamilyDef`
-that uses this axiom for key `0`.
+Declares a new mapping for the open family `Fam` via the production
+of an axiom `Fam.foo : Fam 0 = Nat` and an instance of `FamilyDef`
+that uses this axiom for the index `0`.
 -/
-scoped macro (name := familyDef) doc?:optional(Parser.Command.docComment)
-"family_def " id:ident " : " fam:ident key:term " := " ty:term : command => do
+scoped macro (name := familyDef)
+  doc?:optional(Lean.Parser.Command.docComment)
+  "family_def " id:ident " : " fam:ident idx:term " := " val:term
+: command => do
   let tid := extractMacroScopes fam.getId |>.name
   if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
-    let app := Syntax.mkApp fam #[key]
+    let app := Syntax.mkApp fam #[idx]
     let axm := mkIdentFrom id (canonical := true) <| `_root_ ++ tid ++ id.getId
-    `($[$doc?]? @[simp] axiom $axm : $app = $ty
-    instance : FamilyDef $fam $key $ty := ⟨$axm⟩)
+    `($[$doc?]? @[simp] axiom $axm : $app = $val
+    instance : FamilyDef $fam $idx $val := ⟨$axm⟩)
   else
     Macro.throwErrorAt fam s!"unknown family '{tid}'"
diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
index 4c4c5e198e..1dbf3c8b82 100644
--- a/src/lake/Lake/Util/Name.lean
+++ b/src/lake/Lake/Util/Name.lean
@@ -52,6 +52,14 @@ instance [FromJson α] : FromJson (NameMap α) where
 namespace Name
 open Lean.Name
 
+def eraseHead : Name → Name
+| .anonymous | .str .anonymous _  | .num .anonymous _  => .anonymous
+| .str p s => .str (eraseHead p) s
+| .num p s => .num (eraseHead p) s
+
+theorem eq_anonymous_of_isAnonymous {n : Name} : (h : n.isAnonymous) → n = .anonymous := by
+  cases n <;> simp [Name.isAnonymous]
+
 @[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by
   rw [← beq_iff_eq (a := m) (b := n)]; cases m == n <;> simp +decide
 
@@ -95,5 +103,7 @@ instance : LawfulCmpEq Name Name.quickCmp where
   cmp_rfl := quickCmp_rfl
 
 open Syntax in
-def quoteFrom (ref : Syntax) (n : Name) : Term :=
-  ⟨copyHeadTailInfoFrom (quote n : Term) ref⟩
+def quoteFrom (ref : Syntax) (n : Name) (canonical := false) : Term :=
+  let ref := ref.setHeadInfo (SourceInfo.fromRef ref canonical)
+  let stx := copyHeadTailInfoFrom (quote n : Term) ref
+  ⟨stx⟩
diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean
index 92ccfec75d..402f248125 100644
--- a/src/lake/Lake/Util/StoreInsts.lean
+++ b/src/lake/Lake/Util/StoreInsts.lean
@@ -46,5 +46,5 @@ instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore Name α (StateRefT' ω (N
   store k a := modify (·.insert k a)
 
 @[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m where
-  fetch? := cast (by rw [t.family_key_eq_type]) <| fetch? (m := m) k
-  store a := store k <| cast t.family_key_eq_type.symm a
+  fetch? := cast (by rw [t.fam_eq]) <| fetch? (m := m) k
+  store a := store k <| cast t.fam_eq.symm a