feat: preliminary custom module facets

Author: tydeu

Diff for: Lake/Build/Index.lean

@@ -153,6 +153,13 @@ the initial set of Lake package facets (e.g., `extraDep`).
   | .module 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.facet then
+        have : DynamicType ModuleData facet (ActiveBuildTarget config.resultType) :=
+          ⟨by simp [h, eq_dynamic_type]⟩
+        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 =>

Diff for: Lake/CLI/Build.lean

@@ -25,7 +25,7 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
     | none => throw <| CliError.unknownPackage spec
 
 open Module in
-def resolveModuleTarget (mod : Module) (facet : String) : Except CliError OpaqueTarget :=
+def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : String) : Except CliError OpaqueTarget :=
   if facet.isEmpty || facet == "bin"  then
     return mod.facetTarget binFacet
   else if facet == "ilean" then
@@ -38,6 +38,8 @@ def resolveModuleTarget (mod : Module) (facet : String) : Except CliError Opaque
     return mod.facetTarget oFacet
   else if facet == "dynlib" then
     return mod.facetTarget dynlibFacet
+  else if let some config := ws.findModuleFacetConfig? facet then
+    return mod.facetTarget config.facet
   else
     throw <| CliError.unknownFacet "module" facet
 
@@ -57,7 +59,7 @@ def resolveExeTarget (exe : LeanExe) (facet : String) : Except CliError OpaqueTa
   else
     throw <| CliError.unknownFacet "executable" facet
 
-def resolveTargetInPackage (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
+def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
   if let some exe := pkg.findLeanExe? target then
     resolveExeTarget exe facet
   else if let some lib := pkg.findExternLib? target then
@@ -68,20 +70,20 @@ def resolveTargetInPackage (pkg : Package) (target : Name) (facet : String) : Ex
   else if let some lib := pkg.findLeanLib? target then
     resolveLibTarget lib facet
   else if let some mod := pkg.findModule? target then
-    resolveModuleTarget mod facet
+    resolveModuleTarget ws mod facet
   else
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
-def resolveDefaultPackageTarget (pkg : Package) : Except CliError OpaqueTarget :=
+def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError OpaqueTarget :=
   if pkg.defaultTargets.isEmpty then
     return pkg.defaultTarget
   else
     return Target.collectOpaqueArray <| ←
-      pkg.defaultTargets.mapM (resolveTargetInPackage pkg · "")
+      pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · "")
 
-def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError OpaqueTarget :=
+def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Except CliError OpaqueTarget :=
   if facet.isEmpty then
-    resolveDefaultPackageTarget pkg
+    resolveDefaultPackageTarget ws pkg
   else if facet == "exe" || facet == "bin" then
     return pkg.exeTarget.withoutInfo
   else if facet == "staticLib" then
@@ -104,24 +106,24 @@ def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) :
   else if let some lib := ws.findLeanLib? spec.toName then
     resolveLibTarget lib facet
   else if let some pkg := ws.findPackage? spec.toName then
-    resolvePackageTarget pkg facet
+    resolvePackageTarget ws pkg facet
   else if let some mod := ws.findModule? spec.toName then
-    resolveModuleTarget mod facet
+    resolveModuleTarget ws mod facet
   else
     throw <| CliError.unknownTarget spec
 
 def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Except CliError OpaqueTarget := do
   match spec.splitOn "/" with
   | [spec] =>
     if spec.isEmpty then
-      resolvePackageTarget ws.root facet
+      resolvePackageTarget ws ws.root facet
     else if spec.startsWith "@" then
       let pkg ← parsePackageSpec ws <| spec.drop 1
-      resolvePackageTarget pkg facet
+      resolvePackageTarget ws pkg facet
     else if spec.startsWith "+" then
       let mod := spec.drop 1 |>.toName
       if let some mod := ws.findModule? mod then
-        resolveModuleTarget mod facet
+        resolveModuleTarget ws mod facet
       else
         throw <| CliError.unknownModule mod
     else
