diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index 7d95a6570c..8006f1b11a 100644
--- a/Lake/Build/Data.lean
+++ b/Lake/Build/Data.lean
@@ -44,13 +44,13 @@ as needed (via `target_data`).
 opaque TargetData (facet : WfName) : Type
 
 /--
-The open type family which maps a custom target's name to its build data
-in the Lake build store.
+The open type family which maps a custom target (package × target name) to
+its build data in the Lake build store.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `custom_data`).
 -/
-opaque CustomData (target : WfName) : Type
+opaque CustomData (target : WfName × WfName) : Type
 
 --------------------------------------------------------------------------------
 /-! ## Build Data                                                             -/
@@ -65,7 +65,7 @@ abbrev BuildData : BuildKey → Type
 | .moduleFacet _ f => ModuleData f
 | .packageFacet _ f => PackageData f
 | .targetFacet _ _ f => TargetData f
-| .customTarget _ t => CustomData t
+| .customTarget p t => CustomData (p, t)
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/
@@ -75,26 +75,28 @@ abbrev BuildData : BuildKey → Type
 scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``PackageData
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  let key := WfName.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $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 := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  let key := WfName.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `TargetData`. -/
 scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
 "target_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``TargetData
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  let key := WfName.quoteNameFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `CustomData`. -/
 scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
