From 331c4c39b8a69c045545a38ef823405040570dbf Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 1 Jul 2023 21:00:34 -0400
Subject: [PATCH] feat: type-level named `Package` + target fetch helpers

---
 Lake/Build/Data.lean           | 13 +++++++-----
 Lake/Build/Executable.lean     | 13 ++++++++++++
 Lake/Build/Facets.lean         |  4 ++--
 Lake/Build/Index.lean          |  6 +++---
 Lake/Build/Info.lean           | 33 ++++++++++++----------------
 Lake/Build/Library.lean        | 26 +++++++++++++++++++++++
 Lake/Build/Module.lean         | 19 +++++++++++++++++
 Lake/Build/Package.lean        | 39 ++++++++++++++++++++++++++++++++++
 Lake/Build/Store.lean          | 18 ++++++++--------
 Lake/CLI/Build.lean            | 18 +++++++++-------
 Lake/Config/FacetConfig.lean   | 10 ++++-----
 Lake/Config/Monad.lean         |  2 +-
 Lake/Config/Package.lean       | 18 +++++++++++++---
 Lake/Config/TargetConfig.lean  |  7 +++---
 Lake/Config/Workspace.lean     | 14 ++++++------
 Lake/DSL/DeclUtil.lean         |  8 +++----
 Lake/DSL/Facets.lean           | 10 ++++-----
 Lake/Util/Family.lean          | 31 +++++++++++++++------------
 Lake/Util/StoreInsts.lean      |  2 +-
 examples/ffi/lib/lakefile.lean |  4 ++--
 examples/targets/lakefile.lean |  7 ++++--
 examples/targets/test.sh       |  3 ++-
 22 files changed, 209 insertions(+), 96 deletions(-)

diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index 962e3d699f..79d2579ef4 100644
--- a/Lake/Build/Data.lean
+++ b/Lake/Build/Data.lean
@@ -53,7 +53,10 @@ as needed (via `library_data`).
 -/
 abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
 
