misc: hoist facet name check to load + related bugfixes/refactors

Author: tydeu

Diff for: Lake/Build/Index.lean

@@ -15,7 +15,7 @@ The Lake build index is the complete map of Lake build keys to
 Lake build functions, which is used by Lake to build any Lake build info.
 
 This module contains the definitions used to formalize this concept,
-and it leverages the index to perform topological-based recursive builds.
+and it leverages the index to perform topologically-based recursive builds.
 -/
 
 open Std Lean
@@ -133,6 +133,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
         target ← target.mixOpaqueAsync (← depPkg.extraDep.recBuild)
     target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
   )
+
 /-!
 ## Topologically-based Recursive Build Using the Index
 -/
@@ -145,24 +146,16 @@ 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.name then
-        have : FamilyDef ModuleData facet (ActiveBuildTarget config.resultType) :=
-          ⟨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"
+      have := config.familyDef
+      mkModuleFacetBuild config.build mod
     else
       error s!"do not know how to build module facet `{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 : FamilyDef PackageData facet (ActiveBuildTarget config.resultType) :=
-          ⟨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 := (← getWorkspace).findPackageFacetConfig? facet then
+      have := config.familyDef
+      mkPackageFacetBuild config.build pkg
     else
       error s!"do not know how to build package facet `{facet}`"
   | .customTarget pkg target =>

Diff for: Lake/CLI/Build.lean

@@ -25,43 +25,47 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
     | none => throw <| CliError.unknownPackage spec
 
 open Module in
-def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : String) : Except CliError OpaqueTarget :=
-  if facet.isEmpty || facet == "bin"  then
+def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : WfName) : Except CliError OpaqueTarget :=
+  if facet.isAnonymous || facet == &`bin  then
     return mod.facetTarget leanBinFacet
-  else if facet == "ilean" then
+  else if facet == &`ilean then
     return mod.facetTarget ileanFacet
-  else if facet == "olean" then
+  else if facet == &`olean then
     return mod.facetTarget oleanFacet
-  else if facet == "c" then
+  else if facet == &`c then
     return mod.facetTarget cFacet
-  else if facet == "o" then
+  else if facet == &`o then
     return mod.facetTarget oFacet
-  else if facet == "dynlib" then
+  else if facet == &`dynlib then
     return mod.facetTarget dynlibFacet
   else if let some config := ws.findModuleFacetConfig? facet then
-    return mod.facetTarget config.name
+    if let some (.up ⟨_, h⟩) := config.result_eq_target? then
+      have := config.familyDefTarget h
+      return mod.facetTarget facet
+    else
+      throw <| CliError.nonTargetFacet "module" facet
   else
     throw <| CliError.unknownFacet "module" facet
 
-def resolveLibTarget (lib : LeanLib) (facet : String) : Except CliError OpaqueTarget :=
-  if facet.isEmpty || facet == "lean" || facet == "oleans" then
+def resolveLibTarget (lib : LeanLib) (facet : WfName) : Except CliError OpaqueTarget :=
+  if facet.isAnonymous || facet == &`lean then
     return lib.leanTarget
-  else if facet == "static" then
+  else if facet == &`static then
     return lib.staticLibTarget |>.withoutInfo
-  else if facet == "shared" then
+  else if facet == &`shared then
     return lib.sharedLibTarget |>.withoutInfo
   else
     throw <| CliError.unknownFacet "library" facet
 
-def resolveExeTarget (exe : LeanExe) (facet : String) : Except CliError OpaqueTarget :=
-  if facet.isEmpty || facet == "exe" then
+def resolveExeTarget (exe : LeanExe) (facet : WfName) : Except CliError OpaqueTarget :=
+  if facet.isAnonymous || facet == &`exe then
     return exe.target |>.withoutInfo
   else
     throw <| CliError.unknownFacet "executable" facet
 
-def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
+def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : WfName) (facet : WfName) : Except CliError OpaqueTarget :=
   if let some config := pkg.findTargetConfig? target then
-    if !facet.isEmpty then
+    if !facet.isAnonymous then
       throw <| CliError.invalidFacet target facet
     else if h : pkg.name = config.package then
       have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) :=
@@ -72,7 +76,7 @@ def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (fac
   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
+    if facet.isAnonymous then
       return lib.target.withoutInfo
     else
       throw <| CliError.invalidFacet target facet
@@ -88,27 +92,31 @@ def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliErr
     return pkg.defaultTarget
   else
     return Target.collectOpaqueArray <| ←
-      pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · "")
+      pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous)
 