-"custom_data " id:ident " : " ty:term : command => do
+"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``CustomData
-  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+  let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
+  let pkg := WfName.quoteNameFrom pkg pkg.getId
+  let tgt := WfName.quoteNameFrom tgt tgt.getId
+  `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index a47438f08d..4f40c13ae8 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -167,10 +167,9 @@ the initial set of Lake package facets (e.g., `extraDep`).
       error s!"do not know how to build package facet `{facet}`"
   | .customTarget pkg target =>
     if let some config := pkg.findTargetConfig? target then
-      if h : target = config.name then
-        have h' : FamilyDef CustomData target (ActiveBuildTarget config.resultType) :=
-          ⟨by simp [h]⟩
-        liftM <| cast (by rw [← h'.family_key_eq_type]) <| config.target.activate
+      if h : pkg.name = config.package ∧ target = config.name then
+        have h' : CustomData (pkg.name, target) = ActiveBuildTarget 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"
     else
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index 7ede07e23d..c636e43b64 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -82,7 +82,7 @@ instance [FamilyDef PackageData f α]
 : FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef CustomData t α]
+instance [FamilyDef CustomData (p.name, t) α]
 : FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
   family_key_eq_type := by unfold BuildData; simp
 
diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean
index 3eabc652fc..3a60cdfbd8 100644
--- a/Lake/Build/Key.lean
+++ b/Lake/Build/Key.lean
@@ -68,34 +68,34 @@ quickCmp k k' = Ordering.eq → k = k' := by
   | moduleFacet m f =>
     cases k'
     case moduleFacet m' f' =>
-      dsimp; split
-      next m_eq => intro f_eq; simp [eq_of_cmp m_eq, eq_of_cmp f_eq]
+      dsimp only; split
+      next m_eq => intro f_eq; rw [eq_of_cmp m_eq, eq_of_cmp f_eq]
       next => intro; contradiction
     all_goals (intro; contradiction)
   | packageFacet p f =>
     cases k'
     case packageFacet p' f' =>
-      dsimp; split
-      next p_eq => intro f_eq; simp [eq_of_cmp p_eq, eq_of_cmp f_eq]
+      dsimp only; split
+      next p_eq => intro f_eq; rw [eq_of_cmp p_eq, eq_of_cmp f_eq]
       next => intro; contradiction
     all_goals (intro; contradiction)
   | targetFacet p t f =>
     cases k'
     case targetFacet p' t' f' =>
-      dsimp; split
+      dsimp only; split
       next p_eq =>
         split
         next t_eq =>
           intro f_eq
-          simp [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp 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' =>
-      dsimp; split
-      next p_eq => intro t_eq; simp [eq_of_cmp p_eq, eq_of_cmp t_eq]
+      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)
 
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index c3b50c39bd..678e5500af 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -60,8 +60,15 @@ def resolveExeTarget (exe : LeanExe) (facet : String) : Except CliError OpaqueTa
     throw <| CliError.unknownFacet "executable" facet
 
 def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
-  if let some target := pkg.findTargetConfig? target then
-    return pkg.customTarget target.name |>.target
+  if let some config := pkg.findTargetConfig? target then
+    if !facet.isEmpty then
+      throw <| CliError.invalidFacet target facet
+    else if h : pkg.name = config.package then
+      have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) :=
+        ⟨by simp [h]⟩
+      return pkg.customTarget config.name |>.target
+    else
+      throw <| CliError.badTarget pkg.name target config.package config.name
   else if let some exe := pkg.findLeanExe? target then
     resolveExeTarget exe facet
   else if let some lib := pkg.findExternLib? target then
@@ -99,24 +106,31 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Exc
   else
     throw <| CliError.unknownFacet "package" facet
 
-def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget :=
-  if let some (pkg, target) := ws.findTargetConfig? spec then
-    return pkg.customTarget target.name |>.target
-  else if let some exe := ws.findLeanExe? spec.toName then
+def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
+  if let some (pkg, config) := ws.findTargetConfig? target then
+    if !facet.isEmpty then
+      throw <| CliError.invalidFacet config.name facet
+    else if h : pkg.name = config.package then
+      have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) :=
+        ⟨by simp [h]⟩
+      return pkg.customTarget config.name |>.target
+    else
+      throw <| CliError.badTarget pkg.name target config.package config.name
+  else if let some exe := ws.findLeanExe? target then
     resolveExeTarget exe facet
-  else if let some lib := ws.findExternLib? spec.toName then
+  else if let some lib := ws.findExternLib? target then
     if facet.isEmpty then
       return lib.target.withoutInfo
     else
-      throw <| CliError.invalidFacet spec facet
-  else if let some lib := ws.findLeanLib? spec.toName then
+      throw <| CliError.invalidFacet target facet
+  else if let some lib := ws.findLeanLib? target then
     resolveLibTarget lib facet
-  else if let some pkg := ws.findPackage? spec.toName then
+  else if let some pkg := ws.findPackage? target then
     resolvePackageTarget ws pkg facet
-  else if let some mod := ws.findModule? spec.toName then
+  else if let some mod := ws.findModule? target then
     resolveModuleTarget ws mod facet
   else
-    throw <| CliError.unknownTarget spec
+    throw <| CliError.unknownTarget target
 
 def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Except CliError OpaqueTarget := do
   match spec.splitOn "/" with
@@ -133,7 +147,7 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep
       else
         throw <| CliError.unknownModule mod
     else
-      resolveTargetInWorkspace ws spec facet
+      resolveTargetInWorkspace ws spec.toName facet
   | [pkgSpec, targetSpec] =>
     let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec
     let pkg ← parsePackageSpec ws pkgSpec
diff --git a/Lake/CLI/Error.lean b/Lake/CLI/Error.lean
index 18752eb973..60cef8c295 100644
--- a/Lake/CLI/Error.lean
+++ b/Lake/CLI/Error.lean
@@ -22,9 +22,10 @@ inductive CliError
 | unknownModule (mod : Name)
 | unknownPackage (spec : String)
 | unknownFacet (type facet : String)
-| unknownTarget (spec : String)
+| unknownTarget (target : Name)
 | missingModule (pkg : Name) (mod : Name)
 | missingTarget (pkg : Name) (spec : String)
+| badTarget (pkg target cfgPkg cfgName : Name)
 | invalidTargetSpec (spec : String) (tooMany : Char)
 | invalidFacet (target : Name) (facet : String)
 /- Script CLI Error -/
@@ -51,9 +52,10 @@ def toString : CliError → String
 | unknownModule mod       => s!"unknown module `{mod.toString false}`"
 | unknownPackage spec     => s!"unknown package `{spec}`"
 | unknownFacet ty f       => s!"unknown {ty} facet `{f}`"
-| unknownTarget spec      => s!"unknown target `{spec}`"
+| 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}` "
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
 | invalidFacet t f        => s!"invalid facet `{f}`; target {t.toString false} has no facets"
 | unknownScript s         => s!"unknown script {s}"
diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean
index 551c06c330..0f28f89f78 100644
--- a/Lake/Config/TargetConfig.lean
+++ b/Lake/Config/TargetConfig.lean
@@ -12,17 +12,20 @@ namespace Lake
 structure TargetConfig where
   /-- The name of the target. -/
   name : WfName
+  /-- The name of the target's package. -/
+  package : WfName
   /-- The type of the target's build result. -/
   resultType : Type
   /-- The target's build function. -/
   target : BuildTarget resultType
   /-- Proof that target's build result is the correctly typed target.-/
-  data_eq_target : CustomData name = ActiveBuildTarget resultType
+  data_eq_target : CustomData (package, name) = ActiveBuildTarget resultType
 
