fix: lake: facet names in unknown facet errors (#12261)

This PR fixes a bug in Lake where the facet names printed in unknown
facet errors would contain the internal facet kind.

src/lake/Lake/Build/Infos.lean

@@ -278,6 +278,10 @@ public abbrev LeanLib.facet (facet : Name) (self : LeanLib) : BuildInfo :=
 
 namespace LeanLib
 
+@[inherit_doc defaultFacet]
+public abbrev default (self : LeanLib) : BuildInfo :=
+  self.facetCore defaultFacet
+
 @[inherit_doc modulesFacet]
 public abbrev modules (self : LeanLib) : BuildInfo :=
   self.facetCore modulesFacet
@@ -313,7 +317,7 @@ It is the user's obligation to ensure the facet in question is the executable fa
 public abbrev LeanExe.facetCore (facet : Name) (self : LeanExe) : BuildInfo :=
   .facet self.key facetKind (toFamily self) facet
 
-/-- Build info of the Lean executable. -/
+@[inherit_doc exeFacet]
 public abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=
   self.facetCore LeanExe.exeFacet
 
@@ -326,15 +330,15 @@ It is the user's obligation to ensure the facet in question is an external libra
 public abbrev ExternLib.facetCore (facet : Name) (self : ExternLib) : BuildInfo :=
   .facet self.key facetKind (toFamily self) facet
 
-/-- Build info of the external library's static binary. -/
+@[inherit_doc staticFacet]
 public abbrev ExternLib.static (self : ExternLib) : BuildInfo :=
   self.facetCore ExternLib.staticFacet
 
-/-- Build info of the external library's shared binary. -/
+@[inherit_doc sharedFacet]
 public abbrev ExternLib.shared (self : ExternLib) : BuildInfo :=
   self.facetCore ExternLib.sharedFacet
 
-/-- Build info of the external library's dynlib. -/
+@[inherit_doc dynlibFacet]
 public abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo :=
   self.facetCore ExternLib.dynlibFacet
 
@@ -347,7 +351,7 @@ It is the user's obligation to ensure the facet in question is an external libra
 public abbrev InputFile.facetCore (facet : Name) (self : InputFile) : BuildInfo :=
   .facet self.key facetKind (toFamily self) facet
 
-/-- Build info of the input file's default facet. -/
+@[inherit_doc defaultFacet]
 public abbrev InputFile.default (self : InputFile) : BuildInfo :=
   self.facetCore InputFile.defaultFacet
 
@@ -358,6 +362,6 @@ It is the user's obligation to ensure the facet in question is an external libra
 public abbrev InputDir.facetCore (facet : Name) (self : InputDir) : BuildInfo :=
   .facet self.key facetKind (toFamily self) facet
 
-/-- Build info of the input directory's default facet. -/
+@[inherit_doc defaultFacet]
 public abbrev InputDir.default (self : InputDir) : BuildInfo :=
   self.facetCore InputDir.defaultFacet

src/lake/Lake/Build/Targets.lean

@@ -79,6 +79,14 @@ public def Module.fetchFacetJob (name : Name) (self : Module) : FetchM OpaqueJob
   (self : LeanLibDecl) [Monad m] [MonadError m] [MonadLake m] : m LeanLib
 := KConfigDecl.get self
 
+/-- Fetch the build of the default facets of the library -/
+@[inline] public protected def LeanLib.fetch (self : LeanLib) : FetchM (Job Unit) :=
+  self.default.fetch
+
+/-- Fetch the build of the default facets of the library -/
+@[inline] public protected def LeanLibDecl.fetch (self : LeanLibDecl) : FetchM (Job Unit) := do
+  (← self.get).fetch
+
 /-- Fetch the build result of a library facet. -/
 @[inline] public protected def LibraryFacetDecl.fetch
   (lib : LeanLib) (self : LibraryFacetDecl) [FamilyOut FacetOut self.name α]
@@ -97,17 +105,17 @@ public def LeanLib.fetchFacetJob
 := KConfigDecl.get self
 
 /-- Fetch the build of the Lean executable. -/
-@[inline] public def LeanExe.fetch (self : LeanExe) : FetchM (Job FilePath) :=
+@[inline] public protected def LeanExe.fetch (self : LeanExe) : FetchM (Job FilePath) :=
   self.exe.fetch
 
 /-- Fetch the build of the Lean executable. -/
-@[inline] public def LeanExeDecl.fetch (self : LeanExeDecl) : FetchM (Job FilePath) := do
+@[inline] public protected def LeanExeDecl.fetch (self : LeanExeDecl) : FetchM (Job FilePath) := do
   (← self.get).fetch
 
 /-! ## Input File / Directory Targets -/
 
 /-- Fetch the input file. -/
-@[inline] public def InputFile.fetch (self : InputFile) : FetchM (Job FilePath) :=
+@[inline] public protected def InputFile.fetch (self : InputFile) : FetchM (Job FilePath) :=
   self.default.fetch
 
 /-- Get the input file in the workspace corresponding to this configuration. -/
@@ -116,11 +124,11 @@ public def LeanLib.fetchFacetJob
 := KConfigDecl.get self
 
 /-- Fetch the input file. -/
-@[inline] public def InputFileDecl.fetch (self : InputFileDecl) : FetchM (Job FilePath) := do
+@[inline] public protected def InputFileDecl.fetch (self : InputFileDecl) : FetchM (Job FilePath) := do
   (← self.get).default.fetch
 
 /-- Fetch the files in the input directory. -/
-@[inline] public def InputDir.fetch (self : InputDir) : FetchM (Job (Array FilePath)) :=
+@[inline] public protected def InputDir.fetch (self : InputDir) : FetchM (Job (Array FilePath)) :=
   self.default.fetch
 
 /-- Get the input directory in the workspace corresponding to this configuration. -/
@@ -129,5 +137,5 @@ public def LeanLib.fetchFacetJob
 := KConfigDecl.get self
 
 /-- Fetch the files in the input directory. -/
-@[inline] public def InputDirDecl.fetch (self : InputDirDecl) : FetchM (Job (Array FilePath)) := do
+@[inline] public protected def InputDirDecl.fetch (self : InputDirDecl) : FetchM (Job (Array FilePath)) := do
   (← self.get).default.fetch

src/lake/Lake/CLI/Actions.lean

@@ -83,12 +83,8 @@ public def Package.test
   else if let some lib := pkg.findLeanLib? driver.toName then
     unless cfgArgs.isEmpty ∧ args.isEmpty do
       error s!"{pkg.prettyName}: arguments cannot be passed to a library test driver"
-    match resolveLibTarget (← getWorkspace) lib with
-    | .ok specs =>
-      runBuild (buildSpecs specs) {buildConfig with out := .stdout}
-      return 0
-    | .error e =>
-      error s!"{pkg.prettyName}: invalid test driver: {e}"
+    runBuild lib.fetch {buildConfig with out := .stdout}
+    return 0
   else
     error s!"{pkg.prettyName}: invalid test driver: unknown script, executable, or library '{driver}'"
 

src/lake/Lake/CLI/Build.lean

@@ -68,15 +68,13 @@ public def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError P
     | some pkg => return pkg
     | none => throw <| CliError.unknownPackage spec
 
-open Module in
 def resolveModuleTarget
   (ws : Workspace) (mod : Module) (facet : Name)
 : Except CliError BuildSpec :=
   if facet.isAnonymous then
     return mkBuildSpec mod.leanArts
   else
-    let facet := Module.facetKind ++ facet
-    if let some config := ws.findModuleFacetConfig? facet then do
+    if let some config := ws.findModuleFacetConfig? (Module.facetKind ++ facet) then do
       return mkConfigBuildSpec (mod.facetCore config.name) config.toFacetConfig rfl
     else
       throw <| CliError.unknownFacet "module" facet
@@ -105,39 +103,6 @@ def resolveConfigDeclTarget
     else
       throw <| CliError.unknownFacet decl.kind.toString facet
 
-/-- **For internal use only.** -/
-public def resolveLibTarget
-  (ws : Workspace) (lib : LeanLib) (facet : Name := .anonymous)
-: Except CliError (Array BuildSpec) :=
-  if facet.isAnonymous then
-    lib.defaultFacets.mapM (resolveFacet ·)
-  else
-    Array.singleton <$> resolveFacet (LeanLib.facetKind ++ facet)
-where
-  resolveFacet facet :=
-    if let some config := ws.findLibraryFacetConfig? facet then do
-      return mkConfigBuildSpec (lib.facetCore config.name) config.toFacetConfig rfl
-    else
-      throw <| CliError.unknownFacet "library" facet
-
-def resolveExeTarget
-  (exe : LeanExe) (facet : Name)
-: Except CliError BuildSpec :=
-  if facet.isAnonymous || facet == `exe then
-    return mkBuildSpec exe.exe
-  else
-    throw <| CliError.unknownFacet "executable" facet
-
-def resolveExternLibTarget
-  (lib : ExternLib) (facet : Name)
-: Except CliError BuildSpec :=
-  if facet.isAnonymous || facet = `static then
-    return mkBuildSpec lib.static
-  else if facet = `shared then
-    return mkBuildSpec lib.shared
-  else
-    throw <| CliError.unknownFacet "external library" facet
-
 def resolveTargetInPackage
   (ws : Workspace) (pkg : Package) (target facet : Name)
 : Except CliError (Array BuildSpec) := do
@@ -159,8 +124,7 @@ def resolvePackageTarget
   if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
   else
-    let facet := Package.facetKind ++ facet
-    if let some config := ws.findPackageFacetConfig? facet then do
+    if let some config := ws.findPackageFacetConfig? (Package.facetKind ++ facet) then do
       return #[mkConfigBuildSpec (pkg.facetCore config.name) config.toFacetConfig rfl]
     else
       throw <| CliError.unknownFacet "package" facet

tests/lake/tests/targets/clean.sh

@@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json produced.out

tests/lake/tests/targets/test.sh

@@ -1,28 +1,18 @@
 #!/usr/bin/env bash
-set -exo pipefail
+source ../common.sh
 
 # Prevent MSYS2 from automatically transforming path-like targets
 [ "$OSTYPE" == "cygwin" -o "$OSTYPE" == "msys" ] && export MSYS2_ARG_CONV_EXCL=*
 
-LAKE=${LAKE:-../../.lake/build/bin/lake}
-
-if [ "$OS" = Windows_NT ]; then
-LIB_PREFIX=
-SHARED_LIB_EXT=dll
-elif [ "`uname`" = Darwin ]; then
-LIB_PREFIX=lib
-SHARED_LIB_EXT=dylib
-else
-LIB_PREFIX=lib
-SHARED_LIB_EXT=so
-fi
-
 PKG=targets
 
 ./clean.sh
 
-# Test error on nonexistent facet
-$LAKE build targets:noexistent && exit 1 || true
+# Test errors on nonexistent facets
+test_err 'unknown package facet `bogus`' build targets:bogus
+test_err 'unknown lean_lib facet `bogus`' build Foo:bogus
+test_err 'unknown module facet `bogus`'  build +Foo:bogus
+test_err 'unknown lean_exe facet `bogus`' build a:bogus
 
 # Test custom targets and package, library, and module facets
 diff_out() {
@@ -126,3 +116,6 @@ test -f .lake/build/ir/Bar.c.o.export
 $LAKE build -v src/a.lean
 test -f .lake/build/lib/lean/a.olean
 test ! -f .lake/build/bin/a
+
+# Cleanup
+rm -f produced.out