refactor: lake: generalize targets (#7185)

This PR refactors Lake's build internals to enable the introduction of targets and facets beyond packages, modules, and libraries. Facets, build keys, build info, and CLI commands have been generalized to arbitrary target types.
2025-03-27 01:52:38 -04:00 · 2025-03-27 01:52:38 -04:00 · 183463ce24
commit 183463ce24
parent 69160750f2
40 changed files with 1227 additions and 748 deletions
--- 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)
--- 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
--- a/src/lake/Lake/Build/ExternLib.lean
+++ 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
--- 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
--- 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
--- 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)) :=
--- 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
--- a/src/lake/Lake/Build/InitFacets.lean
+++ 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
--- 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⟩
--- 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

--- 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
--- 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]
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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")]
--- 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
--- 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
--- 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]*
  )
--- 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)
--- 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
--- a/src/lake/Lake/Config/ConfigTarget.lean
+++ 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
--- 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`.
--- 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
--- 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
--- 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⟩
--- 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
--- 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))
--- 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)

--- 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 :=
--- 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)
--- 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 -/

--- 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
--- 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. -/
--- 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}'"
--- 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⟩
--- 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