fix: parameterize CustomData by package and target name
This commit is contained in:
tydeu
parent
7049a8da5f
commit
0875473b13
9 changed files with 80 additions and 55 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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 . -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue