fix: lake: target kinds & keys (#7763)

This PR corrects build key fetches to produce jobs with the proper data
kinds and fixes a failed coercion from key literals to targets.

src/lake/Lake/Build/Data.lean

@@ -46,6 +46,8 @@ def OptDataKind.anonymous : OptDataKind α where
   name := .anonymous
   wf h := by simp [Name.isAnonymous] at h
 
+instance : Inhabited (OptDataKind α) := ⟨OptDataKind.anonymous⟩
+
 @[inline] def OptDataKind.isAnonymous (self : OptDataKind α) : Bool :=
   self.name.isAnonymous
 
@@ -183,7 +185,7 @@ scoped macro (name := dataTypeDecl)
 
 data_type unit : Unit
 data_type bool : Bool
-data_type file_path : System.FilePath
+data_type filepath : System.FilePath
 data_type dynlib : Dynlib
 
 /-- Internal macro for declaring new facet within Lake. -/

src/lake/Lake/Build/Job/Monad.lean

@@ -134,7 +134,7 @@ Logs the job's log and throws if there was an error.
 
 /-- Apply `f` asynchronously to the job's output. -/
 protected def mapM
-  [OptDataKind β] (self : Job α) (f : α → JobM β)
+  [kind : OptDataKind β] (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) :=
   fun fetch stack store ctx trace => do
@@ -156,7 +156,7 @@ Apply `f` asynchronously to the job's output
 and asynchronously await the resulting job.
 -/
 def bindM
-  [OptDataKind β] (self : Job α) (f : α → JobM (Job β))
+  [kind : OptDataKind β] (self : Job α) (f : α → JobM (Job β))
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) :=
   fun fetch stack store ctx trace => do

src/lake/Lake/Build/Key.lean

@@ -31,6 +31,9 @@ A build key with some missing info.
 -/
 def PartialBuildKey := BuildKey
 
+/-- Cast a `BuildKey` to a `PartialBuildKey`. -/
+@[inline] def PartialBuildKey.mk (key : BuildKey) : PartialBuildKey := key
+
 /--
 Parses a `PartialBuildKey` from a `String`.
 Uses the same syntax as the `lake build` / `lake query` CLI.

src/lake/Lake/Build/Target/Fetch.lean

@@ -55,7 +55,9 @@ private def PartialBuildKey.fetchInCoreAux
       else
         let shortFacet := if shortFacet.isAnonymous then `default else shortFacet
         have facet := kind ++ shortFacet
-        let job ← (job.cast h).bindM fun data =>
+        let some cfg := (← getWorkspace).findFacetConfig? facet
+          | error s!"invalid target '{root}': unknown facet '{facet}'"
+        let job ← (job.cast h).bindM (kind := cfg.outKind) fun data =>
           fetch (.facet target kind data facet)
         return ⟨.facet target facet, cast (by simp) job⟩
 where
@@ -67,7 +69,8 @@ where
         | error s!"invalid target '{root}': package '{name}' not found in workspace"
       return pkg
 
-@[inline] private def PartialBuildKey.fetchInCore
+/-- **For internal use only.** -/
+@[inline] def PartialBuildKey.fetchInCore
   (defaultPkg : Package) (self : PartialBuildKey)
 : FetchM ((key : BuildKey) × Job (BuildData key)) :=
   fetchInCoreAux defaultPkg self self true
@@ -108,7 +111,10 @@ private def BuildKey.fetchCore
       if h : kind.isAnonymous then
         error s!"invalid target '{self}': targets of opaque data kinds do not support facets"
       else
-        (job.cast h).bindM fun data => fetch (.facet target kind data facetName)
+        let some cfg := (← getWorkspace).findFacetConfig? facetName
+          | error s!"invalid target '{root}': unknown facet '{facetName}'"
+        (job.cast h).bindM (kind := cfg.outKind) fun data =>
+          fetch (.facet target kind data facetName)
 
 @[inline] protected def BuildKey.fetch
   (self : BuildKey) [FamilyOut BuildData self α] : FetchM (Job α)

src/lake/Lake/CLI/Main.lean

@@ -381,6 +381,26 @@ protected def query : CliM PUnit := do
   let results ← ws.runBuild (querySpecs specs fmt) buildConfig
   results.forM (IO.println ·)
 
+protected def queryKind : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  let targetSpecs ← takeArgs
+  let keys ← targetSpecs.toArray.mapM fun spec =>
+    IO.ofExcept <| PartialBuildKey.parse spec
+  let buildConfig := mkBuildConfig opts
+  let r ← ws.runFetchM (cfg := buildConfig) <| keys.mapM fun key => do
+    let ⟨_, job⟩ ← key.fetchInCore ws.root
+    let kind := job.kind
+    let job ← maybeRegisterJob key.toString job.toOpaque
+    return (kind.name, job)
+  r.forM (IO.println ·.1)
+  r.forM fun (_, job) => do
+    match (← job.wait?) with
+    | some _ => pure ()
+    | none => error "build failed"
+
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
@@ -622,6 +642,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "build"               => lake.build
 | "check-build"         => lake.checkBuild
 | "query"               => lake.query
+| "query-kind"          => lake.queryKind
 | "update" | "upgrade"  => lake.update
 | "resolve-deps"        => lake.resolveDeps
 | "pack"                => lake.pack

src/lake/Lake/Config/FacetConfig.lean

@@ -16,6 +16,8 @@ structure FacetConfig (name : Name) : Type where
   kind : Name
   /-- The facet's fetch function. -/
   fetchFn : DataType kind → FetchM (Job (FacetOut name))
+  /-- The optional data kind of the facet's output. -/
+  [outKind : OptDataKind (FacetOut name)]
   /-- Is this facet compatible with the `lake build` CLI? -/
   buildable : Bool := true
   /-- Format this facet's output (e.g., for `lake query`). -/
@@ -49,11 +51,13 @@ def FacetConfig.toKind? (kind : Name) (self : FacetConfig name) : Option (KFacet
 /-- A smart constructor for facet configurations that generate jobs for the CLI. -/
 @[inline] def mkFacetJobConfig
   [FormatQuery β]
+  [outKind : OptDataKind β]
   [i : FamilyOut DataType kind α]
   [o : FamilyOut FacetOut facet β]
   (build : α → FetchM (Job β)) (buildable := true)
 : KFacetConfig kind facet where
   buildable
+  outKind := o.fam_eq ▸ outKind
   fetchFn := i.fam_eq ▸ o.fam_eq ▸ build
   format := o.fam_eq ▸ formatQuery
 

src/lake/Lake/DSL/Key.lean

@@ -14,11 +14,15 @@ open Lean
 
 namespace Lake.DSL
 
-syntax facetSuffix := ":" noWs ident
-syntax packageTargetLit := ("+" noWs)? ident
+syntax facetSuffix := atomic(":" noWs) ident
+syntax packageTargetLit := atomic("+" noWs)? ident
 
+/-- A module target key literal (with optional facet). -/
 scoped syntax:max "`+" noWs ident facetSuffix* : term
-scoped syntax:max "`@" noWs (ident)? (noWs "/" noWs packageTargetLit)? facetSuffix* : term
+
+/-- A package target key literal (with optional facet). -/
+scoped syntax:max "`@" (noWs ident)?
+  (atomic(noWs "/" noWs) packageTargetLit)? (noWs facetSuffix)* : term
 
 private def expandFacets (tgt : Term) (facets : Array Ident) : MacroM Term := do
   let facetLits := facets.map fun facet => Name.quoteFrom facet facet.getId
@@ -41,7 +45,8 @@ macro_rules
 | `(`+%$tk$mod$[:$facets]*) => withRef tk do
   let modLit := Name.quoteFrom mod mod.getId
   let tgt ← `(BuildKey.module $modLit)
-  expandFacets tgt facets
+  let key ← expandFacets tgt facets
+  `(PartialBuildKey.mk $key)
 | `(`@%$tk$(pkg?)?$[/$tgt?]?$[:$facets]*) => withRef tk do
   let pkgLit :=
     if let some pkg := pkg? then
@@ -53,4 +58,5 @@ macro_rules
       expandPackageTargetLit pkgLit tgt
     else
       `(BuildKey.package $pkgLit)
-  expandFacets tgt facets
+  let key ← expandFacets tgt facets
+  `(PartialBuildKey.mk $key)

src/lake/tests/api/keys.lean

@@ -0,0 +1,56 @@
+import Lake.DSL.Key
+import Lake.Build.Data
+import Lake.Build.Target.Basic
+open Lake DSL
+
+/-! ## Test Key Literal Representations -/
+
+/-- info: Lake.BuildKey.module `mod -/
+#guard_msgs in #eval `+mod
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.module `mod) `facet -/
+#guard_msgs in #eval `+mod:facet
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.facet (Lake.BuildKey.module `mod) `f1) `f2 -/
+#guard_msgs in #eval `+mod:f1:f2
+
+/-- info: Lake.BuildKey.package Lean.Name.anonymous -/
+#guard_msgs in #eval `@
+
+/-- info: Lake.BuildKey.package `pkg -/
+#guard_msgs in #eval `@pkg
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.package `pkg) `facet -/
+#guard_msgs in #eval `@pkg:facet
+
+/-- info: Lake.BuildKey.packageTarget `pkg `target -/
+#guard_msgs in #eval `@pkg/target
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target) `facet -/
+#guard_msgs in #eval `@pkg/target:facet
+
+/-- info: Lake.BuildKey.packageTarget `pkg `target.«_+» -/
+#guard_msgs in #eval `@pkg/+target
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target.«_+») `facet -/
+#guard_msgs in #eval `@pkg/+target:facet
+
+/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `target -/
+#guard_msgs in #eval `@/target
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `target) `facet -/
+#guard_msgs in #eval `@/target:facet
+
+/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `mod.«_+» -/
+#guard_msgs in #eval `@/+mod
+
+/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `mod.«_+») `facet -/
+#guard_msgs in #eval `@/+mod:facet
+
+/-! ## Other Tests -/
+
+-- Test syntax does not conflict with a type ascription
+def stx  := (`@pkg : PartialBuildKey)
+
+-- Test coercion to a target
+def coe : Array (Target Dynlib) := #[`@pkg/target:facet]

src/lake/tests/api/test.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LEAN=${LEAN:-lean}
+
+# Run Lean tests
+$LEAN keys.lean

src/lake/tests/kinds/.gitignore

@@ -0,0 +1 @@
+/files

src/lake/tests/kinds/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json files

src/lake/tests/kinds/lakefile.lean

@@ -0,0 +1,20 @@
+import Lake
+open System Lake DSL
+
+package test where
+  srcDir := "files"
+
+lean_lib Lib
+lean_exe exe
+
+input_file inFile where
+  path := "files" / "test.txt"
+
+input_dir inDir where
+  path := "files"
+
+target pathTarget : FilePath :=
+  return Job.pure "files"
+
+target dynlibTarget : Dynlib :=
+  return Job.pure {name := "test", path := "test.lib"}

src/lake/tests/kinds/test.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# setup directory structure
+mkdir -p files
+touch files/Lib.lean
+echo "def main : IO Unit := pure ()" > files/exe.lean
+touch files/test.txt
+
+# Test that targets have their expected data kinds
+$LAKE query-kind exe | diff -u --strip-trailing-cr <(echo filepath) -
+$LAKE query-kind Lib:static | diff -u --strip-trailing-cr <(echo filepath) -
+$LAKE query-kind Lib:shared | diff -u --strip-trailing-cr <(echo dynlib) -
+$LAKE query-kind inFile | diff -u --strip-trailing-cr <(echo filepath) -
+$LAKE query-kind inDir | diff -u --strip-trailing-cr <(echo [anonymous]) -
+$LAKE query-kind pathTarget | diff -u --strip-trailing-cr <(echo filepath) -
+$LAKE query-kind dynlibTarget | diff -u --strip-trailing-cr <(echo dynlib) -