-instance [h : FamilyDef TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
+instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α :=
+  ⟨by simp [h.family_key_eq_type]⟩
+
+instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
   ⟨h.family_key_eq_type⟩
 
 /--
@@ -80,10 +83,10 @@ abbrev BuildData : BuildKey → Type
 | .targetFacet _ _ f => TargetData f
 | .customTarget p t => CustomData (p, t)
 
-instance : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
-instance : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
-instance : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
-instance : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨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⟩
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/
diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean
index d9deb2d7e3..8a5f81d6ec 100644
--- a/Lake/Build/Executable.lean
+++ b/Lake/Build/Executable.lean
@@ -7,6 +7,19 @@ import Lake.Build.Common
 
 namespace Lake
 
+/-- Get the Lean executable in the workspace with the configuration's name. -/
+@[inline] def LeanExeConfig.get (self : LeanExeConfig)
+[Monad m] [MonadError m] [MonadLake m] : m LeanExe := do
+  let some exe ← findLeanExe? self.name
+    | error "Lean executable '{self.name}' does not exist in the workspace"
+  return exe
+
+
+/-- Fetch the build of the Lean executable. -/
+@[inline] def LeanExeConfig.fetch
+(self : LeanExeConfig) : IndexBuildM (BuildJob FilePath) := do
+  (← self.get).exe.fetch
+
 /-! # Build Executable -/
 
 protected def LeanExe.recBuildExe
diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean
index c46b94cee6..fc1ddc6987 100644
--- a/Lake/Build/Facets.lean
+++ b/Lake/Build/Facets.lean
@@ -42,8 +42,8 @@ structure ModuleFacet (α) where
 instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
   ⟨facet.data_eq⟩
 
-instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
-  ⟨facet, family_key_eq_type⟩
+instance [FamilyOut ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
+  ⟨facet, FamilyOut.family_key_eq_type⟩
 
 /--
 The core compilation / elaboration of the Lean file via `lean`,
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 593bc7f747..c065840cf5 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -23,7 +23,7 @@ Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
 @[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
-[h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) :=
+[h : FamilyOut TargetData facet α] : IndexBuildM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
 def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
@@ -89,12 +89,12 @@ Recursively build the given info using the Lake build index
 and a topological / suspending scheduler and return the dynamic result.
 -/
 @[macro_inline] def buildIndexTop (info : BuildInfo)
-[FamilyDef BuildData info.key α] : RecBuildM α := do
+[FamilyOut BuildData info.key α] : RecBuildM α := do
   cast (by simp) <| buildIndexTop' info
 
 /-- Build the given Lake target in a fresh build store. -/
 @[inline] def BuildInfo.build
-(self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
+(self : BuildInfo) [FamilyOut BuildData self.key α] : BuildM α :=
   buildIndexTop self |>.run
 
 export BuildInfo (build)
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index fd5c6787f0..f0cb49d21d 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -72,47 +72,40 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 | dynlibExternLib l => l.dynlibBuildKey
 | target p t => p.targetBuildKey t
 
-/-- Class recording that a package `p` has name `n`. -/
-class PackageName (p : Package) (n : outParam Name) : Prop where
-  proof : p.name = n
-
-instance : PackageName p p.name := ⟨rfl⟩
-
 /-! ### Instances for deducing data types of `BuildInfo` keys -/
 
-instance [FamilyDef ModuleData f α]
+instance [FamilyOut ModuleData f α]
 : FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef PackageData f α]
+instance [FamilyOut PackageData f α]
 : FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [h : PackageName p n] [FamilyDef CustomData (n, t) α]
-: FamilyDef BuildData (BuildInfo.key (.target p t)) α where
-  family_key_eq_type := by unfold BuildData; simp [h.proof]
+instance (priority := low) {p : NPackage n} : FamilyDef BuildData
+  (.customTarget p.toPackage.name t) (CustomData (n,t)) := ⟨by simp⟩
 
-instance [FamilyDef CustomData (p.name, t) α]
-: FamilyDef BuildData (BuildInfo.key (.target p t)) α where
+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
 
-instance [FamilyDef TargetData (`leanLib ++ f) α]
+instance [FamilyOut TargetData (`leanLib ++ f) α]
 : FamilyDef BuildData (BuildInfo.key (.libraryFacet l f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef TargetData LeanExe.exeFacet α]
+instance [FamilyOut TargetData LeanExe.exeFacet α]
 : FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef TargetData ExternLib.staticFacet α]
+instance [FamilyOut TargetData ExternLib.staticFacet α]
 : FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef TargetData ExternLib.sharedFacet α]
+instance [FamilyOut TargetData ExternLib.sharedFacet α]
 : FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef TargetData ExternLib.dynlibFacet α]
+instance [FamilyOut TargetData ExternLib.dynlibFacet α]
 : FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
 
@@ -131,8 +124,8 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 /-- The monad for build functions that are part of the index. -/
 abbrev IndexBuildM := IndexT RecBuildM
 
-/-- Fetch the given info using the Lake build index. -/
-@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexBuildM α :=
+/-- Fetch the result associated with the info using the Lake build index. -/
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : IndexBuildM α :=
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)
diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean
index 416f86f28d..123d377288 100644
--- a/Lake/Build/Library.lean
+++ b/Lake/Build/Library.lean
@@ -7,6 +7,32 @@ import Lake.Build.Common
 
 namespace Lake
 
+/-- Get the Lean library in the workspace with the configuration's name. -/
+@[inline] def LeanLibConfig.get (self : LeanLibConfig)
+[Monad m] [MonadError m] [MonadLake m] : m LeanLib := do
+  let some lib ← findLeanLib? self.name
+    | error "Lean library '{self.name}' does not exist in the workspace"
+  return lib
+
+/-- Fetch the build result of a library facet. -/
+@[inline] protected def LibraryFacetDecl.fetch (lib : LeanLib)
+(self : LibraryFacetDecl) [FamilyOut LibraryData self.name α] : IndexBuildM α := do
+  fetch <| lib.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def LibraryFacetConfig.fetchJob (lib : LeanLib)
+(self : LibraryFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "library facet '{self.name}' has no associated build job"
+  return getJob <| ← fetch <| lib.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def LeanLib.fetchFacetJob
+(name : Name) (self : LeanLib) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).libraryFacetConfigs.find? name
+    | error "library facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
 /-! # Build Lean & Static Lib -/
 
 /--
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 034e283df9..7ef6977545 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -11,6 +11,25 @@ open System
 
 namespace Lake
 
