From 2f9eefd35a53d8e90a86bb2845583abe4411a30d Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 1 Jul 2022 04:52:50 -0400 Subject: [PATCH] feat: inductive `BuildKey` + proper custom targets --- Lake/Build/Data.lean | 37 +++----- Lake/Build/Index.lean | 41 ++++---- Lake/Build/IndexTargets.lean | 2 +- Lake/Build/Info.lean | 59 +++++++----- Lake/Build/Key.lean | 171 ++++++++++++++++------------------ Lake/Build/Store.lean | 54 +++++++---- Lake/CLI/Build.lean | 4 +- Lake/Config/TargetConfig.lean | 8 +- Lake/DSL/Facets.lean | 4 +- Lake/Util/DynamicType.lean | 2 + Lake/Util/Name.lean | 1 + 11 files changed, 205 insertions(+), 178 deletions(-) diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean index 2b2838ad40..c5d59ca0a7 100644 --- a/Lake/Build/Data.lean +++ b/Lake/Build/Data.lean @@ -29,6 +29,9 @@ opaque PackageData (facet : WfName) : Type /-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/ opaque TargetData (facet : WfName) : Type +/-- Type of build data associated with custom targets. -/ +opaque CustomData (target : WfName) : Type + -------------------------------------------------------------------------------- /-! ## Build Data -/ -------------------------------------------------------------------------------- @@ -38,28 +41,11 @@ Type of the build data associated with a key in the Lake build store. It is dynamic type composed of the three separate dynamic types for modules, packages, and targets. -/ -abbrev BuildData (key : BuildKey) := - if key.isModuleKey then - ModuleData key.facet - else if key.isPackageKey then - PackageData key.facet - else - TargetData key.facet - -theorem isModuleKey_data {k : BuildKey} -(h : k.isModuleKey = true) : BuildData k = ModuleData k.facet := by - unfold BuildData; simp [h] - -theorem isPackageKey_data {k : BuildKey} -(h : k.isPackageKey = true) : BuildData k = PackageData k.facet := by - unfold BuildData, BuildKey.isModuleKey - simp [of_decide_eq_true (of_decide_eq_true h |>.1), h] - -theorem isTargetKey_data {k : BuildKey} -(h : k.isTargetKey = true) : BuildData k = TargetData k.facet := by - unfold BuildData, BuildKey.isModuleKey, BuildKey.isPackageKey - have ⟨has_p, has_t⟩ := of_decide_eq_true h - simp [of_decide_eq_true has_p, of_decide_eq_true has_t, h] +abbrev BuildData : BuildKey → Type +| .moduleFacet _ f => ModuleData f +| .packageFacet _ f => PackageData f +| .targetFacet _ _ f => TargetData f +| .customTarget _ t => CustomData t -------------------------------------------------------------------------------- /-! ## Macros for Declaring Build Data -/ @@ -85,3 +71,10 @@ scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment) let dty := mkCIdentFrom (← getRef) ``TargetData let key := WfName.quoteFrom id <| WfName.ofName <| id.getId `($[$doc?]? dynamic_data $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 + let dty := mkCIdentFrom (← getRef) ``CustomData + let key := WfName.quoteFrom id <| WfName.ofName <| id.getId + `($[$doc?]? dynamic_data $id : $dty $key := $ty) diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 5077915bea..5ed65ac082 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -67,10 +67,10 @@ dynamically typed equivalent. cast (by rw [← h.eq_dynamic_type]) build /-- -Converts a conveniently typed target build function into its +Converts a conveniently typed target facet build function into its dynamically typed equivalent. -/ -@[inline] def mkTargetBuild (facet : WfName) (build : IndexT m α) +@[inline] def mkTargetFacetBuild (facet : WfName) (build : IndexT m α) [h : DynamicType TargetData facet α] : IndexT m (TargetData facet) := cast (by rw [← h.eq_dynamic_type]) build @@ -141,47 +141,50 @@ the initial set of Lake package facets (e.g., `extraDep`). @[specialize] def recBuildIndex (info : BuildInfo) : IndexT m (BuildData info.key) := do have : MonadLift BuildM m := ⟨liftM⟩ match info with - | .module mod facet => + | .moduleFacet mod facet => if let some build := moduleBuildMap.find? facet then build mod else if let some config := (← getWorkspace).findModuleFacetConfig? facet then if h : facet = config.name then have : DynamicType ModuleData facet (ActiveBuildTarget config.resultType) := - ⟨by simp [h, eq_dynamic_type]⟩ + ⟨by simp [h]⟩ mkModuleFacetBuild config.build mod else error "module facet's name in the configuration does not match the name it was registered with" else error s!"do not know how to build module facet `{facet}`" - | .package pkg facet => + | .packageFacet pkg facet => if let some build := packageBuildMap.find? facet then build pkg else if let some config := pkg.findPackageFacetConfig? facet then if h : facet = config.name then have : DynamicType PackageData facet (ActiveBuildTarget config.resultType) := - ⟨by simp [h, eq_dynamic_type]⟩ + ⟨by simp [h]⟩ mkPackageFacetBuild config.build pkg else error "package facet's name in the configuration does not match the name it was registered with" - else if let some config := pkg.findTargetConfig? facet then - if h : facet = config.name then - have : DynamicType PackageData facet (ActiveBuildTarget config.resultType) := - ⟨by simp [h, eq_dynamic_type]⟩ - mkPackageFacetBuild config.build pkg + else + 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' : DynamicType CustomData target (ActiveBuildTarget config.resultType) := + ⟨by simp [h]⟩ + cast (by rw [← h'.eq_dynamic_type]) <| config.build pkg else error "target's name in the configuration does not match the name it was registered with" else - error s!"do not know how to build package facet `{facet}`" + error s!"could not build `{target}` of `{pkg.name}` -- target not found" | .staticLeanLib lib => - mkTargetBuild LeanLib.staticFacet lib.recBuildStatic + mkTargetFacetBuild LeanLib.staticFacet lib.recBuildStatic | .sharedLeanLib lib => - mkTargetBuild LeanLib.sharedFacet lib.recBuildShared + mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared | .leanExe exe => - mkTargetBuild LeanExe.facet exe.recBuild + mkTargetFacetBuild LeanExe.facet exe.recBuild | .staticExternLib lib => - mkTargetBuild ExternLib.staticFacet lib.target.activate + mkTargetFacetBuild ExternLib.staticFacet lib.target.activate | .sharedExternLib lib => - mkTargetBuild ExternLib.sharedFacet do + mkTargetFacetBuild ExternLib.sharedFacet do let staticTarget := Target.active <| ← lib.static.recBuild staticToLeanDynlibTarget staticTarget |>.activate @@ -197,8 +200,8 @@ Recursively build the given info using the Lake build index and a topological / suspending scheduler and return the dynamic result. -/ @[inline] def buildIndexTop (info : BuildInfo) -[h : DynamicType BuildData info.key α] : CycleT BuildKey m α := do - cast (by simp [h.eq_dynamic_type]) <| buildIndexTop' (m := m) info +[DynamicType BuildData info.key α] : CycleT BuildKey m α := do + cast (by simp) <| buildIndexTop' (m := m) info end diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean index c387a64055..7096ad04b1 100644 --- a/Lake/Build/IndexTargets.lean +++ b/Lake/Build/IndexTargets.lean @@ -40,7 +40,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : WfName) let buildMods : BuildM _ := do let mods ← self.getModuleArray let modTargets ← failOnBuildCycle <| ← EStateT.run' BuildStore.empty - <| mods.mapM fun mod => buildIndexTop <| BuildInfo.module mod facet + <| mods.mapM fun mod => buildIndexTop <| mod.facet facet (·.task) <$> ActiveTarget.collectOpaqueArray modTargets buildMods.catchFailure fun _ => pure <| failure diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index d8054e3c26..36d9d7f7ac 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -20,13 +20,14 @@ namespace Lake /-- The type of Lake's build info. -/ inductive BuildInfo -| module (module : Module) (facet : WfName) -| package (package : Package) (facet : WfName) +| moduleFacet (module : Module) (facet : WfName) +| packageFacet (package : Package) (facet : WfName) | staticLeanLib (lib : LeanLib) | sharedLeanLib (lib : LeanLib) | leanExe (exe : LeanExe) | staticExternLib (lib : ExternLib) | sharedExternLib (lib : ExternLib) +| customTarget (package : Package) (target : WfName) -------------------------------------------------------------------------------- /-! ## Build Info & Keys -/ @@ -35,67 +36,75 @@ inductive BuildInfo /-! ### Build Key Helper Constructors -/ abbrev Module.facetBuildKey (facet : WfName) (self : Module) : BuildKey := - ⟨none, self.keyName, facet⟩ + .moduleFacet self.name facet abbrev Package.facetBuildKey (facet : WfName) (self : Package) : BuildKey := - ⟨self.name, none, facet⟩ + .packageFacet self.name facet + +abbrev Package.targetBuildKey (target : WfName) (self : Package) : BuildKey := + .customTarget self.name target abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey := - ⟨self.pkg.name, self.name, staticFacet⟩ + .targetFacet self.pkg.name self.name staticFacet abbrev LeanLib.sharedBuildKey (self : LeanLib) : BuildKey := - ⟨self.pkg.name, self.name, sharedFacet⟩ + .targetFacet self.pkg.name self.name sharedFacet abbrev LeanExe.buildKey (self : LeanExe) : BuildKey := - ⟨self.pkg.name, self.name, facet⟩ + .targetFacet self.pkg.name self.name facet abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey := - ⟨self.pkg.name, self.name, staticFacet⟩ + .targetFacet self.pkg.name self.name staticFacet abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey := - ⟨self.pkg.name, self.name, sharedFacet⟩ + .targetFacet self.pkg.name self.name sharedFacet /-! ### Build Info to Key -/ /-- The key that identifies the build in the Lake build store. -/ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey -| module m f => m.facetBuildKey f -| package p f => p.facetBuildKey f +| moduleFacet m f => m.facetBuildKey f +| packageFacet p f => p.facetBuildKey f | staticLeanLib l => l.staticBuildKey | sharedLeanLib l => l.sharedBuildKey | leanExe x => x.buildKey | staticExternLib l => l.staticBuildKey | sharedExternLib l => l.sharedBuildKey +| customTarget p t => p.targetBuildKey t /-! ### Instances for deducing data types of `BuildInfo` keys -/ instance [DynamicType ModuleData f α] -: DynamicType BuildData (BuildInfo.key (.module m f)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] +: DynamicType BuildData (BuildInfo.key (.moduleFacet m f)) α where + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType PackageData f α] -: DynamicType BuildData (BuildInfo.key (.package p f)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] +: DynamicType BuildData (BuildInfo.key (.packageFacet p f)) α where + eq_dynamic_type := by unfold BuildData; simp + +instance [DynamicType CustomData t α] +: DynamicType BuildData (BuildInfo.key (.customTarget p t)) α where + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType TargetData LeanLib.staticFacet α] : DynamicType BuildData (BuildInfo.key (.staticLeanLib l)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType TargetData LeanLib.sharedFacet α] : DynamicType BuildData (BuildInfo.key (.sharedLeanLib l)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType TargetData LeanExe.facet α] : DynamicType BuildData (BuildInfo.key (.leanExe x)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType TargetData ExternLib.staticFacet α] : DynamicType BuildData (BuildInfo.key (.staticExternLib l)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] + eq_dynamic_type := by unfold BuildData; simp instance [DynamicType TargetData ExternLib.sharedFacet α] : DynamicType BuildData (BuildInfo.key (.sharedExternLib l)) α where - eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] + eq_dynamic_type := by unfold BuildData; simp -------------------------------------------------------------------------------- /-! ## Recursive Building -/ @@ -111,7 +120,7 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m /-- Build the given info using the Lake build index. -/ @[inline] def BuildInfo.recBuild (self : BuildInfo) [DynamicType BuildData self.key α] : IndexT m α := - fun build => cast (by simp [eq_dynamic_type]) <| build self + fun build => cast (by simp) <| build self export BuildInfo (recBuild) @@ -147,7 +156,7 @@ namespace Module /-- Build info for the module's specified facet. -/ abbrev facet (facet : WfName) (self : Module) : BuildInfo := - .module self facet + .moduleFacet self facet variable (self : Module) @@ -163,12 +172,16 @@ end Module /-- Build info for the package's specified facet. -/ abbrev Package.facet (facet : WfName) (self : Package) : BuildInfo := - .package self facet + .packageFacet self facet /-- Build info for the package's `extraDepTarget`. -/ abbrev Package.extraDep (self : Package) : BuildInfo := self.facet &`extraDep +/-- Build info for a custom package target. -/ +abbrev Package.customTarget (target : WfName) (self : Package) : BuildInfo := + .customTarget self target + /-- Build info of the Lean library's static binary. -/ abbrev LeanLib.static (self : LeanLib) : BuildInfo := .staticLeanLib self diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean index b5bbe00b31..3eabc652fc 100644 --- a/Lake/Build/Key.lean +++ b/Lake/Build/Key.lean @@ -8,103 +8,96 @@ import Lake.Util.Name namespace Lake /-- The type of keys in the Lake build store. -/ -structure BuildKey where - package? : Option WfName - target? : Option WfName - facet : WfName - deriving Inhabited, Repr, DecidableEq, Hashable +inductive BuildKey +| moduleFacet (module : WfName) (facet : WfName) +| packageFacet (package : WfName) (facet : WfName) +| targetFacet (package : WfName) (target : WfName) (facet : WfName) +| customTarget (package : WfName) (target : WfName) +deriving Inhabited, Repr, DecidableEq, Hashable namespace BuildKey -@[inline] def hasPackage (self : BuildKey) : Bool := - self.package? ≠ none - -@[simp] theorem hasPackage_mk : BuildKey.hasPackage ⟨some p, x, f⟩ := by - simp [BuildKey.hasPackage] - -@[inline] def package (self : BuildKey) (h : self.hasPackage) : WfName := - match mh:self.package? with - | some n => n - | none => absurd mh <| by - unfold hasPackage at h - exact of_decide_eq_true h - -@[inline] def hasTarget (self : BuildKey) : Bool := - self.target? ≠ none - -@[simp] theorem hasTarget_mk : BuildKey.hasTarget ⟨x, some t, f⟩ := by - simp [BuildKey.hasTarget] - -@[inline] def target (self : BuildKey) (h : self.hasTarget) : WfName := - match mh:self.target? with - | some n => n - | none => absurd mh <| by - unfold hasTarget at h - exact of_decide_eq_true h - -@[inline] def isModuleKey (self : BuildKey) : Bool := - self.package? = none ∧ self.hasTarget - -@[simp] theorem isModuleKey_mk : BuildKey.isModuleKey ⟨none, some m, f⟩ := by - simp [BuildKey.isModuleKey] - -@[simp] theorem not_isModuleKey_pkg : ¬BuildKey.isModuleKey ⟨some pkg, x, f⟩ := by - simp [BuildKey.isModuleKey] - -@[inline] def module (self : BuildKey) (h : self.isModuleKey) : WfName := - self.target <| by - unfold isModuleKey at h - exact of_decide_eq_true h |>.2 - -@[inline] def isPackageKey (self : BuildKey) : Bool := - self.hasPackage ∧ self.target? = none - -@[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by - simp [BuildKey.isPackageKey] - -@[simp] theorem not_isPackageKey_target : ¬BuildKey.isPackageKey ⟨o, some t, f⟩ := by - simp [BuildKey.isPackageKey] - -@[inline] def isTargetKey (self : BuildKey) : Bool := - self.hasPackage ∧ self.hasTarget - -@[simp] theorem isTargetKey_mk : BuildKey.isTargetKey ⟨some p, some t, f⟩ := by - simp [BuildKey.isTargetKey] - -protected def toString : (self : BuildKey) → String -| ⟨some p, none, f⟩ => s!"@{p}:{f}" -| ⟨none, some m, f⟩ => s!"+{m}:{f}" -| ⟨some p, some t, f⟩ => s!"{p}/{t}:{f}" -| ⟨none, none, f⟩ => s!":{f}" +def toString : (self : BuildKey) → String +| moduleFacet m f => s!"+{m}:{f}" +| packageFacet p f => s!"@{p}:{f}" +| targetFacet p t f => s!"{p}/{t}:{f}" +| customTarget p t => s!"{p}/{t}" instance : ToString BuildKey := ⟨(·.toString)⟩ -def quickCmp (k k' : BuildKey) := - match Option.compareWith WfName.quickCmp k.package? k'.package? with - | .eq => - match Option.compareWith WfName.quickCmp k.target? k'.target? with - | .eq => k.facet.quickCmp k'.facet - | ord => ord - | ord => ord +def quickCmp (k k' : BuildKey) : Ordering := + match k with + | moduleFacet m f => + match k' with + | moduleFacet m' f' => + match m.quickCmp m' with + | .eq => f.quickCmp f' + | ord => ord + | _ => .lt + | packageFacet p f => + match k' with + | moduleFacet .. => .gt + | packageFacet p' f' => + match p.quickCmp p' with + | .eq => f.quickCmp f' + | ord => ord + | _ => .lt + | targetFacet p t f => + match k' with + | customTarget .. => .lt + | targetFacet p' t' f' => + match p.quickCmp p' with + | .eq => + match t.quickCmp t' with + | .eq => f.quickCmp f' + | ord => ord + | ord => ord + | _=> .gt + | customTarget p t => + match k' with + | customTarget p' t' => + match p.quickCmp p' with + | .eq => t.quickCmp t' + | ord => ord + | _ => .gt -theorem eq_of_quickCmp : -{k k' : _} → quickCmp k k' = Ordering.eq → k = k' := by - intro ⟨p, t, f⟩ ⟨p', t', f'⟩ +theorem eq_of_quickCmp {k k' : BuildKey} : +quickCmp k k' = Ordering.eq → k = k' := by unfold quickCmp - simp only [] - split - next p_eq => - split - next t_eq => - intro f_eq - have p_eq := eq_of_cmp p_eq - have t_eq := eq_of_cmp t_eq - have f_eq := eq_of_cmp f_eq - simp only [p_eq, t_eq, f_eq] - next => - intros; contradiction - next => - intros; contradiction + cases k with + | 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] + 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] + next => intro; contradiction + all_goals (intro; contradiction) + | targetFacet p t f => + cases k' + case targetFacet p' t' f' => + dsimp; 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] + 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] + next => intro; contradiction + all_goals (intro; contradiction) instance : EqOfCmp BuildKey quickCmp where eq_of_cmp := eq_of_quickCmp diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean index 91cea34733..ec3eba0492 100644 --- a/Lake/Build/Store.lean +++ b/Lake/Build/Store.lean @@ -27,14 +27,20 @@ abbrev BuildStore := namespace BuildStore +-- Linter reports false positives on the `v` variables below +set_option linter.unusedVariables false + /-- Derive an array of built module facets from the store. -/ def collectModuleFacetArray (self : BuildStore) (facet : WfName) [DynamicType ModuleData facet α] : Array α := Id.run do let mut res : Array α := #[] for ⟨k, v⟩ in self do - if h : k.isModuleKey ∧ k.facet = facet then - let of_data := by unfold BuildData; simp [h, eq_dynamic_type] - res := res.push <| cast of_data v + match k with + | .moduleFacet m f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h, eq_dynamic_type] + res := res.push <| cast of_data v + | _ => pure () return res /-- Derive a map of module names to built facets from the store. -/ @@ -42,27 +48,41 @@ def collectModuleFacetMap (self : BuildStore) (facet : WfName) [DynamicType ModuleData facet α] : NameMap α := Id.run do let mut res := Lean.mkNameMap α for ⟨k, v⟩ in self do - if h : k.isModuleKey ∧ k.facet = facet then - let of_data := by simp [isModuleKey_data h.1, h.2, eq_dynamic_type] - res := res.insert (k.module h.1) <| cast of_data v + match k with + | .moduleFacet m f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h, eq_dynamic_type] + res := res.insert m <| cast of_data v + | _ => pure () return res -/-- Derive an array of built module facets from the store. -/ +/-- Derive an array of built package facets from the store. -/ def collectPackageFacetArray (self : BuildStore) (facet : WfName) [DynamicType PackageData facet α] : Array α := Id.run do let mut res : Array α := #[] for ⟨k, v⟩ in self do - if h : k.isPackageKey ∧ k.facet = facet then - let of_data := by simp [isPackageKey_data h.1, h.2, eq_dynamic_type] - res := res.push <| cast of_data v + match k with + | .packageFacet _ f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h, eq_dynamic_type] + 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 : WfName) [DynamicType 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, eq_dynamic_type] + 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) -[DynamicType TargetData &`externLib.shared α] : Array α := Id.run do - let mut res : Array α := #[] - for ⟨k, v⟩ in self do - if h : k.isTargetKey ∧ k.facet = &`externLib.shared then - let of_data := by simp [isTargetKey_data h.1, h.2, eq_dynamic_type] - res := res.push <| cast of_data v - return res +[DynamicType TargetData &`externLib.shared α] : Array α := + self.collectTargetFacetArray &`externLib.shared diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index b82796f4a9..e1f8ea884d 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -61,7 +61,7 @@ def resolveExeTarget (exe : LeanExe) (facet : String) : Except CliError OpaqueTa def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget := if let some target := pkg.findTargetConfig? target then - return pkg.facet target.name |>.target + return pkg.customTarget target.name |>.target else if let some exe := pkg.findLeanExe? target then resolveExeTarget exe facet else if let some lib := pkg.findExternLib? target then @@ -101,7 +101,7 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Exc def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget := if let some (pkg, target) := ws.findTargetConfig? spec then - return pkg.facet target.name |>.target + return pkg.customTarget target.name |>.target else if let some exe := ws.findLeanExe? spec.toName then resolveExeTarget exe facet else if let some lib := ws.findExternLib? spec.toName then diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean index 86532ab33f..725ab86d1c 100644 --- a/Lake/Config/TargetConfig.lean +++ b/Lake/Config/TargetConfig.lean @@ -19,10 +19,12 @@ structure TargetConfig where [Monad m] → [MonadLift BuildM m] → [MonadBuildStore m] → Package → IndexT m (ActiveBuildTarget resultType) /-- Proof that target's build result is the correctly typed target.-/ - data_eq_target : PackageData name = ActiveBuildTarget resultType + data_eq_target : CustomData name = ActiveBuildTarget resultType + +custom_data _nil_ : ActiveOpaqueTarget instance : Inhabited TargetConfig := ⟨{ - name := &`extraDep + name := &`_nil_ resultType := PUnit build := default data_eq_target := eq_dynamic_type @@ -31,7 +33,7 @@ instance : Inhabited TargetConfig := ⟨{ hydrate_opaque_type OpaqueTargetConfig TargetConfig instance dynamicTypeOfTargetConfig {cfg : TargetConfig} -: DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) := +: DynamicType CustomData 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 a878966863..206b4ecef7 100644 --- a/Lake/DSL/Facets.lean +++ b/Lake/DSL/Facets.lean @@ -56,8 +56,8 @@ 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 <| ``Lake.PackageData ++ id.getId - `(package_data $id : ActiveBuildTarget $ty + let axm := mkIdentFrom id <| ``CustomData ++ id.getId + `(custom_data $id : ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : TargetConfig := { name := $(WfName.quoteFrom id (WfName.ofName id.getId)) resultType := $ty diff --git a/Lake/Util/DynamicType.lean b/Lake/Util/DynamicType.lean index a935de9823..5e98283fb7 100644 --- a/Lake/Util/DynamicType.lean +++ b/Lake/Util/DynamicType.lean @@ -13,6 +13,8 @@ class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ T export DynamicType (eq_dynamic_type) +attribute [simp] eq_dynamic_type + @[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a := cast eq_dynamic_type.symm b diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 6bd9378af7..6c95784f69 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -258,6 +258,7 @@ 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` protected def quoteFrom (ref : Syntax) : WfName → Term | ⟨n, w⟩ => match n with | .anonymous => mkCIdentFrom ref ``anonymous