From 48d595b722e4d32bbe9ce2615df7397e2e96eeee Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Jun 2022 22:57:18 -0400 Subject: [PATCH] feat: preliminary custom package facets --- Lake/Build/Index.lean | 9 +++- Lake/CLI/Build.lean | 4 +- Lake/Config/Load.lean | 24 ++++++----- Lake/Config/ModuleFacetConfig.lean | 8 ++-- Lake/Config/Opaque.lean | 3 ++ Lake/Config/Package.lean | 2 + Lake/Config/PackageFacetConfig.lean | 39 +++++++++++++++++ Lake/Config/TargetConfig.lean | 2 +- Lake/Config/Workspace.lean | 7 ++- Lake/DSL.lean | 3 +- Lake/DSL/Attributes.lean | 3 ++ Lake/DSL/Facets.lean | 67 +++++++++++++++++++++++++++++ Lake/DSL/ModuleFacet.lean | 27 ------------ Lake/DSL/Target.lean | 27 ------------ examples/targets/lakefile.lean | 4 ++ examples/targets/test.sh | 2 + 16 files changed, 157 insertions(+), 74 deletions(-) create mode 100644 Lake/Config/PackageFacetConfig.lean create mode 100644 Lake/DSL/Facets.lean delete mode 100644 Lake/DSL/ModuleFacet.lean delete mode 100644 Lake/DSL/Target.lean diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 18467795a1..63d8bd0954 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -154,7 +154,7 @@ the initial set of Lake package facets (e.g., `extraDep`). if let some build := moduleBuildMap.find? facet then build mod else if let some config := (← getWorkspace).findModuleFacetConfig? facet then - if h : facet = config.facet then + if h : facet = config.name then have : DynamicType ModuleData facet (ActiveBuildTarget config.resultType) := ⟨by simp [h, eq_dynamic_type]⟩ mkModuleFacetBuild config.build mod @@ -165,6 +165,13 @@ the initial set of Lake package facets (e.g., `extraDep`). | .package 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]⟩ + 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) := diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index b65d62ceb4..ba755d0c88 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -39,7 +39,7 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : String) : Excep else if facet == "dynlib" then return mod.facetTarget dynlibFacet else if let some config := ws.findModuleFacetConfig? facet then - return mod.facetTarget config.facet + return mod.facetTarget config.name else throw <| CliError.unknownFacet "module" facet @@ -94,6 +94,8 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Exc return pkg.sharedLibTarget.withoutInfo else if facet == "leanLib" || facet == "oleans" then return pkg.leanLibTarget.withoutInfo + else if let some config := ws.findPackageFacetConfig? facet then + return pkg.facet config.name |>.target else throw <| CliError.unknownFacet "package" facet diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 4a9c75e40b..89fe810ebb 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -7,6 +7,7 @@ import Lean.Elab.Frontend import Lake.DSL.Attributes import Lake.DSL.Extensions import Lake.Config.ModuleFacetConfig +import Lake.Config.PackageFacetConfig import Lake.Config.TargetConfig namespace Lake @@ -107,12 +108,17 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) if config.defaultFacet = PackageFacet.oleans then logWarning "The `oleans` package facet has been deprecated in favor of `leanLib`." let config := {config with dependencies := depsExt.getState env ++ config.dependencies} - -- Load Target & Script Configurations + -- Tag Load Helpers let mkTagMap {α} (attr) (f : Name → IO α) : IO (NameMap α) := attr.ext.getState env |>.foldM (init := {}) fun map declName => return map.insert declName <| ← f declName let evalConst (α typeName declName) : IO α := IO.ofExcept (env.evalConstCheck α leanOpts typeName declName).run.run + let evalConstMap {α β} (f : α → β) (declName) : IO β := + match env.evalConst α leanOpts declName with + | .ok a => pure <| f a + | .error e => throw <| IO.userError e + -- Load Target & Script Configurations let scripts ← mkTagMap scriptAttr (evalScriptDecl env · leanOpts) let leanLibConfigs ← mkTagMap leanLibAttr @@ -121,14 +127,12 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) (evalConst LeanExeConfig ``LeanExeConfig) let externLibConfigs ← mkTagMap externLibAttr (evalConst ExternLibConfig ``ExternLibConfig) - let opaqueModuleFacetConfigs ← mkTagMap moduleFacetAttr fun declName => - match env.evalConst ModuleFacetConfig leanOpts declName with - | .ok config => pure <| OpaqueModuleFacetConfig.mk config - | .error e => throw <| IO.userError e - let opaqueTargetConfigs ← mkTagMap targetAttr fun declName => - match env.evalConst TargetConfig leanOpts declName with - | .ok config => pure <| OpaqueTargetConfig.mk config - | .error e => throw <| IO.userError e + let opaqueModuleFacetConfigs ← mkTagMap moduleFacetAttr + (evalConstMap OpaqueModuleFacetConfig.mk) + let opaquePackageFacetConfigs ← mkTagMap packageFacetAttr + (evalConstMap OpaquePackageFacetConfig.mk) + let opaqueTargetConfigs ← mkTagMap targetAttr + (evalConstMap OpaqueTargetConfig.mk) let defaultTargets := defaultTargetAttr.ext.getState env |>.toArray -- Construct the Package if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then @@ -137,7 +141,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) return { dir, config, scripts, leanLibConfigs, leanExeConfigs, externLibConfigs, - opaqueModuleFacetConfigs, opaqueTargetConfigs, + opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs, defaultTargets } | _ => error s!"configuration file has multiple `package` declarations" diff --git a/Lake/Config/ModuleFacetConfig.lean b/Lake/Config/ModuleFacetConfig.lean index a6e4690c96..2f22a9ed79 100644 --- a/Lake/Config/ModuleFacetConfig.lean +++ b/Lake/Config/ModuleFacetConfig.lean @@ -12,7 +12,7 @@ open Lean System /-- A module facet's declarative configuration. -/ structure ModuleFacetConfig where /-- The name of the facet. -/ - facet : WfName + name : WfName /-- The type of the facet's build result. -/ resultType : Type /-- The module facet's build function. -/ @@ -20,10 +20,10 @@ structure ModuleFacetConfig where [Monad m] → [MonadLift BuildM m] → [MonadBuildStore m] → Module → IndexT m (ActiveBuildTarget resultType) /-- Proof that module facet's build result is the correctly typed target.-/ - data_eq_target : ModuleData facet = ActiveBuildTarget resultType + data_eq_target : ModuleData name = ActiveBuildTarget resultType instance : Inhabited ModuleFacetConfig := ⟨{ - facet := &`lean.bin + name := &`lean.bin resultType := PUnit build := default data_eq_target := eq_dynamic_type @@ -32,7 +32,7 @@ instance : Inhabited ModuleFacetConfig := ⟨{ hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig instance {cfg : ModuleFacetConfig} -: DynamicType ModuleData cfg.facet (ActiveBuildTarget cfg.resultType) := +: DynamicType ModuleData cfg.name (ActiveBuildTarget cfg.resultType) := ⟨cfg.data_eq_target⟩ /-- Try to find a module facet configuration in the package with the given name . -/ diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index 57ff10c9d7..ee013215cd 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -16,5 +16,8 @@ declare_opaque_type OpaqueWorkspace /-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/ declare_opaque_type OpaqueModuleFacetConfig +/-- Opaque reference to a `PackageFacetConfig` used for forward declaration. -/ +declare_opaque_type OpaquePackageFacetConfig + /-- Opaque reference to a `TargetConfig` used for forward declaration. -/ declare_opaque_type OpaqueTargetConfig diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index c018f8a837..9035f677ec 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -265,6 +265,8 @@ structure Package where externLibConfigs : NameMap ExternLibConfig := {} /-- (Opaque references to) module facets defined in the package. -/ opaqueModuleFacetConfigs : NameMap OpaqueModuleFacetConfig := {} + /-- (Opaque references to) module facets defined in the package. -/ + opaquePackageFacetConfigs : NameMap OpaquePackageFacetConfig := {} /-- (Opaque references to) targets defined in the package. -/ opaqueTargetConfigs : NameMap OpaqueTargetConfig := {} /-- diff --git a/Lake/Config/PackageFacetConfig.lean b/Lake/Config/PackageFacetConfig.lean new file mode 100644 index 0000000000..83fc6f954a --- /dev/null +++ b/Lake/Config/PackageFacetConfig.lean @@ -0,0 +1,39 @@ +/- +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 + +namespace Lake + +/-- A package facet's declarative configuration. -/ +structure PackageFacetConfig where + /-- The name of the target. -/ + name : WfName + /-- The type of the target's build result. -/ + resultType : Type + /-- The target's build function. -/ + build : {m : Type → Type} → + [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 + +instance : Inhabited PackageFacetConfig := ⟨{ + name := &`extraDep + resultType := PUnit + build := default + data_eq_target := eq_dynamic_type +}⟩ + +hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig + +instance (cfg : PackageFacetConfig) +: DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) := + ⟨cfg.data_eq_target⟩ + +/-- Try to find a package configuration in the package with the given name . -/ +def Package.findPackageFacetConfig? (name : Name) (self : Package) : Option PackageFacetConfig := + self.opaquePackageFacetConfigs.find? name |>.map (·.get) diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean index 0eb45c1734..86532ab33f 100644 --- a/Lake/Config/TargetConfig.lean +++ b/Lake/Config/TargetConfig.lean @@ -30,7 +30,7 @@ instance : Inhabited TargetConfig := ⟨{ hydrate_opaque_type OpaqueTargetConfig TargetConfig -instance {cfg : TargetConfig} +instance dynamicTypeOfTargetConfig {cfg : TargetConfig} : DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) := ⟨cfg.data_eq_target⟩ diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index d0317de81d..4a94a1a8ec 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lean.Util.Paths -import Lake.Config.TargetConfig import Lake.Config.ModuleFacetConfig +import Lake.Config.PackageFacetConfig +import Lake.Config.TargetConfig open System open Lean (LeanPaths) @@ -91,6 +92,10 @@ def findExternLib? (name : Name) (self : Workspace) : Option ExternLib := def findModuleFacetConfig? (name : Name) (self : Workspace) : Option ModuleFacetConfig := self.packageArray.findSome? fun pkg => pkg.findModuleFacetConfig? name +/-- Try to find a package facet configuration in the workspace with the given name. -/ +def findPackageFacetConfig? (name : Name) (self : Workspace) : Option PackageFacetConfig := + self.packageArray.findSome? fun pkg => pkg.findPackageFacetConfig? name + /-- Try to find a target configuration in the workspace with the given name. -/ def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × TargetConfig) := self.packageArray.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩) diff --git a/Lake/DSL.lean b/Lake/DSL.lean index c42861f1bf..3eb6bc12f2 100644 --- a/Lake/DSL.lean +++ b/Lake/DSL.lean @@ -11,5 +11,4 @@ import Lake.DSL.Package import Lake.DSL.Script import Lake.DSL.Require import Lake.DSL.Targets -import Lake.DSL.ModuleFacet -import Lake.DSL.Target +import Lake.DSL.Facets diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean index cc23ae23b2..1135ebf80f 100644 --- a/Lake/DSL/Attributes.lean +++ b/Lake/DSL/Attributes.lean @@ -39,3 +39,6 @@ initialize defaultTargetAttr : TagAttribute ← initialize moduleFacetAttr : TagAttribute ← registerTagAttribute `moduleFacet "mark a definition as a Lake module facet" + +initialize packageFacetAttr : TagAttribute ← + registerTagAttribute `packageFacet "mark a definition as a Lake package facet" diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean new file mode 100644 index 0000000000..a878966863 --- /dev/null +++ b/Lake/DSL/Facets.lean @@ -0,0 +1,67 @@ +/- +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.DSL.DeclUtil +import Lake.Config.ModuleFacetConfig +import Lake.Config.PackageFacetConfig +import Lake.Config.TargetConfig + +/-! +Macros for declaring custom facets and targets. +-/ + +namespace Lake.DSL +open Lean Parser Command + +scoped macro (name := moduleFacetDecl) +doc?:optional(docComment) attrs?:optional(Term.attributes) +kw:"module_facet " sig:simpleDeclSig : command => do + match sig with + | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) => + let attr ← withRef kw `(Term.attrInstance| moduleFacet) + let attrs := #[attr] ++ expandAttrs attrs? + 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)) + resultType := $ty + build := $defn + data_eq_target := $axm + }) + | stx => Macro.throwErrorAt stx "ill-formed module facet declaration" + +scoped macro (name := packageFacetDecl) +doc?:optional(docComment) attrs?:optional(Term.attributes) +kw:"package_facet " sig:simpleDeclSig : command => do + match sig with + | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) => + let attr ← withRef kw `(Term.attrInstance| packageFacet) + let attrs := #[attr] ++ expandAttrs attrs? + 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)) + resultType := $ty + build := $defn + data_eq_target := $axm + }) + | stx => Macro.throwErrorAt stx "ill-formed package facet declaration" + +scoped macro (name := targetDecl) +doc?:optional(docComment) attrs?:optional(Term.attributes) +kw:"target " sig:simpleDeclSig : command => do + match sig with + | `(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 + $[$doc?]? @[$attrs,*] def $id : TargetConfig := { + name := $(WfName.quoteFrom id (WfName.ofName id.getId)) + resultType := $ty + build := $defn + data_eq_target := $axm + }) + | stx => Macro.throwErrorAt stx "ill-formed target declaration" diff --git a/Lake/DSL/ModuleFacet.lean b/Lake/DSL/ModuleFacet.lean deleted file mode 100644 index b230e0f9ac..0000000000 --- a/Lake/DSL/ModuleFacet.lean +++ /dev/null @@ -1,27 +0,0 @@ -/- -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.DSL.DeclUtil -import Lake.Config.ModuleFacetConfig - -namespace Lake.DSL -open Lean Parser Command - -scoped macro (name := moduleFacetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"module_facet " sig:simpleDeclSig : command => do - match sig with - | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) => - let attr ← withRef kw `(Term.attrInstance| moduleFacet) - let attrs := #[attr] ++ expandAttrs attrs? - let axm := mkIdentFrom id <| ``Lake.ModuleData ++ id.getId - `(module_data $id : ActiveBuildTarget $ty - $[$doc?]? @[$attrs,*] def $id : ModuleFacetConfig := { - facet := $(WfName.quoteFrom id (WfName.ofName id.getId)) - resultType := $ty - build := $defn - data_eq_target := $axm - }) - | stx => Macro.throwErrorAt stx "ill-formed module facet declaration" diff --git a/Lake/DSL/Target.lean b/Lake/DSL/Target.lean deleted file mode 100644 index 9d20444523..0000000000 --- a/Lake/DSL/Target.lean +++ /dev/null @@ -1,27 +0,0 @@ -/- -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.DSL.DeclUtil -import Lake.Config.TargetConfig - -namespace Lake.DSL -open Lean Parser Command - -scoped macro (name := targetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"target " sig:simpleDeclSig : command => do - match sig with - | `(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 - $[$doc?]? @[$attrs,*] def $id : TargetConfig := { - name := $(WfName.quoteFrom id (WfName.ofName id.getId)) - resultType := $ty - build := $defn - data_eq_target := $axm - }) - | stx => Macro.throwErrorAt stx "ill-formed target declaration" diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean index a7173ee84b..caae985bb0 100644 --- a/examples/targets/lakefile.lean +++ b/examples/targets/lakefile.lean @@ -24,3 +24,7 @@ target meow : PUnit := fun pkg => do target bark : PUnit := fun _ => do logInfo "Bark!" return ActiveTarget.nil + +package_facet print_name : PUnit := fun pkg => do + IO.println pkg.name + return ActiveTarget.nil diff --git a/examples/targets/test.sh b/examples/targets/test.sh index a19f4aeba8..c8ec05cf3c 100755 --- a/examples/targets/test.sh +++ b/examples/targets/test.sh @@ -42,3 +42,5 @@ test -f ./build/lib/libFoo.a test -f ./build/lib/Bar.$SHARED_LIB_EXT $LAKE build bark | grep -m1 Bark! + +$LAKE build targets:print_name | grep -m1 targets