+/-- Fetch the build result of a module facet. -/
+@[inline] protected def ModuleFacetDecl.fetch (mod : Module)
+(self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : IndexBuildM α := do
+  fetch <| mod.facet self.name
+
+/-- Fetch the build job of a module facet. -/
+def ModuleFacetConfig.fetchJob (mod : Module)
+(self : ModuleFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "module facet '{self.name}' has no associated build job"
+  return getJob <| ← fetch <| mod.facet self.name
+
+/-- Fetch the build job of a module facet. -/
+def Module.fetchFacetJob
+(name : Name) (self : Module) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).moduleFacetConfigs.find? name
+    | error "library facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
 def Module.buildUnlessUpToDate (mod : Module)
 (dynlibPath : SearchPath) (dynlibs : Array FilePath)
 (depTrace : BuildTrace) : BuildM PUnit := do
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index e0470b4d3d..f95595dd59 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -9,6 +9,45 @@ import Lake.Build.Common
 open System
 namespace Lake
 
+/-- Fetch the build job of the specified package target. -/
+def Package.fetchTargetJob (self : Package)
+(target : Name) : IndexBuildM (Option (BuildJob Unit)) :=  do
+  let some config := self.findTargetConfig? target
+    | error s!"package '{self.name}' has no target '{target}'"
+  return config.getJob (← fetch <| self.target target)
+
+/-- Fetch the build result of a target. -/
+protected def TargetDecl.fetch (self : TargetDecl)
+[FamilyDef CustomData (self.pkg, self.name) α] : IndexBuildM α := do
+  let some pkg ← findPackage? self.pkg
+    | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
+  fetch <| pkg.target self.name
+
+/-- Fetch the build job of the target. -/
+def TargetDecl.fetchJob (self : TargetDecl) : IndexBuildM (BuildJob Unit) :=  do
+  let some pkg ← findPackage? self.pkg
+    | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
+  return self.config.getJob (← fetch <| pkg.target self.name)
+
+/-- Fetch the build result of a package facet. -/
+@[inline] protected def PackageFacetDecl.fetch (pkg : Package)
+(self : PackageFacetDecl) [FamilyOut PackageData self.name α] : IndexBuildM α := do
+  fetch <| pkg.facet self.name
+
+/-- Fetch the build job of a package facet. -/
+def PackageFacetConfig.fetchJob (pkg : Package)
+(self : PackageFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "package facet '{pkg.name}' has no associated build job"
+  return getJob <| ← fetch <| pkg.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def Package.fetchFacetJob
+(name : Name) (self : Package) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).packageFacetConfigs.find? name
+    | error "package facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
 /-- Compute a topological ordering of the package's transitive dependencies. -/
 def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do
   let mut deps := #[]
diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean
index cb88133760..63cf94ed12 100644
--- a/Lake/Build/Store.lean
+++ b/Lake/Build/Store.lean
@@ -32,57 +32,57 @@ set_option linter.unusedVariables false
 
 /-- Derive an array of built module facets from the store. -/
 def collectModuleFacetArray (self : BuildStore)
-(facet : Name) [FamilyDef ModuleData facet α] : Array α := Id.run do
+(facet : Name) [FamilyOut ModuleData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
+        have of_data := by unfold BuildData; simp [h]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive a map of module names to built facets from the store. -/
 def collectModuleFacetMap (self : BuildStore)
-(facet : Name) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
+(facet : Name) [FamilyOut ModuleData facet α] : NameMap α := Id.run do
   let mut res := Lean.mkNameMap α
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
+        have of_data := by unfold BuildData; simp [h]
         res := res.insert m <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built package facets from the store. -/
 def collectPackageFacetArray (self : BuildStore)
-(facet : Name) [FamilyDef PackageData facet α] : Array α := Id.run do
+(facet : Name) [FamilyOut PackageData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .packageFacet _ f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
+        have of_data := by unfold BuildData; simp [h]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built target facets from the store. -/
 def collectTargetFacetArray (self : BuildStore)
-(facet : Name) [FamilyDef TargetData facet α] : Array α := Id.run do
+(facet : Name) [FamilyOut TargetData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .targetFacet _ _ f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
+        have of_data := by unfold BuildData; simp [h]
         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)
-[FamilyDef TargetData `externLib.shared α] : Array α :=
+[FamilyOut TargetData `externLib.shared α] : Array α :=
   self.collectTargetFacetArray `externLib.shared
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 0929c1b432..0f57189588 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -12,23 +12,25 @@ namespace Lake
 
 structure BuildSpec where
   info : BuildInfo
-  getJob : BuildData info.key → Job Unit
+  getBuildJob : BuildData info.key → BuildJob Unit
 
-/-- Get the `Job` associated with some `BuildJob` `BuildData`. -/
-@[inline] def BuildData.toJob
-[FamilyDef BuildData k (BuildJob α)] (data : BuildData k) : Job Unit :=
+@[inline] def BuildSpec.getJob (self : BuildSpec) (data : BuildData self.info.key) : Job Unit :=
+  discard <| self.getBuildJob data
+
+@[inline] def BuildData.toBuildJob
+[FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit :=
   discard <| ofFamily data
 
 @[inline] def mkBuildSpec (info : BuildInfo)
-[FamilyDef BuildData info.key (BuildJob α)] : BuildSpec :=
-  {info, getJob := BuildData.toJob}
+[FamilyOut BuildData info.key (BuildJob α)] : BuildSpec :=
+  {info, getBuildJob := BuildData.toBuildJob}
 
 @[inline] def mkConfigBuildSpec (facetType : String)
 (info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
 : Except CliError BuildSpec := do
   let some getJob := config.getJob?
     | throw <| CliError.nonCliFacet facetType facet
-  return {info, getJob := h ▸ getJob}
+  return {info, getBuildJob := h ▸ getJob}
 
 def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) :=
   self.getJob <$> buildIndexTop' self.info
@@ -89,7 +91,7 @@ def resolveCustomTarget (pkg : Package)
   else do
     let info := pkg.target name
     have h : BuildData info.key = CustomData (pkg.name, name) := rfl
-    return {info, getJob := fun data => discard (h ▸ config.getJob data).toJob}
+    return {info, getBuildJob := h ▸ config.getJob}
 
 def resolveTargetInPackage (ws : Workspace)
 (pkg : Package) (target facet : Name) : Except CliError (Array BuildSpec) :=
diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean
index 3d8f668602..36632967ed 100644
--- a/Lake/Config/FacetConfig.lean
+++ b/Lake/Config/FacetConfig.lean
@@ -13,14 +13,14 @@ structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type
   /-- The facet's build (function). -/
   build : ι → IndexBuildM (DataFam name)
   /-- Does this facet produce an associated asynchronous job? -/
-  getJob? : Option (DataFam name → Job Unit)
+  getJob? : Option (DataFam name → BuildJob Unit)
   deriving Inhabited
 
 protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
 
 /-- A smart constructor for facet configurations that are not known to generate targets. -/
 @[inline] def mkFacetConfig (build : ι → IndexBuildM α)
-[h : FamilyDef Fam facet α] : FacetConfig Fam ι facet where
+[h : FamilyOut Fam facet α] : FacetConfig Fam ι facet where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := none
 
@@ -29,15 +29,15 @@ A smart constructor for facet configurations that generate jobs for the CLI.
 This is for small jobs that do not the increase the progress counter.
 -/
 @[inline] def mkFacetJobConfigSmall (build : ι → IndexBuildM (BuildJob α))
-[h : FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
+[h : FamilyOut Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := some fun data => discard <| ofFamily data
 
 /-- A smart constructor for facet configurations that generate jobs for the CLI.  -/
 @[inline] def mkFacetJobConfig (build : ι → IndexBuildM (BuildJob α))
-[FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet :=
+[FamilyOut Fam facet (BuildJob α)] : FacetConfig Fam ι facet :=
   mkFacetJobConfigSmall fun i => do
-    let ctx ← readThe BuildContext 
+    let ctx ← readThe BuildContext
     ctx.startedBuilds.modify (·+1)
     let job ← build i
     job.bindSync (prio := .default + 1) fun a trace => do
diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean
index bb4dbf1623..77d8e5cd8f 100644
--- a/Lake/Config/Monad.lean
+++ b/Lake/Config/Monad.lean
@@ -56,7 +56,7 @@ variable [Functor m]
   (·.root) <$> read
 
 @[inherit_doc Workspace.findPackage?, inline]
-def findPackage? (name : Name) : m (Option Package) :=
+def findPackage? (name : Name) : m (Option (NPackage name)) :=
   (·.findPackage? name) <$> getWorkspace
 
 @[inherit_doc Workspace.findModule?, inline]
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index d876d93889..e405b80896 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -226,11 +226,23 @@ abbrev PackageSet := HashSet Package
 abbrev OrdPackageSet := OrdHashSet Package
 @[inline] def OrdPackageSet.empty : OrdPackageSet := OrdHashSet.empty
 
-namespace Package
+/-- The package's name. -/
+abbrev Package.name (self : Package) : Name :=
+  self.config.name
+
+/-- A package with a name known at type-level. -/
+structure NPackage (name : Name) extends Package where
+  name_eq : toPackage.name = name
+
+attribute [simp] NPackage.name_eq
+
+instance : CoeOut (NPackage name) Package := ⟨NPackage.toPackage⟩
+instance : CoeDep Package pkg (NPackage pkg.name) := ⟨⟨pkg, rfl⟩⟩
 
 /-- The package's name. -/
-abbrev name (self : Package) : Name :=
-  self.config.name
+abbrev NPackage.name (_ : NPackage n) := n
+
+namespace Package
 
 /-- The package's direct dependencies. -/
 @[inline] def deps (self : Package) : Array Package  :=
diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean
index 39ba2a938f..b272f47209 100644
--- a/Lake/Config/TargetConfig.lean
+++ b/Lake/Config/TargetConfig.lean
@@ -11,16 +11,15 @@ namespace Lake
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  build : (pkg : Package) → [PackageName pkg pkgName] →
-    IndexBuildM (CustomData (pkgName, name))
+  build : (pkg : NPackage pkgName) → IndexBuildM (CustomData (pkgName, name))
   /-- The target's resulting build job. -/
   getJob : CustomData (pkgName, name) → BuildJob Unit
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-(build : (pkg : Package) → [PackageName pkg pkgName] → IndexBuildM (BuildJob α))
-[h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
+(build : (pkg : NPackage pkgName) → IndexBuildM (BuildJob α))
+[h : FamilyOut CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob := fun data => discard <| ofFamily data
 
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 384f6331e2..9f2906e764 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -20,7 +20,7 @@ structure Workspace : Type where
   /-- The detect `Lake.Env` of the workspace. -/
   lakeEnv : Lake.Env
   /-- Name-package map of packages within the workspace. -/
-  packageMap : NameMap Package := {}
+  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. -/
@@ -58,19 +58,19 @@ namespace Workspace
 
 /-- The `List` of packages to the workspace. -/
 def packageList (self : Workspace) : List Package :=
-  self.packageMap.revFold (fun pkgs _ pkg => pkg :: pkgs) []
+  self.packageMap.revFold (fun pkgs _ pkg => pkg.toPackage :: pkgs) []
 
 /-- The `Array` of packages to the workspace. -/
 def packageArray (self : Workspace) : Array Package :=
-  self.packageMap.fold (fun pkgs _ pkg => pkgs.push pkg) #[]
+  self.packageMap.fold (fun pkgs _ pkg => pkgs.push pkg.toPackage) #[]
 
 /-- Add a package to the workspace. -/
 def addPackage (pkg : Package) (self : Workspace) : Workspace :=
   {self with packageMap := self.packageMap.insert pkg.name pkg}
 
 /-- Try to find a package within the workspace with the given name. -/
-@[inline] def findPackage? (pkg : Name) (self : Workspace) : Option Package :=
-  self.packageMap.find? pkg
+@[inline] def findPackage? (name : Name) (self : Workspace) : Option (NPackage name) :=
+  self.packageMap.find? name
 
 /-- Check if the module is local to any package in the workspace. -/
 def isLocalModule (mod : Name) (self : Workspace) : Bool :=
@@ -181,6 +181,4 @@ def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
 
 /-- Remove all packages' build outputs (i.e., delete their build directories). -/
 def clean (self : Workspace) : IO Unit := do
-  for (_, pkg) in self.packageMap do
-    pkg.clean
-  self.root.clean
+  self.packageMap.forM fun _ pkg => pkg.clean
diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean
index 7c2db288b6..ae11f9733a 100644
--- a/Lake/DSL/DeclUtil.lean
+++ b/Lake/DSL/DeclUtil.lean
@@ -73,14 +73,14 @@ def mkConfigStructDecl (name? : Option Name)
 (doc? : Option DocComment) (attrs : Array AttrInstance) (ty : Term)
 : (spec : Syntax) → MacroM Syntax.Command
 | `(structDeclSig| $id:ident) =>
-  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty :=
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
     {name := $(quote id.getId)})
 | `(structDeclSig| $id:ident where $ds;* $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty where
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty where
       name := $(quote id.getId); $ds;* $[$wds?]?)
 | `(structDeclSig| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
-  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $(ty?.getD ty) := $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $(ty?.getD ty) := $defn $[$wds?]?)
 | `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
   let defn ← `({ name := $(quote id.getId), $fs,* })
-  `($[$doc?]? @[$attrs,*] def $(fixName id name?) : $ty := $defn $[$wds?]?)
+  `($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed configuration syntax"
diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean
index 43f5d23bcb..a7c66fca4e 100644
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@@ -40,7 +40,7 @@ kw:"module_facet " sig:buildDeclSig : command => do
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
     let mod ← expandOptSimpleBinder mod?
     `(module_data $id : BuildJob $ty
-      $[$doc?:docComment]? @[$attrs,*] def $facetId : ModuleFacetDecl := {
+      $[$doc?:docComment]? @[$attrs,*] abbrev $facetId : ModuleFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig
           fun $mod => ($defn : IndexBuildM (BuildJob $ty))
@@ -69,7 +69,7 @@ kw:"package_facet " sig:buildDeclSig : command => do
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
     let pkg ← expandOptSimpleBinder pkg?
     `(package_data $id : BuildJob $ty
-      $[$doc?]? @[$attrs,*] def $facetId : PackageFacetDecl := {
+      $[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig
           fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
@@ -98,7 +98,7 @@ kw:"library_facet " sig:buildDeclSig : command => do
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
     let lib ← expandOptSimpleBinder lib?
     `(library_data $id : BuildJob $ty
-      $[$doc?]? @[$attrs,*] def $facetId : LibraryFacetDecl := {
+      $[$doc?]? @[$attrs,*] abbrev $facetId : LibraryFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig
           fun $lib => ($defn : IndexBuildM (BuildJob $ty))
@@ -127,11 +127,11 @@ kw:"target " sig:buildDeclSig : command => do
     let pkgName := mkIdentFrom id `_package.name
     let pkg ← expandOptSimpleBinder pkg?
     `(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
-      $[$doc?]? @[$attrs,*] def $id : TargetDecl := {
+      $[$doc?]? @[$attrs,*] abbrev $id : TargetDecl := {
         pkg := $pkgName
         name := $name
         config := Lake.mkTargetJobConfig
-          fun $pkg _ => ($defn : IndexBuildM (BuildJob $ty))
+          fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
       }  $[$wds?]?)
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
 
diff --git a/Lake/Util/Family.lean b/Lake/Util/Family.lean
index 7d08bb9816..07926f0939 100644
--- a/Lake/Util/Family.lean
+++ b/Lake/Util/Family.lean
@@ -113,14 +113,14 @@ def foo := Id.run do
 ## Type Safety
 
 In order to maintain type safety, `a = b → Fam a = Fam b` must actually hold.
-That is, one must not define mapping to two different types with equivalent
+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.
 
 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 = α`` thus causing a name clash
-if two keys overlap and thereby producing an error.
+declaration ``axiom Fam.name : Fam `name = α``. This causes a name clash
+if two keys overlap and thereby produces an error.
 -/
 
 open Lean
@@ -131,24 +131,29 @@ namespace Lake
 
 /--
 Defines a single mapping of the **open type family** `Fam`, namely `Fam a = β`.
-See the module documentation of `Lake.Util.Family` for details what an open type
-family is in Lake.
+See the module documentation of `Lake.Util.Family` for details on what an open
+type family is in Lake.
 -/
-class FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
+class FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : semiOutParam $ Type v) : Prop where
   family_key_eq_type : Fam a = β
 
-export FamilyDef (family_key_eq_type)
+/-- 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 = β
 
--- Simplifies proofs involving open type families.
-attribute [simp] family_key_eq_type
+-- Simplifies proofs involving open type families
+attribute [simp] FamilyOut.family_key_eq_type
+
+instance [FamilyDef Fam a β] : FamilyOut Fam a β where
+  family_key_eq_type := FamilyDef.family_key_eq_type
 
 /-- Cast a datum from its individual type to its general family. -/
-@[macro_inline] def toFamily [FamilyDef Fam a β] (b : β) : Fam a :=
-  cast family_key_eq_type.symm b
+@[macro_inline] def toFamily [FamilyOut Fam a β] (b : β) : Fam a :=
+  cast FamilyOut.family_key_eq_type.symm b
 
 /-- Cast a datum from its general family to its individual type. -/
-@[macro_inline] def ofFamily [FamilyDef Fam a β] (b : Fam a) : β :=
-  cast family_key_eq_type b
+@[macro_inline] def ofFamily [FamilyOut Fam a β] (b : Fam a) : β :=
+  cast FamilyOut.family_key_eq_type b
 
 /--
 The syntax:
diff --git a/Lake/Util/StoreInsts.lean b/Lake/Util/StoreInsts.lean
index e82f41d54f..03adfbf955 100644
--- a/Lake/Util/StoreInsts.lean
+++ b/Lake/Util/StoreInsts.lean
@@ -21,6 +21,6 @@ instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
 instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) :=
   inferInstanceAs (MonadStore _ _ (StateT (RBMap ..) _))
 
-@[inline] instance [MonadDStore κ β m] [t : FamilyDef β k α] : MonadStore1 k α m where
+@[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1 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
diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean
index ec2ffb4d21..cf6ac018ec 100644
--- a/examples/ffi/lib/lakefile.lean
+++ b/examples/ffi/lib/lakefile.lean
@@ -12,13 +12,13 @@ lean_lib FFI
   root := `Main
 }
 
-target ffi.o (pkg : Package) : FilePath := do
+target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
   let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
   let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
   buildO "ffi.cpp" oFile srcJob flags "c++"
 
-extern_lib libleanffi (pkg : Package) := do
+extern_lib libleanffi pkg := do
   let name := nameToStaticLib "leanffi"
   let ffiO ← fetch <| pkg.target ``ffi.o
   buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean
index 80eb397f02..8a177b5cd0 100644
--- a/examples/targets/lakefile.lean
+++ b/examples/targets/lakefile.lean
@@ -23,7 +23,7 @@ lean_exe b
 lean_exe c
 
 @[default_target]
-target meow (pkg : Package) : Unit := do
+target meow pkg : Unit := do
   IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!"
   return .nil
 
@@ -31,6 +31,9 @@ target bark : Unit := do
   logInfo "Bark!"
   return .nil
 
+target bark_bark : Unit := do
+  bark.fetch
+
 package_facet print_name pkg : Unit := do
   IO.println pkg.name
   return .nil
@@ -39,7 +42,7 @@ module_facet get_src mod : FilePath := do
   inputFile mod.leanFile
 
 module_facet print_src mod : Unit := do
-  (← fetch (mod.facet `get_src)).bindSync fun src trace => do
+  (← fetch <| mod.facet `get_src).bindSync fun src trace => do
     IO.println src
     return ((), trace)
 
diff --git a/examples/targets/test.sh b/examples/targets/test.sh
index fbea23f5cb..f9d1937baa 100755
--- a/examples/targets/test.sh
+++ b/examples/targets/test.sh
@@ -16,7 +16,8 @@ fi
 
 ./clean.sh
 
-$LAKE build targets/bark | grep -m1 Bark!
+$LAKE build bark | grep -m1 Bark!
+$LAKE build targets/bark_bark | grep -m1 Bark!
 $LAKE build Foo.Test:print_src | grep -m1 Test.lean
 $LAKE build foo:print_name | grep -m1 foo