@@ -132,11 +134,11 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep
     if targetSpec.startsWith "+" then
       let mod := targetSpec.drop 1 |>.toName
       if let some mod := pkg.findModule? mod then
-        resolveModuleTarget mod facet
+        resolveModuleTarget ws mod facet
       else
         throw <| CliError.unknownModule mod
     else
-      resolveTargetInPackage pkg spec facet
+      resolveTargetInPackage ws pkg spec facet
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 

Diff for: Lake/CLI/Main.lean

@@ -313,7 +313,7 @@ def command : (cmd : String) → CliM PUnit
   let target ← show Except _ _ from do
     let targets ← targetSpecs.mapM <| parseTargetSpec ws
     if targets.isEmpty then
-      resolveDefaultPackageTarget ws.root
+      resolveDefaultPackageTarget ws ws.root
     else
       return Target.collectOpaqueList targets
   let ctx ← mkBuildContext ws config.leanInstall config.lakeInstall

Diff for: Lake/Config/Load.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone
 import Lean.Elab.Frontend
 import Lake.DSL.Attributes
 import Lake.DSL.Extensions
-import Lake.Config.Package
+import Lake.Config.ModuleFacetConfig
 
 namespace Lake
 open Lean System
@@ -95,6 +95,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
     match packageAttr.ext.getState env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
     | [pkgDeclName] =>
+      -- Load Package Configuration
       let config ← evalPackageDecl env pkgDeclName dir args leanOpts
       unless config.dependencies.isEmpty do
         logWarning "Syntax for package dependencies has changed. Use the new `require` syntax."