-def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : String) : Except CliError OpaqueTarget :=
-  if facet.isEmpty then
+def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : WfName) : Except CliError OpaqueTarget :=
+  if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
-  else if facet == "exe" || facet == "bin" then
+  else if facet == &`exe then
     return pkg.exeTarget.withoutInfo
-  else if facet == "staticLib" then
+  else if facet == &`staticLib then
     return pkg.staticLibTarget.withoutInfo
-  else if facet == "sharedLib" then
+  else if facet == &`sharedLib then
     return pkg.sharedLibTarget.withoutInfo
-  else if facet == "leanLib" || facet == "oleans" then
+  else if facet == &`leanLib then
     return pkg.leanLibTarget.withoutInfo
   else if let some config := ws.findPackageFacetConfig? facet then
-    return pkg.facet config.name |>.target
+    if let some (.up ⟨_, h⟩) := config.result_eq_target? then
+      have := config.familyDefTarget h
+      return pkg.facet facet |>.target
+    else
+      throw <| CliError.nonTargetFacet "package" facet
   else
     throw <| CliError.unknownFacet "package" facet
 
-def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
+def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : WfName) : Except CliError OpaqueTarget :=
   if let some (pkg, config) := ws.findTargetConfig? target then
-    if !facet.isEmpty then
+    if !facet.isAnonymous then
       throw <| CliError.invalidFacet config.name facet
     else if h : pkg.name = config.package then
       have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) :=
@@ -119,7 +127,7 @@ def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : String) :
   else if let some exe := ws.findLeanExe? target then
     resolveExeTarget exe facet
   else if let some lib := ws.findExternLib? target then
-    if facet.isEmpty then
+    if facet.isAnonymous then
       return lib.target.withoutInfo
     else
       throw <| CliError.invalidFacet target facet
@@ -132,7 +140,7 @@ def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : String) :
   else
     throw <| CliError.unknownTarget target
 
-def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Except CliError OpaqueTarget := do
+def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : WfName) : Except CliError OpaqueTarget := do
   match spec.splitOn "/" with
   | [spec] =>
     if spec.isEmpty then
@@ -158,15 +166,15 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep
       else
         throw <| CliError.unknownModule mod
     else
-      resolveTargetInPackage ws pkg spec facet
+      resolveTargetInPackage ws pkg (WfName.ofName targetSpec) facet
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 
 def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError OpaqueTarget := do
   match spec.splitOn ":" with
   | [spec] =>
-    resolveTargetBaseSpec ws spec
+    resolveTargetBaseSpec ws spec .anonymous
   | [rootSpec, facet] =>
-    resolveTargetBaseSpec ws rootSpec facet
+    resolveTargetBaseSpec ws rootSpec (WfName.ofString facet)
   | _ =>
     throw <| CliError.invalidTargetSpec spec ':'

Diff for: Lake/CLI/Error.lean

@@ -21,13 +21,14 @@ inductive CliError
 /- Build CLI Errors -/
 | unknownModule (mod : Name)
 | unknownPackage (spec : String)
-| unknownFacet (type facet : String)
+| unknownFacet (type : String) (facet : Name)
 | unknownTarget (target : Name)
 | missingModule (pkg : Name) (mod : Name)
 | missingTarget (pkg : Name) (spec : String)
 | badTarget (pkg target cfgPkg cfgName : Name)
+| nonTargetFacet (type : String) (facet : Name)
 | invalidTargetSpec (spec : String) (tooMany : Char)
-| invalidFacet (target : Name) (facet : String)
+| invalidFacet (target : Name) (facet : Name)
 /- Script CLI Error -/
 | unknownScript (script : String)
 | missingScriptDoc (script : String)
@@ -51,13 +52,14 @@ def toString : CliError → String
 | unknownTemplate spec    => s!"unknown package template `{spec}`"
 | unknownModule mod       => s!"unknown module `{mod.toString false}`"
 | unknownPackage spec     => s!"unknown package `{spec}`"
-| unknownFacet ty f       => s!"unknown {ty} facet `{f}`"
+| unknownFacet ty f       => s!"unknown {ty} facet `{f.toString false}`"
 | unknownTarget t         => s!"unknown target `{t.toString false}`"
 | missingModule pkg mod   => s!"package '{pkg.toString false}' has no module '{mod.toString false}'"
 | missingTarget pkg spec  => s!"package '{pkg.toString false}' has no target '{spec}'"
 | badTarget p t p' t'     => s!"target registered as `{p.toString false}/{t.toString false}` but configured as `{p'.toString false}/{t'.toString false}` "
