From 2ccd41ac8210ccca08d752b3a4851ec8b3e537ea Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Jun 2022 20:54:49 -0400 Subject: [PATCH] feat: preliminary custom targets --- Lake/Build/Index.lean | 9 +++++-- Lake/Build/Info.lean | 2 -- Lake/CLI/Build.lean | 8 ++++-- Lake/Config/Load.lean | 7 +++++- Lake/Config/ModuleFacetConfig.lean | 2 +- Lake/Config/Opaque.lean | 3 +++ Lake/Config/Package.lean | 4 ++- Lake/Config/TargetConfig.lean | 39 ++++++++++++++++++++++++++++++ Lake/Config/Workspace.lean | 5 ++++ Lake/DSL.lean | 1 + Lake/DSL/Attributes.lean | 6 ++++- Lake/DSL/DeclUtil.lean | 3 +++ Lake/DSL/ModuleFacet.lean | 11 +++------ Lake/DSL/Target.lean | 27 +++++++++++++++++++++ examples/targets/lakefile.lean | 9 +++++++ examples/targets/test.sh | 10 +++++--- 16 files changed, 126 insertions(+), 20 deletions(-) create mode 100644 Lake/Config/TargetConfig.lean create mode 100644 Lake/DSL/Target.lean diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index f9ae3917b7..18467795a1 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -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.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 "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}`" | .staticLeanLib lib => @@ -179,8 +186,6 @@ the initial set of Lake package facets (e.g., `extraDep`). mkTargetBuild ExternLib.sharedFacet do let staticTarget := Target.active <| ← lib.static.recBuild staticToLeanDynlibTarget staticTarget |>.activate - | _ => - error s!"do not know how to build `{info.key}`" /-- Recursively build the given info using the Lake build index diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 1796482f94..6144e39eb6 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -27,7 +27,6 @@ inductive BuildInfo | leanExe (exe : LeanExe) | staticExternLib (lib : ExternLib) | sharedExternLib (lib : ExternLib) -| custom (package : Package) (target : WfName) (facet : WfName) -------------------------------------------------------------------------------- /-! ## Build Info & Keys -/ @@ -67,7 +66,6 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey | leanExe x => x.buildKey | staticExternLib l => l.staticBuildKey | sharedExternLib l => l.sharedBuildKey -| custom p t f => ⟨p.name, t, f⟩ /-! ### Instances for deducing data types of `BuildInfo` keys -/ diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 606b783722..b65d62ceb4 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -60,7 +60,9 @@ 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 exe := pkg.findLeanExe? target then + if let some target := pkg.findTargetConfig? target then + return pkg.facet target.name |>.target + else if let some exe := pkg.findLeanExe? target then resolveExeTarget exe facet else if let some lib := pkg.findExternLib? target then if facet.isEmpty then @@ -96,7 +98,9 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Exc throw <| CliError.unknownFacet "package" facet def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget := - if let some exe := ws.findLeanExe? spec.toName then + if let some (pkg, target) := ws.findTargetConfig? spec then + return pkg.facet 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 if facet.isEmpty then diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index fd1d0a4982..4a9c75e40b 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.TargetConfig namespace Lake open Lean System @@ -124,6 +125,10 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) 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 defaultTargets := defaultTargetAttr.ext.getState env |>.toArray -- Construct the Package if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then @@ -132,7 +137,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) return { dir, config, scripts, leanLibConfigs, leanExeConfigs, externLibConfigs, - opaqueModuleFacetConfigs, + opaqueModuleFacetConfigs, opaqueTargetConfigs, defaultTargets } | _ => error s!"configuration file has multiple `package` declarations" diff --git a/Lake/Config/ModuleFacetConfig.lean b/Lake/Config/ModuleFacetConfig.lean index 5e1b9f2966..a6e4690c96 100644 --- a/Lake/Config/ModuleFacetConfig.lean +++ b/Lake/Config/ModuleFacetConfig.lean @@ -9,7 +9,7 @@ import Lake.Build.Store namespace Lake open Lean System -/-- A Module facet's declarative configuration. -/ +/-- A module facet's declarative configuration. -/ structure ModuleFacetConfig where /-- The name of the facet. -/ facet : WfName diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index 7d6dafa80f..57ff10c9d7 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -15,3 +15,6 @@ declare_opaque_type OpaqueWorkspace /-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/ declare_opaque_type OpaqueModuleFacetConfig + +/-- 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 57c6715b4b..c018f8a837 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -263,8 +263,10 @@ structure Package where leanExeConfigs : NameMap LeanExeConfig := {} /-- External library targets for the package. -/ externLibConfigs : NameMap ExternLibConfig := {} - /-- (Opaque) module facets defined in the package. -/ + /-- (Opaque references to) module facets defined in the package. -/ opaqueModuleFacetConfigs : NameMap OpaqueModuleFacetConfig := {} + /-- (Opaque references to) targets defined in the package. -/ + opaqueTargetConfigs : NameMap OpaqueTargetConfig := {} /-- The names of the package's targets to build by default (i.e., on a bare `lake build` of the package). diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean new file mode 100644 index 0000000000..0eb45c1734 --- /dev/null +++ b/Lake/Config/TargetConfig.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 custom target's declarative configuration. -/ +structure TargetConfig 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 TargetConfig := ⟨{ + name := &`extraDep + resultType := PUnit + build := default + data_eq_target := eq_dynamic_type +}⟩ + +hydrate_opaque_type OpaqueTargetConfig TargetConfig + +instance {cfg : TargetConfig} +: DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) := + ⟨cfg.data_eq_target⟩ + +/-- Try to find a target configuration in the package with the given name . -/ +def Package.findTargetConfig? (name : Name) (self : Package) : Option TargetConfig := + self.opaqueTargetConfigs.find? name |>.map (·.get) diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 6734152fa6..d0317de81d 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -4,6 +4,7 @@ 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 open System @@ -90,6 +91,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 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, ·⟩) + /-- The `LEAN_PATH` of the workspace. -/ def oleanPath (self : Workspace) : SearchPath := self.packageList.map (·.oleanDir) diff --git a/Lake/DSL.lean b/Lake/DSL.lean index aa9ec3f719..c42861f1bf 100644 --- a/Lake/DSL.lean +++ b/Lake/DSL.lean @@ -12,3 +12,4 @@ import Lake.DSL.Script import Lake.DSL.Require import Lake.DSL.Targets import Lake.DSL.ModuleFacet +import Lake.DSL.Target diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean index c7e88c2ecf..cc23ae23b2 100644 --- a/Lake/DSL/Attributes.lean +++ b/Lake/DSL/Attributes.lean @@ -23,13 +23,17 @@ initialize leanExeAttr : TagAttribute ← initialize externLibAttr : TagAttribute ← registerTagAttribute `externLib "mark a definition as a Lake external library target" +initialize targetAttr : TagAttribute ← + registerTagAttribute `target "mark a definition as a custom Lake target" + initialize defaultTargetAttr : TagAttribute ← registerTagAttribute `defaultTarget "mark a Lake target as the package's default" fun name => do let valid ← getEnv <&> fun env => leanLibAttr.hasTag env name || leanExeAttr.hasTag env name || - externLibAttr.hasTag env name + externLibAttr.hasTag env name || + targetAttr.hasTag env name unless valid do throwError "attribute `defaultTarget` can only be used on a target (e.g., `lean_lib`, `lean_exe`)" diff --git a/Lake/DSL/DeclUtil.lean b/Lake/DSL/DeclUtil.lean index f0d03e18de..3e8dfb5650 100644 --- a/Lake/DSL/DeclUtil.lean +++ b/Lake/DSL/DeclUtil.lean @@ -47,6 +47,9 @@ syntax declValTyped := syntax declValOptTyped := (Term.typeSpec)? declValSimple +syntax simpleDeclSig := + ident Term.typeSpec declValSimple + def expandAttrs (attrs? : Option Attributes) : Array AttrInstance := if let some attrs := attrs? then match attrs with diff --git a/Lake/DSL/ModuleFacet.lean b/Lake/DSL/ModuleFacet.lean index 6e0f7bd45d..b230e0f9ac 100644 --- a/Lake/DSL/ModuleFacet.lean +++ b/Lake/DSL/ModuleFacet.lean @@ -9,15 +9,12 @@ import Lake.Config.ModuleFacetConfig namespace Lake.DSL open Lean Parser Command -syntax moduleFacetDeclSpec := - ident Term.typeSpec declValSimple - scoped macro (name := moduleFacetDecl) doc?:optional(docComment) attrs?:optional(Term.attributes) -"module_facet " spec:moduleFacetDeclSpec : command => do - match spec with - | `(moduleFacetDeclSpec| $id:ident : $ty := $defn $[$wds?]?) => - let attr ← `(Term.attrInstance| moduleFacet) +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 diff --git a/Lake/DSL/Target.lean b/Lake/DSL/Target.lean new file mode 100644 index 0000000000..9d20444523 --- /dev/null +++ b/Lake/DSL/Target.lean @@ -0,0 +1,27 @@ +/- +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 fdeee09a8e..a7173ee84b 100644 --- a/examples/targets/lakefile.lean +++ b/examples/targets/lakefile.lean @@ -15,3 +15,12 @@ lean_exe b @[defaultTarget] lean_exe c + +@[defaultTarget] +target meow : PUnit := fun pkg => do + IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!" + return ActiveTarget.nil + +target bark : PUnit := fun _ => do + logInfo "Bark!" + return ActiveTarget.nil diff --git a/examples/targets/test.sh b/examples/targets/test.sh index 6f6c4728af..a19f4aeba8 100755 --- a/examples/targets/test.sh +++ b/examples/targets/test.sh @@ -1,9 +1,8 @@ -set -e +#!/usr/bin/env bash +set -exo pipefail LAKE=${LAKE:-../../build/bin/lake} -set -x - if [ "$OS" = Windows_NT ]; then SHARED_LIB_EXT=dll elif [ "`uname`" = Darwin ]; then @@ -14,6 +13,8 @@ fi ./clean.sh +$LAKE build bark | grep -m1 Bark! + $LAKE build +Foo.Test test -f ./build/lib/Foo/Test.olean @@ -27,6 +28,7 @@ $LAKE build ./build/bin/c test -f ./build/lib/Foo.olean +cat ./build/meow.txt | grep -m1 Meow! $LAKE build a b @@ -38,3 +40,5 @@ $LAKE build bar:shared test -f ./build/lib/libFoo.a test -f ./build/lib/Bar.$SHARED_LIB_EXT + +$LAKE build bark | grep -m1 Bark!