feat: preliminary custom package facets

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) :=

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
 

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"

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 . -/

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

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 := {}
   /--

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)

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⟩
 

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, ·⟩)

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

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"

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"

Lake/DSL/ModuleFacet.lean

@@ -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"

Lake/DSL/Target.lean

@@ -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"

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

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