@@ -105,24 +106,33 @@ 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}
-      let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
-        fun m d => return m.insert d <| ← evalScriptDecl env d leanOpts
-      let leanLibConfigs ← leanLibAttr.ext.getState env |>.foldM (init := {}) fun m d =>
-        let eval := env.evalConstCheck LeanLibConfig leanOpts ``LeanLibConfig d
-        return m.insert d <| ← IO.ofExcept eval.run.run
-      let leanExeConfigs ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d =>
-        let eval := env.evalConstCheck LeanExeConfig leanOpts ``LeanExeConfig d
-        return m.insert d <| ← IO.ofExcept eval.run.run
-      let externLibConfigs ← externLibAttr.ext.getState env |>.foldM (init := {}) fun m d =>
-        let eval := env.evalConstCheck ExternLibConfig leanOpts ``ExternLibConfig d
-        return m.insert d <| ← IO.ofExcept eval.run.run
+      -- Load Target & Script Configurations
+      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 scripts ← mkTagMap scriptAttr
+        (evalScriptDecl env · leanOpts)
+      let leanLibConfigs ← mkTagMap leanLibAttr
+        (evalConst LeanLibConfig ``LeanLibConfig)
+      let leanExeConfigs ← mkTagMap leanExeAttr
+        (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 defaultTargets := defaultTargetAttr.ext.getState env |>.toArray
+      -- Construct the Package
       if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
         logWarning <| "Package targets are deprecated. " ++
           "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
-      let defaultTargets := defaultTargetAttr.ext.getState env |>.toArray
       return {
         dir, config, scripts,
         leanLibConfigs, leanExeConfigs, externLibConfigs,
+        opaqueModuleFacetConfigs,
         defaultTargets
       }
     | _ => error s!"configuration file has multiple `package` declarations"

Diff for: Lake/Config/ModuleFacetConfig.lean

@@ -0,0 +1,40 @@
+/-
+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
+open Lean System
+
+/-- A Module facet's declarative configuration. -/
+structure ModuleFacetConfig where
+  /-- The name of the facet. -/
+  facet : WfName
+  /-- The type of the facet's build result. -/
+  resultType : Type
+  /-- The module facet's build function. -/
+  build : {m : Type → Type} →
+    [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
+
+instance : Inhabited ModuleFacetConfig := ⟨{
+  facet := &`lean.bin
+  resultType := PUnit
+  build := default
+  data_eq_target := eq_dynamic_type
+}⟩
+
+hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig
+
+instance {cfg : ModuleFacetConfig}
+: DynamicType ModuleData cfg.facet (ActiveBuildTarget cfg.resultType) :=
+  ⟨cfg.data_eq_target⟩
+
+/-- Try to find a module facet configuration in the package with the given name . -/
+def Package.findModuleFacetConfig? (name : Name) (self : Package) : Option ModuleFacetConfig :=
+  self.opaqueModuleFacetConfigs.find? name |>.map (·.get)

Diff for: Lake/Config/Monad.lean

@@ -55,6 +55,15 @@ variable [Functor m]
 @[inline] def findModule? (mod : Name) : m (Option Module) :=
   (·.findModule? mod) <$> getWorkspace
 
+@[inline] def findLeanExe? (mod : Name) : m (Option LeanExe) :=
+  (·.findLeanExe? mod) <$> getWorkspace
+
+@[inline] def findLeanLib? (mod : Name) : m (Option LeanLib) :=
+  (·.findLeanLib? mod) <$> getWorkspace
+
+@[inline] def findExternLib? (mod : Name) : m (Option ExternLib) :=
+  (·.findExternLib? mod) <$> getWorkspace
+
 @[inline] def getOleanPath : m SearchPath :=
   (·.oleanPath) <$> getWorkspace
 

Diff for: Lake/Config/Opaque.lean

@@ -3,18 +3,15 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-namespace Lake
+import Lake.Util.Opaque
 
-opaque OpaquePackagePointed : NonemptyType.{0}
+namespace Lake
 
 /-- Opaque reference to a `Package` used for forward declaration. -/
-def OpaquePackage : Type := OpaquePackagePointed.type
-
-instance : Nonempty OpaquePackage := OpaquePackagePointed.property
-
-opaque OpaqueWorkspacePointed : NonemptyType.{0}
+declare_opaque_type OpaquePackage
 
 /-- Opaque reference to a `Workspace` used for forward declaration. -/
-def OpaqueWorkspace : Type := OpaqueWorkspacePointed.type
+declare_opaque_type OpaqueWorkspace
 
-instance : Nonempty OpaqueWorkspace := OpaqueWorkspacePointed.property
+/-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/
+declare_opaque_type OpaqueModuleFacetConfig

Diff for: Lake/Config/Package.lean

@@ -263,37 +263,20 @@ structure Package where
   leanExeConfigs : NameMap LeanExeConfig := {}
   /-- External library targets for the package. -/
   externLibConfigs : NameMap ExternLibConfig := {}
+  /-- (Opaque) module facets defined in the package. -/
+  opaqueModuleFacetConfigs : NameMap OpaqueModuleFacetConfig := {}
   /--
   The names of the package's targets to build by default
   (i.e., on a bare `lake build` of the package).
   -/
   defaultTargets : Array Name := #[]
   deriving Inhabited
 
+hydrate_opaque_type OpaquePackage Package
+
 abbrev PackageSet := RBTree Package (·.name.quickCmp ·.name)
 @[inline] def PackageSet.empty : PackageSet := RBTree.empty
 
-namespace OpaquePackage
-
-unsafe def unsafeMk (pkg : Package) : OpaquePackage :=
-  unsafeCast pkg
-
-@[implementedBy unsafeMk] opaque mk (pkg : Package) : OpaquePackage
-
-instance : Coe Package OpaquePackage := ⟨mk⟩
-instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
-
-unsafe def unsafeGet (self : OpaquePackage) : Package :=
-  unsafeCast self
-
-@[implementedBy unsafeGet] opaque get (self : OpaquePackage) : Package
-
-instance : Coe OpaquePackage Package := ⟨get⟩
-
-@[simp] axiom get_mk {pkg : Package} : get (mk pkg) = pkg
-
-end OpaquePackage
-
 /--
 An alternate signature for package configurations
 that permits more dynamic configurations, but is still pure.

Diff for: Lake/Config/Workspace.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean.Util.Paths
-import Lake.Config.LeanExe
-import Lake.Config.ExternLib
+import Lake.Config.ModuleFacetConfig
 
 open System
 open Lean (LeanPaths)
@@ -23,26 +22,7 @@ structure Workspace where
   packageMap : NameMap Package := {}
   deriving Inhabited
 
-namespace OpaqueWorkspace
-
-unsafe def unsafeMk (ws : Workspace) : OpaqueWorkspace :=
-  unsafeCast ws
-
-@[implementedBy unsafeMk] opaque mk (ws : Workspace) : OpaqueWorkspace
-
-instance : Coe Workspace OpaqueWorkspace := ⟨mk⟩
-instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩
-
-unsafe def unsafeGet (self : OpaqueWorkspace) : Workspace :=
-  unsafeCast self
-
-@[implementedBy unsafeGet] opaque get (self : OpaqueWorkspace) : Workspace
-
-instance : Coe OpaqueWorkspace Workspace := ⟨get⟩
-
-@[simp] axiom get_mk {ws : Workspace} : get (mk ws) = ws
-
-end OpaqueWorkspace
+hydrate_opaque_type OpaqueWorkspace Workspace
 
 namespace Workspace
 
@@ -86,6 +66,10 @@ def findPackage? (pkg : Name) (self : Workspace) : Option Package :=
 def isLocalModule (mod : Name) (self : Workspace) : Bool :=
   self.packageMap.any fun _ pkg => pkg.isLocalModule mod
 
+/-- Check if the module is buildable by any package in the workspace. -/
+def isBuildableModule (mod : Name) (self : Workspace) : Bool :=
+  self.packageMap.any fun _ pkg => pkg.isBuildableModule mod
+
 /-- Locate the named module in the workspace (if it is local to it). -/
 def findModule? (mod : Name) (self : Workspace) : Option Module :=
   self.packageArray.findSome? (·.findModule? mod)
@@ -98,10 +82,14 @@ def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib :=
 def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe :=
   self.packageArray.findSome? fun pkg => pkg.findLeanExe? name
 
-/-- Get the workspace's external library with the given name. -/
+/-- Try to find an external library in the workspace with the given name. -/
 def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
   self.packageArray.findSome? fun pkg => pkg.findExternLib? name
 
+/-- Try to find a module facet configuration in the workspace with the given name. -/
+def findModuleFacetConfig? (name : Name) (self : Workspace) : Option ModuleFacetConfig :=
+  self.packageArray.findSome? fun pkg => pkg.findModuleFacetConfig? name
+
 /-- The `LEAN_PATH` of the workspace. -/
 def oleanPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.oleanDir)
@@ -111,6 +99,6 @@ def leanSrcPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.srcDir)
 
 /-- The `LeanPaths` of the workspace. -/
-def leanPaths (self : Workspace) : LeanPaths :=
-  let pkgs := self.packageList
-  { oleanPath := pkgs.map (·.oleanDir), srcPath := pkgs.map (·.srcDir) }
+def leanPaths (self : Workspace) : LeanPaths where
+  oleanPath := self.packageList.map (·.oleanDir)
+  srcPath := self.packageList.map (·.srcDir)

Diff for: Lake/DSL.lean

@@ -11,3 +11,4 @@ import Lake.DSL.Package
 import Lake.DSL.Script
 import Lake.DSL.Require
 import Lake.DSL.Targets
+import Lake.DSL.ModuleFacet

Diff for: Lake/DSL/Attributes.lean

@@ -32,3 +32,6 @@ initialize defaultTargetAttr : TagAttribute ←
         externLibAttr.hasTag env name
       unless valid do
         throwError "attribute `defaultTarget` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
+
+initialize moduleFacetAttr : TagAttribute ←
+  registerTagAttribute `moduleFacet "mark a definition as a Lake module facet"