-custom_data _nil_ : ActiveOpaqueTarget
+family_def _nil_ : CustomData (&`✝, &`✝) := ActiveOpaqueTarget
 
 instance : Inhabited TargetConfig := ⟨{
-  name := &`_nil_
+  name := &`✝
+  package := &`✝
   resultType := PUnit
   target := default
   data_eq_target := family_key_eq_type
@@ -31,7 +34,7 @@ instance : Inhabited TargetConfig := ⟨{
 hydrate_opaque_type OpaqueTargetConfig TargetConfig
 
 instance FamilyDefOfTargetConfig {cfg : TargetConfig}
-: FamilyDef CustomData cfg.name (ActiveBuildTarget cfg.resultType) :=
+: FamilyDef CustomData (cfg.package, cfg.name) (ActiveBuildTarget cfg.resultType) :=
   ⟨cfg.data_eq_target⟩
 
 /-- Try to find a target configuration in the package with the given name . -/
diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean
index 03bbab4c2f..c0f924584b 100644
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@@ -25,7 +25,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
     let axm := mkIdentFrom id <| ``ModuleData ++ id.getId
     `(module_data $id : ActiveBuildTarget $ty
       $[$doc?]? @[$attrs,*] def $id : ModuleFacetConfig := {
-        name := $(WfName.quoteFrom id (WfName.ofName id.getId))
+        name := $(WfName.quoteNameFrom id id.getId)
         resultType := $ty
         build := $defn
         data_eq_target := $axm
@@ -42,7 +42,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
     let axm := mkIdentFrom id <| ``PackageData ++ id.getId
     `(package_data $id : ActiveBuildTarget $ty
       $[$doc?]? @[$attrs,*] def $id : PackageFacetConfig := {
-        name := $(WfName.quoteFrom id (WfName.ofName id.getId))
+        name := $(WfName.quoteNameFrom id id.getId)
         resultType := $ty
         build := $defn
         data_eq_target := $axm
@@ -57,9 +57,12 @@ kw:"target " sig:simpleDeclSig : command => do
     let attr ← withRef kw `(Term.attrInstance| target)
     let attrs := #[attr] ++ expandAttrs attrs?
     let axm := mkIdentFrom id <| ``CustomData ++ id.getId
-    `(custom_data $id : ActiveBuildTarget $ty
+    let name := WfName.quoteNameFrom id id.getId
+    let pkgName ← withRef id `(WfName.ofName $(mkIdentFrom id `_package.name))
+    `(family_def $id : CustomData ($pkgName, $name) := ActiveBuildTarget $ty
       $[$doc?]? @[$attrs,*] def $id : TargetConfig := {
-        name := $(WfName.quoteFrom id (WfName.ofName id.getId))
+        name := $name
+        package := $pkgName
         resultType := $ty
         target := $defn
         data_eq_target := $axm
diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean
index 6c95784f69..0d6a342c28 100644
--- a/Lake/Util/Name.lean
+++ b/Lake/Util/Name.lean
@@ -257,15 +257,17 @@ theorem eq_of_quickCmp :
 instance : EqOfCmp WfName WfName.quickCmp where
   eq_of_cmp h := WfName.eq_of_quickCmp h
 
-open Syntax in
-set_option linter.unusedVariables.patternVars false in -- false positive on `w`
+open Syntax
+
+def quoteNameFrom (ref : Syntax) : Name → Term
+| .anonymous => mkCIdentFrom ref ``anonymous
+| .str p s _ => mkApp (mkCIdentFrom ref ``mkStr)
+  #[quoteNameFrom ref p, quote s]
+| .num p v _ => mkApp (mkCIdentFrom ref ``mkNum)
+  #[quoteNameFrom ref p, quote v]
+
 protected def quoteFrom (ref : Syntax) : WfName → Term
-| ⟨n, w⟩ => match n with
-  | .anonymous => mkCIdentFrom ref ``anonymous
-  | .str p s _ => mkApp (mkCIdentFrom ref ``mkStr)
-    #[WfName.quoteFrom ref ⟨p, w.elimStr⟩, quote s]
-  | .num p v _ => mkApp (mkCIdentFrom ref ``mkNum)
-    #[WfName.quoteFrom ref ⟨p, w.elimNum⟩, quote v]
+| ⟨n, _⟩ => quoteNameFrom ref n
 
 instance : Quote WfName := ⟨WfName.quoteFrom Syntax.missing⟩
 
@@ -282,7 +284,7 @@ properties that help ensure certain features of Lake work as intended.
 -/
 scoped macro:max (name := wfNameLit) "&" noWs stx:name : term =>
   if let some nm := stx.raw.isNameLit? then
-    return WfName.quoteFrom stx <| WfName.ofName nm
+    return WfName.quoteNameFrom stx nm
   else
     Macro.throwErrorAt stx "ill-formed name literal"