From 6bb51012562685f052db21865fed8afaced4ae17 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 27 Jul 2022 19:54:15 -0400
Subject: [PATCH] refactor:  pattern `TargetConfig`  off `FacetConfig`

---
 Lake/Build/Executable.lean     |  2 --
 Lake/Build/Index.lean          | 14 ++----------
 Lake/Build/Library.lean        |  8 +++----
 Lake/Build/Module.lean         | 14 ++++++------
 Lake/Build/Package.lean        |  4 ++--
 Lake/CLI/Build.lean            | 26 ++++++++++-----------
 Lake/CLI/Error.lean            |  8 +++----
 Lake/Config/FacetConfig.lean   |  6 +++++
 Lake/Config/Opaque.lean        |  2 +-
 Lake/Config/Package.lean       |  6 ++---
 Lake/Config/TargetConfig.lean  | 41 ++++++++++++++--------------------
 Lake/Config/Workspace.lean     |  6 ++---
 Lake/DSL/Facets.lean           | 15 +++++--------
 Lake/Load/Package.lean         | 28 +++++++++--------------
 Lake/Util/Compare.lean         | 18 ++++++++++++++-
 Lake/Util/Task.lean            |  2 ++
 examples/targets/lakefile.lean | 14 ++++++------
 examples/targets/test.sh       |  2 ++
 18 files changed, 106 insertions(+), 110 deletions(-)

diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean
index 97d11cdd3a..7cfdd560f2 100644
--- a/Lake/Build/Executable.lean
+++ b/Lake/Build/Executable.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Info
-import Lake.Build.Store
 import Lake.Build.Targets
 
 namespace Lake
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 0dcc0e06ab..7da4ee75c0 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -44,13 +44,9 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
     error s!"do not know how to build package facet `{facet}`"
 | .customTarget pkg target =>
   if let some config := pkg.findTargetConfig? target then