+| nonTargetFacet t f      => s!"{t} facet `{f.toString false}` is not a buildable target"
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
-| invalidFacet t f        => s!"invalid facet `{f}`; target {t.toString false} has no facets"
+| invalidFacet t f        => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
 | unknownScript s         => s!"unknown script {s}"
 | missingScriptDoc s      => s!"no documentation provided for `{s}`"
 | invalidScriptSpec s     => s!"invalid script spec '{s}' (too many '/')"

Diff for: Lake/Config/FacetConfig.lean

@@ -0,0 +1,83 @@
+/-
+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 facet's declarative configuration. -/
+structure FacetConfig (DataFam : WfName → Type u) (BuildFn : Type u → Type v) (name : WfName) where
+  /-- The type of the target's build result. -/
+  resultType : Type u
+  /-- The facet's build function. -/
+  build : BuildFn resultType
+  /-- Proof that the facet's build result data type is properly registered. -/
+  data_eq_result : DataFam name = resultType
+   /-- Is this facet a buildable target? -/
+  result_eq_target? : Option <| PLift <| PSigma fun α => resultType = ActiveBuildTarget α
+
+instance [(α : Type u) → Inhabited (BuildFn α)] : Inhabited (FacetConfig DataFam BuildFn name) := ⟨{
+  resultType := DataFam name
+  build := default
+  data_eq_result := rfl
+  result_eq_target? := none
+}⟩
+
+abbrev FacetBuildFn (ι) :=
+  fun resultType => {m : Type → Type} →
+    [Monad m] → [MonadLift BuildM m] → [MonadBuildStore m] →
+    ι → IndexT m resultType
+
+instance : Inhabited (FacetBuildFn ι α) :=
+  ⟨fun _ => liftM (m := BuildM) failure⟩
+
+namespace FacetConfig
+
+protected def name (_ : FacetConfig DataFam BuildFn name) :=
+  name
+
+instance (cfg : FacetConfig Fam Fn name) :
+  FamilyDef Fam cfg.name cfg.resultType := ⟨cfg.data_eq_result⟩
+
+def familyDef (cfg : FacetConfig Fam Fn name) : FamilyDef Fam name cfg.resultType :=
+  ⟨cfg.data_eq_result⟩
+
+def familyDefTarget (cfg : FacetConfig Fam Fn name)
+(h : cfg.resultType = ActiveBuildTarget α) : FamilyDef Fam name (ActiveBuildTarget α) :=
+  ⟨h ▸ cfg.data_eq_result⟩
+
+end FacetConfig
+
+/-- A dependently typed configuration based on its registered name. -/
+structure NamedConfigDecl (β : WfName → Type u) where
+  name : WfName
+  config : β name
+
+--------------------------------------------------------------------------------
+
+/-- A module facet's declarative configuration. -/
+abbrev ModuleFacetConfig := FacetConfig ModuleData (FacetBuildFn Module)
+hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig name
+
+/-- Try to find a module facet configuration in the package with the given name . -/
+def Package.findModuleFacetConfig? (name : WfName) (self : Package) : Option (ModuleFacetConfig name) :=
+  self.opaqueModuleFacetConfigs.find? name |>.map (·.get)
+
+/-- A module facet declaration from a configuration file. -/
+abbrev ModuleFacetDecl := NamedConfigDecl ModuleFacetConfig
+
+--------------------------------------------------------------------------------
+
+/-- A package facet's declarative configuration. -/
+abbrev PackageFacetConfig := FacetConfig PackageData (FacetBuildFn Package)
+hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig name
+
+/-- Try to find a package configuration in the package with the given name . -/
+def Package.findPackageFacetConfig? (name : WfName) (self : Package) : Option (PackageFacetConfig name) :=
+  self.opaquePackageFacetConfigs.find? name |>.map (·.get)
+
+/-- A package facet declaration from a configuration file. -/
+abbrev PackageFacetDecl := NamedConfigDecl PackageFacetConfig

Diff for: Lake/Config/Glob.lean

@@ -27,9 +27,9 @@ partial def forEachNoduleIn [Monad m] [MonadLiftT IO m]
 (dir : FilePath) (f : WfName → m PUnit) : m PUnit := do
   for entry in (← dir.readDir) do
     if (← liftM (m := IO) <| entry.path.isDir) then
-      f entry.fileName
+      f <| WfName.ofString <| entry.fileName
     else if entry.path.extension == some "lean" then
-      f <| FilePath.withExtension entry.fileName "" |>.toString
+      f <| WfName.ofString <| FilePath.withExtension entry.fileName "" |>.toString
 
 namespace Glob