-    if h : pkg.name = config.package ∧ target = config.name then
-      have h' : CustomData (pkg.name, target) = BuildJob config.resultType := by simp [h]
-      liftM <| cast (by rw [← h']) <| config.target.activate
-    else
-      error "target's name in the configuration does not match the name it was registered with"
+    config.build pkg
   else
-      error s!"could not build `{target}` of `{pkg.name}` -- target not found"
+    error s!"could not build `{target}` of `{pkg.name}` -- target not found"
 | .libraryFacet lib facet => do
   if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
     config.build lib
@@ -98,12 +94,6 @@ export BuildInfo (build)
 [FamilyDef BuildData self.key (BuildJob α)] : BuildTarget α :=
   Target.mk <| self.build |>.catchFailure fun _ => pure failure
 
-/-- A smart constructor for facet configurations that generate CLI targets. -/
-@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (BuildJob α))
-[h : FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
-  build := cast (by rw [← h.family_key_eq_type]) build
-  getJob? := some fun data => discard <| ofFamily data
-
 /-! ### Lean Executable Builds -/
 
 @[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean
index 9f55a05b71..023e66e270 100644
--- a/Lake/Build/Library.lean
+++ b/Lake/Build/Library.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Index
+import Lake.Build.Targets
 
 namespace Lake
 
@@ -32,7 +32,7 @@ protected def LeanLib.recBuildLean
 
 /-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
 def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
-  mkFacetTargetConfig (·.recBuildLean)
+  mkFacetJobConfig (·.recBuildLean)
 
 protected def LeanLib.recBuildStatic
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
@@ -41,7 +41,7 @@ protected def LeanLib.recBuildStatic
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
-  mkFacetTargetConfig (·.recBuildStatic)
+  mkFacetJobConfig (·.recBuildStatic)
 
 /-! # Build Shared Lib -/
 
@@ -83,7 +83,7 @@ protected def LeanLib.recBuildShared
 
 /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
 def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
-  mkFacetTargetConfig (·.recBuildShared)
+  mkFacetJobConfig (·.recBuildShared)
 
 open LeanLib in
 /--
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index abcb0141c9..cef5c27ac3 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Mac Malone
 -/
 import Lean.Elab.Import
-import Lake.Build.Index
+import Lake.Build.Targets
 
 open System
 
@@ -126,19 +126,19 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact)
 
 /-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
 def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
-  mkFacetTargetConfig (·.recBuildLean .leanBin)
+  mkFacetJobConfig (·.recBuildLean .leanBin)
 
 /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
 def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
-  mkFacetTargetConfig (·.recBuildLean .olean)
+  mkFacetJobConfig (·.recBuildLean .olean)
 
 /-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
 def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
-  mkFacetTargetConfig (·.recBuildLean .ilean)
+  mkFacetJobConfig (·.recBuildLean .ilean)
 
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 def Module.cFacetConfig : ModuleFacetConfig cFacet :=
-  mkFacetTargetConfig (·.recBuildLean .c)
+  mkFacetJobConfig (·.recBuildLean .c)
 
 /-- Recursively build the module's object file from its C file produced by `lean`. -/
 def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
@@ -147,7 +147,7 @@ def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
 
 /-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
 def Module.oFacetConfig : ModuleFacetConfig oFacet :=
-  mkFacetTargetConfig (·.recBuildLeanO)
+  mkFacetJobConfig (·.recBuildLeanO)
 
 /--
 Recursively parse the Lean files of a module and its imports
@@ -220,7 +220,7 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do
 
 /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
 def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
-  mkFacetTargetConfig (·.recBuildDynlib)
+  mkFacetJobConfig (·.recBuildDynlib)
 
 open Module in
 /--
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index 2b5db86a94..d5c5aa320c 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Index
+import Lake.Build.Targets
 
 namespace Lake
 
@@ -34,7 +34,7 @@ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Uni
 
 /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
-  mkFacetTargetConfig (·.recBuildExtraDepTargets)
+  mkFacetJobConfig (·.recBuildExtraDepTargets)
 
 open Package in
 /--
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index d3ffbefd8e..7c8913e3d1 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -27,15 +27,15 @@ structure BuildSpec where
 (info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
 : Except CliError BuildSpec := do
   let some getJob := config.getJob?
-    | throw <| CliError.nonTargetFacet facetType facet
+    | throw <| CliError.nonCliFacet facetType facet
   return {info, getJob := h ▸ getJob}
 
-def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) := do
-  return self.getJob <| ← buildIndexTop' self.info
+def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) :=
+  self.getJob <$> buildIndexTop' self.info
 
 def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do
   let jobs ← RecBuildM.run do specs.mapM (·.build)
-  jobs.forM (discard <| liftM <| await ·)
+  jobs.forM (discard <| ·.await)
 
 /-! ## Parsing CLI Build Target Specifiers -/
 
@@ -79,15 +79,15 @@ def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError Bu
     throw <| CliError.unknownFacet "external library" facet
 
 def resolveCustomTarget (pkg : Package)
-(target facet : Name) (config : TargetConfig) : Except CliError BuildSpec :=
+(name facet : Name) (config : TargetConfig pkg.name name) : Except CliError BuildSpec :=
   if !facet.isAnonymous then
-    throw <| CliError.invalidFacet target facet
-  else if h : pkg.name = config.package then
-    have : FamilyDef CustomData (pkg.name, config.name) (BuildJob config.resultType) :=
-      ⟨by simp [h]⟩
-    return mkBuildSpec <| pkg.customTarget config.name
-  else
-    throw <| CliError.badTarget pkg.name target config.package config.name
+    throw <| CliError.invalidFacet name facet
+  else do
+    let info := pkg.customTarget name
+    let some getJob := config.getJob?
+      | throw <| CliError.nonCliTarget name
+    have h : BuildData info.key = CustomData (pkg.name, name) := rfl
+    return {info, getJob := h ▸ getJob}
 
 def resolveTargetInPackage (ws : Workspace)
 (pkg : Package) (target facet : Name) : Except CliError BuildSpec :=
@@ -117,7 +117,7 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Excep
 
 def resolveTargetInWorkspace (ws : Workspace)
 (target : Name) (facet : Name) : Except CliError (Array BuildSpec) :=
-  if let some (pkg, config) := ws.findTargetConfig? target then
+  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
diff --git a/Lake/CLI/Error.lean b/Lake/CLI/Error.lean
index 659da26900..c4d1ed614b 100644
--- a/Lake/CLI/Error.lean
+++ b/Lake/CLI/Error.lean
@@ -25,8 +25,8 @@ inductive CliError
 | unknownTarget (target : Name)
 | missingModule (pkg : Name) (mod : Name)
 | missingTarget (pkg : Name) (spec : String)
-| badTarget (pkg target cfgPkg cfgName : Name)
-| nonTargetFacet (type : String) (facet : Name)
+| nonCliTarget (target : Name)
+| nonCliFacet (type : String) (facet : Name)
 | invalidTargetSpec (spec : String) (tooMany : Char)
 | invalidFacet (target : Name) (facet : Name)
 /- Script CLI Error -/
@@ -56,8 +56,8 @@ def toString : CliError → String
 | unknownTarget t         => s!"unknown target `{t.toString false}`"
 | missingModule pkg mod   => s!"package '{pkg.toString false}' has no module '{mod.toString false}'"
 | missingTarget pkg spec  => s!"package '{pkg.toString false}' has no target '{spec}'"
-| badTarget p t p' t'     => s!"target registered as `{p.toString false}/{t.toString false}` but configured as `{p'.toString false}/{t'.toString false}` "
-| nonTargetFacet t f      => s!"{t} facet `{f.toString false}` is not a buildable target"
+| nonCliTarget t          => s!"target `{t.toString false}` is not a buildable via `lake`"
+| nonCliFacet t f         => s!"{t} facet `{f.toString false}` is not a buildable via `lake`"
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
 | invalidFacet t f        => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
 | unknownScript s         => s!"unknown script {s}"
diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean
index 688024f170..6d58b51df5 100644
--- a/Lake/Config/FacetConfig.lean
+++ b/Lake/Config/FacetConfig.lean
@@ -24,6 +24,12 @@ protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := none
 
+/-- A smart constructor for facet configurations that generate jobs for the CLI. -/
+@[inline] def mkFacetJobConfig (build : ι → IndexBuildM (BuildJob α))
+[h : FamilyDef 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 dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where
   name : Name
diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean
index 41c8e513df..93b708c091 100644
--- a/Lake/Config/Opaque.lean
+++ b/Lake/Config/Opaque.lean
@@ -15,4 +15,4 @@ declare_opaque_type OpaquePackage
 declare_opaque_type OpaqueWorkspace
 
 /-- Opaque reference to a `TargetConfig` used for forward declaration. -/
-declare_opaque_type OpaqueTargetConfig
+declare_opaque_type OpaqueTargetConfig (pkgName name : Name)
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 50e75ed9e4..cce875562e 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -125,7 +125,7 @@ deriving Inhabited
 /-! # Package -/
 --------------------------------------------------------------------------------
 
-abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp
+abbrev DNameMap α := DRBMap Name α Name.quickCmp
 @[inline] def DNameMap.empty : DNameMap α := DRBMap.empty
 
 /-- A Lake package -- its location plus its configuration. -/
@@ -147,7 +147,7 @@ structure Package where
   /-- External library targets for the package. -/
   externLibConfigs : NameMap ExternLibConfig := {}
   /-- (Opaque references to) targets defined in the package. -/
-  opaqueTargetConfigs : NameMap OpaqueTargetConfig := {}
+  opaqueTargetConfigs : DNameMap (OpaqueTargetConfig config.name) := {}
   /--
   The names of the package's targets to build by default
   (i.e., on a bare `lake build` of the package).
@@ -165,7 +165,7 @@ abbrev PackageSet := RBTree Package (·.config.name.quickCmp ·.config.name)
 namespace Package
 
 /-- The package's name. -/
-@[inline] def name (self : Package) : Name :=
+abbrev name (self : Package) : Name :=
   self.config.name
 
 /-- An `Array` of the package's direct dependencies. -/
diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean
index d97c2a6e37..0532f30dd5 100644
--- a/Lake/Config/TargetConfig.lean
+++ b/Lake/Config/TargetConfig.lean
@@ -9,34 +9,27 @@ import Lake.Build.Store
 namespace Lake
 
 /-- A custom target's declarative configuration. -/
-structure TargetConfig where
-  /-- The name of the target. -/
-  name : Name
-  /-- The name of the target's package. -/
-  package : Name
-  /-- The type of the target's build result. -/
-  resultType : Type
+structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  target : BuildTarget resultType
-  /-- Proof that target's build result is the correctly typed target.-/
-  data_eq_target : CustomData (package, name) = BuildJob resultType
+  build : Package → IndexBuildM (CustomData (pkgName, name))
+  /-- Does this target produce an associated asynchronous job? -/
+  getJob? : Option (CustomData (pkgName, name) → Job Unit)
+  deriving Inhabited
 
-family_def _nil_ : CustomData (.anonymous, .anonymous) := BuildJob Unit
+/-- A smart constructor for target configurations that generate CLI targets. -/
+@[inline] def mkTargetJobConfig (build : Package → IndexBuildM (BuildJob α))
+[h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
+  build := cast (by rw [← h.family_key_eq_type]) build
+  getJob? := some fun data => discard <| ofFamily data
 
-instance : Inhabited TargetConfig := ⟨{
-  name := .anonymous
-  package := .anonymous
-  resultType := PUnit
-  target := default
-  data_eq_target := family_key_eq_type
-}⟩
+/-- A dependently typed configuration based on its registered package and name. -/
+structure TargetDecl where
+  pkg : Name
+  name : Name
+  config : TargetConfig pkg name
 
-hydrate_opaque_type OpaqueTargetConfig TargetConfig
-
-instance FamilyDefOfTargetConfig {cfg : TargetConfig}
-: FamilyDef CustomData (cfg.package, cfg.name) (BuildJob cfg.resultType) :=
-  ⟨cfg.data_eq_target⟩
+hydrate_opaque_type OpaqueTargetConfig TargetConfig pkgName name
 
 /-- Try to find a target configuration in the package with the given name . -/
-def Package.findTargetConfig? (name : Name) (self : Package) : Option TargetConfig :=
+def Package.findTargetConfig? (name : Name) (self : Package) : Option (TargetConfig self.name name) :=
   self.opaqueTargetConfigs.find? name |>.map (·.get)
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index f775388186..20774adfa1 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -93,12 +93,12 @@ def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
   self.packageArray.findSome? fun pkg => pkg.findExternLib? name
 
 /-- Try to find a target configuration in the workspace with the given name. -/
-def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × TargetConfig) :=
+def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) :=
   self.packageArray.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
 
 /-- Add a module facet to the workspace. -/
 def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
-  {self with moduleFacetConfigs := self.moduleFacetConfigs.insert cfg.name cfg}
+  {self with moduleFacetConfigs := self.moduleFacetConfigs.insert name cfg}
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
 def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
@@ -106,7 +106,7 @@ def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFace
 
 /-- Add a package facet to the workspace. -/
 def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
-  {self with packageFacetConfigs := self.packageFacetConfigs.insert cfg.name cfg}
+  {self with packageFacetConfigs := self.packageFacetConfigs.insert name cfg}
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
 def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean
index e647148def..8711f565be 100644
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@@ -26,7 +26,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
     `(module_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
         name := $name
-        config := Lake.mkFacetTargetConfig $defn
+        config := Lake.mkFacetJobConfig $defn
       })
   | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
 
@@ -41,7 +41,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
     `(package_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
         name := $name
-        config := Lake.mkFacetTargetConfig $defn
+        config := Lake.mkFacetJobConfig $defn
       })
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
@@ -56,7 +56,7 @@ kw:"library_facet " sig:simpleDeclSig : command => do
     `(library_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] def $id : LibraryFacetDecl := {
         name := $name
-        config := Lake.mkFacetTargetConfig $defn
+        config := Lake.mkFacetJobConfig $defn
       })
   | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
 
@@ -67,15 +67,12 @@ kw:"target " sig:simpleDeclSig : command => do
   | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) =>
     let attr ← withRef kw `(Term.attrInstance| target)
     let attrs := #[attr] ++ expandAttrs attrs?
-    let axm := mkIdentFrom id <| ``CustomData ++ id.getId
     let name := Name.quoteFrom id id.getId
     let pkgName := mkIdentFrom id `_package.name
     `(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
-      $[$doc?]? @[$attrs,*] def $id : TargetConfig := {
+      $[$doc?]? @[$attrs,*] def $id : TargetDecl := {
+        pkg := $pkgName
         name := $name
-        package := $pkgName
-        resultType := $ty
-        target := $defn
-        data_eq_target := $axm
+        config := Lake.mkTargetJobConfig $defn
       })
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean
index 4631932b0a..6491e2417e 100644
--- a/Lake/Load/Package.lean
+++ b/Lake/Load/Package.lean
@@ -75,9 +75,13 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
     evalConstCheck env opts LeanExeConfig ``LeanExeConfig name
   let externLibConfigs ← IO.ofExcept <| mkTagMap env externLibAttr fun name =>
     evalConstCheck env opts ExternLibConfig ``ExternLibConfig name
-  let opaqueTargetConfigs ← mkTagMap env targetAttr fun declName =>
-    match evalConstCheck env opts TargetConfig ``TargetConfig declName with
-    | .ok a => pure <| OpaqueTargetConfig.mk a
+  let opaqueTargetConfigs ← mkDTagMap env targetAttr fun name =>
+    match evalConstCheck env opts TargetDecl ``TargetDecl name with
+    | .ok decl =>
+      if h : decl.pkg = self.config.name ∧ decl.name = name then
+        return OpaqueTargetConfig.mk <| h.1 ▸ h.2 ▸ decl.config
+      else
+        error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`"
     | .error e => error e
   let defaultTargets := defaultTargetAttr.ext.getState env |>.fold (·.push ·) #[]
 
@@ -101,26 +105,14 @@ def Workspace.addFacetsFromEnv
   let mut ws := self
   for name in moduleFacetAttr.ext.getState env do
     match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with
-    | .ok decl =>
-      if h : name = decl.name then
-        ws := ws.addModuleFacetConfig <| h ▸ decl.config
-      else
-        error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .ok decl => ws := ws.addModuleFacetConfig <| decl.config
     | .error e => error e
   for name in packageFacetAttr.ext.getState env do
     match evalConstCheck env opts PackageFacetDecl ``PackageFacetDecl name with
-    | .ok decl =>
-      if h : name = decl.name then
-        ws := ws.addPackageFacetConfig <| h ▸ decl.config
-      else
-        error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .ok decl => ws := ws.addPackageFacetConfig <| decl.config
     | .error e => error e
   for name in libraryFacetAttr.ext.getState env do
     match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with
-    | .ok decl =>
-      if h : name = decl.name then
-        ws := ws.addLibraryFacetConfig <| h ▸ decl.config
-      else
-        error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .ok decl => ws := ws.addLibraryFacetConfig <| decl.config
     | .error e => error e
   return ws
diff --git a/Lake/Util/Compare.lean b/Lake/Util/Compare.lean
index 8179ff8743..80a2a880c9 100644
--- a/Lake/Util/Compare.lean
+++ b/Lake/Util/Compare.lean
@@ -46,7 +46,6 @@ instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
 instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
   eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
 
-
 -- ## Basic Instances
 
 theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
@@ -108,3 +107,20 @@ instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp)
     intro o
     unfold Option.compareWith
     cases o <;> simp
+
+def Prod.compareWith
+(cmpA : α → α → Ordering) (cmpB : β → β → Ordering)
+: (α × β) → (α × β) → Ordering :=
+  fun (a, b) (a', b') => match cmpA a a' with | .eq => cmpB b b' | ord => ord
+
+instance [EqOfCmp α cmpA] [EqOfCmp β cmpB]
+: EqOfCmp (α × β) (Prod.compareWith cmpA cmpB) where
+  eq_of_cmp := by
+    intro (a, b) (a', b')
+    dsimp only [Prod.compareWith]
+    split; next ha => intro hb; rw [eq_of_cmp ha, eq_of_cmp hb]
+    intros; contradiction
+
+instance [LawfulCmpEq α cmpA] [LawfulCmpEq β cmpB]
+: LawfulCmpEq (α × β) (Prod.compareWith cmpA cmpB) where
+  cmp_rfl := by simp [Prod.compareWith]
diff --git a/Lake/Util/Task.lean b/Lake/Util/Task.lean
index 427e39e952..5d988737fb 100644
--- a/Lake/Util/Task.lean
+++ b/Lake/Util/Task.lean
@@ -18,3 +18,5 @@ instance : Monad BaseIOTask := inferInstanceAs <| Monad Task
 
 abbrev EIOTask ε := ExceptT ε BaseIOTask
 abbrev OptionIOTask := OptionT BaseIOTask
+
+instance : Inhabited (OptionIOTask α) := ⟨failure⟩
diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean
index 6aa718e227..a23d8be643 100644
--- a/examples/targets/lakefile.lean
+++ b/examples/targets/lakefile.lean
@@ -17,14 +17,14 @@ lean_exe b
 lean_exe c
 
 @[defaultTarget]
-target meow : PUnit := Target.mk <| sync (m := BuildM) do
-  IO.FS.writeFile (_package.buildDir / "meow.txt") "Meow!"
-  return default
+target meow : Unit := fun pkg => do
+  IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!"
+  return .nil
 
-target bark : PUnit := Target.mk <| sync (m := BuildM) do
+target bark : Unit := fun _pkg => do
   logInfo "Bark!"
-  return default
+  return .nil
 
-package_facet print_name : PUnit := fun pkg => do
+package_facet print_name : Unit := fun pkg => do
   IO.println pkg.name
-  return BuildJob.nil
+  return .nil
diff --git a/examples/targets/test.sh b/examples/targets/test.sh
index 9b26b85b1a..71a9274202 100755
--- a/examples/targets/test.sh
+++ b/examples/targets/test.sh
@@ -47,3 +47,5 @@ test -f ./build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
 $LAKE build bark | grep -m1 Bark!
 
 $LAKE build targets:print_name | grep -m1 targets
+
+$LAKE build targets:deps && exit 1 || true