feat: lake query (#6323)

This PR adds a new Lake CLI command, `lake query`, that both builds
targets and outputs their results. It can produce raw text or JSON
-formatted output (with `--json` / `-J`).

This PR removes the `lean.` prefix from the module import facets (for
ease-of-use in the `lake query` CLII). It also renames the package
`deps` facet, `transDeps`. The new `deps` facet just returns the
package's direct dependencies.

src/lake/Lake/Build/Executable.lean

@@ -27,7 +27,7 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
   for mod in imports do
     for facet in mod.nativeFacets self.supportInterpreter do
       linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
-  let deps := (← (← fetch <| self.pkg.facet `deps).await).push self.pkg
+  let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch
   buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean

src/lake/Lake/Build/Facets.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 prelude
 import Lake.Build.Data
 import Lake.Build.Job.Basic
+import Lake.Config.OutFormat
 
 /-!
 # Simple Builtin Facet Declarations
@@ -16,9 +17,10 @@ definitions (e.g., `Module`), and some of the facets here are used in said
 definitions.
 -/
 
+open System
+open Lean hiding SearchPath
+
 namespace Lake
-open Lean (Name)
-open System (SearchPath FilePath)
 
 /-- A dynamic/shared library for linking. -/
 structure Dynlib where
@@ -31,6 +33,9 @@ structure Dynlib where
 def Dynlib.dir? (self : Dynlib) : Option FilePath :=
   self.path.parent
 
+instance : ToText Dynlib := ⟨(·.path.toString)⟩
+instance : ToJson Dynlib := ⟨(·.path.toString)⟩
+
 /-! ## Module Facets -/
 
 /-- A module facet name along with proof of its data type. -/

src/lake/Lake/Build/Index.lean

@@ -50,24 +50,24 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
 def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-    config.build mod
+    config.fetchFn mod
   else
-    error s!"do not know how to build module facet `{facet}`"
+    error s!"do not know how to fetch module facet `{facet}`"
 | .packageFacet pkg facet => do
   if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-    config.build pkg
+    config.fetchFn pkg
   else
-    error s!"do not know how to build package facet `{facet}`"
+    error s!"do not know how to fetch package facet `{facet}`"
 | .target pkg target =>
   if let some config := pkg.findTargetConfig? target then
-    config.build pkg
+    config.fetchFn pkg
   else
-    error s!"could not build `{target}` of `{pkg.name}` -- target not found"
+    error s!"could not fetch `{target}` of `{pkg.name}` -- target not found"
 | .libraryFacet lib facet => do
   if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
-    config.build lib
+    config.fetchFn lib
   else
-    error s!"do not know how to build library facet `{facet}`"
+    error s!"do not know how to fetch library facet `{facet}`"
 | .leanExe exe =>
   mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
 | .staticExternLib lib =>

src/lake/Lake/Build/Info.lean

@@ -124,16 +124,16 @@ definitions.
 -/
 
 /-- The direct local imports of the Lean module. -/
-abbrev Module.importsFacet := `lean.imports
-module_data lean.imports : Array Module
+abbrev Module.importsFacet := `imports
+module_data imports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
-abbrev Module.transImportsFacet := `lean.transImports
-module_data lean.transImports : Array Module
+abbrev Module.transImportsFacet := `transImports
+module_data transImports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
-abbrev Module.precompileImportsFacet := `lean.precompileImports
-module_data lean.precompileImports : Array Module
+abbrev Module.precompileImportsFacet := `precompileImports
+module_data precompileImports : Array Module
 
 /-- Shared library for `--load-dynlib`. -/
 abbrev Module.dynlibFacet := `dynlib
@@ -143,10 +143,13 @@ module_data dynlib : Dynlib
 abbrev LeanLib.modulesFacet := `modules
 library_data modules : Array Module
 
-/-- The package's complete array of transitive dependencies. -/
+/-- The package's array of dependencies. -/
 abbrev Package.depsFacet := `deps
 package_data deps : Array Package
 
+/-- The package's complete array of transitive dependencies. -/
+abbrev Package.transDepsFacet := `transDeps
+package_data transDeps : Array Package
 
 /-!
 ### Facet Build Info Helper Constructors
@@ -252,6 +255,14 @@ abbrev Package.optRelease := @optGitHubRelease
 abbrev Package.extraDep (self : Package) : BuildInfo :=
   self.facet extraDepFacet
 
+@[inherit_doc depsFacet]
+abbrev Package.deps (self : Package) : BuildInfo :=
+  self.facet depsFacet
+
+@[inherit_doc transDepsFacet]
+abbrev Package.transDeps (self : Package) : BuildInfo :=
+  self.facet transDepsFacet
+
 /-- Build info for a custom package target. -/
 abbrev Package.target (target : Name) (self : Package) : BuildInfo :=
   .target self target

src/lake/Lake/Build/Library.lean

@@ -41,7 +41,7 @@ where
 
 /-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
 def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=
-  mkFacetJobConfig LeanLib.recCollectLocalModules
+  mkFacetJobConfig LeanLib.recCollectLocalModules (buildable := false)
 
 protected def LeanLib.recBuildLean
 (self : LeanLib) : FetchM (Job Unit) := do

src/lake/Lake/Build/Module.lean

@@ -40,7 +40,7 @@ def Module.recParseImports (mod : Module) : FetchM (Job (Array Module)) := Job.a
 
 /-- The `ModuleFacetConfig` for the builtin `importsFacet`. -/
 def Module.importsFacetConfig : ModuleFacetConfig importsFacet :=
-  mkFacetJobConfig recParseImports
+  mkFacetJobConfig recParseImports (buildable := false)
 
 structure ModuleImportData where
   module : Module
@@ -80,7 +80,7 @@ def Module.recComputeTransImports (mod : Module) : FetchM (Job (Array Module)) :
 
 /-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/
 def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet :=
-  mkFacetJobConfig recComputeTransImports
+  mkFacetJobConfig recComputeTransImports (buildable := false)
 
 def computePrecompileImportsAux
   (leanFile : FilePath) (imports : Array Module)
@@ -97,7 +97,7 @@ def Module.recComputePrecompileImports (mod : Module) : FetchM (Job (Array Modul
 
 /-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/
 def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
-  mkFacetJobConfig recComputePrecompileImports
+  mkFacetJobConfig recComputePrecompileImports (buildable := false)
 
 /--
 Recursively build a module's dependencies, including:

src/lake/Lake/Build/Package.lean

@@ -19,18 +19,30 @@ open System
 namespace Lake
 open Lean (Name)
 
+/-- Fetch the package's direct dependencies. -/
+def Package.recFetchDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
+  (pure ·) <$> self.depConfigs.mapM fun cfg => do
+    let some dep ← findPackage? cfg.name
+      | error s!"{self.name}: package not found for dependency '{cfg.name}' \
+        (this is likely a bug in Lake)"
+    return dep
+
+/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
+def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
+  mkFacetJobConfig recFetchDeps (buildable := false)
+
 /-- Compute a topological ordering of the package's transitive dependencies. -/
-def Package.recComputeDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
+def Package.recComputeTransDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
   (pure ·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do
     let some dep ← findPackage? cfg.name
       | error s!"{self.name}: package not found for dependency '{cfg.name}' \
         (this is likely a bug in Lake)"
-    let depDeps ← (← fetch <| dep.facet `deps).await
+    let depDeps ← (← fetch <| dep.facet `transDeps).await
     return depDeps.foldl (·.insert ·) deps |>.insert dep
 
-/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
-def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
-  mkFacetJobConfig recComputeDeps
+/-- The `PackageFacetConfig` for the builtin `transDepsFacet`. -/
+def Package.transDepsFacetConfig : PackageFacetConfig transDepsFacet :=
+  mkFacetJobConfig recComputeTransDeps (buildable := false)
 
 /--
 Tries to download and unpack the package's cached build archive
@@ -234,6 +246,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
 def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
+  |>.insert transDepsFacet transDepsFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
   |>.insert optBuildCacheFacet optBuildCacheFacetConfig
   |>.insert buildCacheFacet buildCacheFacetConfig

src/lake/Lake/CLI/Build.lean

@@ -8,35 +8,47 @@ import Lake.Config.Monad
 import Lake.Build.Job
 import Lake.CLI.Error
 
+open System Lean
+
 namespace Lake
-open Lean (Name)
 
 /-! ## Build Target Specifiers -/
 
 structure BuildSpec where
   info : BuildInfo
-
-@[inline] def BuildData.toJob
-  [FamilyOut BuildData k (Job α)] (data : BuildData k)
-: OpaqueJob :=
-  ofFamily data |>.toOpaque
+  buildable := true
+  format : OutFormat → BuildData info.key → String := nullFormat
 
 @[inline] def mkBuildSpec
-  (info : BuildInfo) [FamilyOut BuildData info.key α]
-: BuildSpec := {info}
+  (info : BuildInfo) [FormatQuery α] [h : FamilyOut BuildData info.key α]
+: BuildSpec where
+  info
+  buildable := true
+  format := h.family_key_eq_type ▸ formatQuery
 
 @[inline] def mkConfigBuildSpec
-  (facetType : String) (info : BuildInfo) (config : FacetConfig Fam ι facet)
-: Except CliError BuildSpec := do
-  unless config.cli do
-    throw <| CliError.nonCliFacet facetType facet
-  return {info}
+  (info : BuildInfo)
+  (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+: BuildSpec where
+  info
+  buildable := config.buildable
+  format := h ▸ config.format
 
-@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM OpaqueJob := do
-  maybeRegisterJob (self.info.key.toSimpleString) (← self.info.fetch)
+@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (Job (BuildData self.info.key)) := do
+  maybeRegisterJob self.info.key.toSimpleString (← self.info.fetch)
+
+@[inline] protected def BuildSpec.build (self : BuildSpec) : FetchM OpaqueJob := do
+  return (← self.fetch).toOpaque
+
+@[inline] protected def BuildSpec.query (self : BuildSpec) (fmt : OutFormat) : FetchM (Job String) := do
+  maybeRegisterJob self.info.key.toSimpleString =<< do
+    return (← self.info.fetch).map (self.format fmt)
 
 def buildSpecs (specs : Array BuildSpec) : FetchM (Job Unit) := do
-  return .mixArray (← specs.mapM (·.fetch))
+  return Job.mixArray (← specs.mapM (·.build))
+
+def querySpecs (specs : Array BuildSpec) (fmt : OutFormat) : FetchM (Job (Array String)) := do
+  return Job.collectArray (← specs.mapM (·.query fmt))
 
 /-! ## Parsing CLI Build Target Specifiers -/
 
@@ -50,12 +62,12 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
 
 open Module in
 def resolveModuleTarget
-  (ws : Workspace) (mod : Module) (facet : Name := .anonymous)
+  (ws : Workspace) (mod : Module) (facet : Name)
 : Except CliError BuildSpec :=
   if facet.isAnonymous then
-    return mkBuildSpec <| mod.facet leanArtsFacet
+    return mkBuildSpec (mod.facet leanArtsFacet)
   else if let some config := ws.findModuleFacetConfig? facet then do
-    mkConfigBuildSpec "module" (mod.facet facet) config
+    return mkConfigBuildSpec (mod.facet facet) config rfl
   else
     throw <| CliError.unknownFacet "module" facet
 
@@ -69,17 +81,21 @@ def resolveLibTarget
 where
   resolveFacet facet :=
     if let some config := ws.findLibraryFacetConfig? facet then do
-      mkConfigBuildSpec "library" (lib.facet facet) config
+      return mkConfigBuildSpec (lib.facet facet) config rfl
     else
       throw <| CliError.unknownFacet "library" facet
 
-def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError BuildSpec :=
+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 :=
+def resolveExternLibTarget
+  (lib : ExternLib) (facet : Name)
+: Except CliError BuildSpec :=
   if facet.isAnonymous || facet = `static then
     return mkBuildSpec lib.static
   else if facet = `shared then
@@ -94,10 +110,11 @@ def resolveCustomTarget
   if !facet.isAnonymous then
     throw <| CliError.invalidFacet name facet
   else do
-    return {info := pkg.target name}
+    return {info := pkg.target name, format := config.format}
 
-def resolveTargetInPackage (ws : Workspace)
-(pkg : Package) (target facet : Name) : Except CliError (Array BuildSpec) :=
+def resolveTargetInPackage
+  (ws : Workspace) (pkg : Package) (target facet : Name)
+: Except CliError (Array BuildSpec) :=
   if let some config := pkg.findTargetConfig? target then
     Array.singleton <$> resolveCustomTarget pkg target facet config
   else if let some exe := pkg.findLeanExe? target then
@@ -111,19 +128,24 @@ def resolveTargetInPackage (ws : Workspace)
   else
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
-def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) :=
+def resolveDefaultPackageTarget
+  (ws : Workspace) (pkg : Package)
+: Except CliError (Array BuildSpec) :=
   pkg.defaultTargets.flatMapM (resolveTargetInPackage ws pkg · .anonymous)
 
-def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) :=
+def resolvePackageTarget
+  (ws : Workspace) (pkg : Package) (facet : Name)
+: Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
   else if let some config := ws.findPackageFacetConfig? facet then do
-    Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config
+    return #[mkConfigBuildSpec (pkg.facet facet) config rfl]
   else
     throw <| CliError.unknownFacet "package" facet
 
-def resolveTargetInWorkspace (ws : Workspace)
-(target : Name) (facet : Name) : Except CliError (Array BuildSpec) :=
+def resolveTargetInWorkspace
+  (ws : Workspace) (target : Name) (facet : Name)
+: Except CliError (Array BuildSpec) :=
   if let some ⟨pkg, config⟩ := ws.findTargetConfig? target then
     Array.singleton <$> resolveCustomTarget pkg target facet config
   else if let some exe := ws.findLeanExe? target then
@@ -140,7 +162,8 @@ def resolveTargetInWorkspace (ws : Workspace)
     throw <| CliError.unknownTarget target
 
 def resolveTargetBaseSpec
-(ws : Workspace) (spec : String) (facet : Name) : Except CliError (Array BuildSpec) := do
+  (ws : Workspace) (spec : String) (facet : Name)
+: Except CliError (Array BuildSpec) := do
   match spec.splitOn "/" with
   | [spec] =>
     if spec.isEmpty then
@@ -172,7 +195,9 @@ def resolveTargetBaseSpec
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 
-def parseExeTargetSpec (ws : Workspace) (spec : String) : Except CliError LeanExe := do
+def parseExeTargetSpec
+  (ws : Workspace) (spec : String)
+: Except CliError LeanExe := do
   match spec.splitOn "/" with
   | [targetSpec] =>
     let targetName := stringToLegalOrSimpleName targetSpec
@@ -189,7 +214,9 @@ def parseExeTargetSpec (ws : Workspace) (spec : String) : Except CliError LeanEx
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 
-def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (Array BuildSpec) := do
+def parseTargetSpec
+  (ws : Workspace) (spec : String)
+: Except CliError (Array BuildSpec) := do
   match spec.splitOn ":" with
   | [spec] =>
     resolveTargetBaseSpec ws spec .anonymous
@@ -198,7 +225,9 @@ def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (Array Bu
   | _ =>
     throw <| CliError.invalidTargetSpec spec ':'
 
-def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (Array BuildSpec) := do
+def parseTargetSpecs
+  (ws : Workspace) (specs : List String)
+: Except CliError (Array BuildSpec) := do
   let mut results := #[]
   for spec in specs do
     results := results ++ (← parseTargetSpec ws spec)

src/lake/Lake/CLI/Error.lean

@@ -30,8 +30,7 @@ inductive CliError
 | unknownTarget (target : Name)
 | missingModule (pkg : Name) (mod : Name)
 | missingTarget (pkg : Name) (spec : String)
-| nonCliTarget (target : Name)
-| nonCliFacet (type : String) (facet : Name)
+| invalidBuildTarget (key : String)
 | invalidTargetSpec (spec : String) (tooMany : Char)
 | invalidFacet (target : Name) (facet : Name)
 /- Executable CLI Errors -/
@@ -68,8 +67,7 @@ def toString : CliError → String
 | 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}'"
-| nonCliTarget t          => s!"target `{t.toString false}` is not a buildable via `lake`"
-| nonCliFacet t f         => s!"{t} facet `{f.toString false}` is not a buildable via `lake`"
+| invalidBuildTarget t    => s!"'{t}' is not a build target (perhaps you meant 'lake query'?)"
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
 | invalidFacet t f        => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
 | unknownExe s            => s!"unknown executable {s}"

src/lake/Lake/CLI/Help.lean

@@ -18,6 +18,7 @@ COMMANDS:
   new <name> <temp>     create a Lean package in a new directory
   init <name> <temp>    create a Lean package in the current directory
   build <targets>...    build targets
+  query <targets>...    build targets and output results
   exe <exe> <args>...   build an exe and run it in Lake's environment
   check-build           check if any default build targets are configured
   test                  test the package using the configured test driver
@@ -52,6 +53,8 @@ BASIC OPTIONS:
   --no-build            exit immediately if a build target is not up-to-date
   --no-cache            build packages locally; do not download build caches
   --try-cache           attempt to download build caches for supported packages
+  --json, -J            output JSON-formatted results (in `lake query`)
+  --text                output results as plain text (in `lake query`)
 
 OUTPUT OPTIONS:
   --quiet, -q           hide informational logs and the progress indicator
@@ -136,9 +139,23 @@ TARGET EXAMPLES:        build the ...
   a/+A:c                C file of module `A` of package `a`
   :foo                  facet `foo` of the root package
 
-A bare `lake build` command will build the default facet of the root package.
+A bare `lake build` command will build the default target(s) of the root package.
 Package dependencies are not updated during a build."
 
+def helpQuery :=
+"Build targets and output results
+
+USAGE:
+  lake query [<targets>...]
+
+Builds a set of targets, reporting progress on standard error and outputting
+the results on standard out. Target results are output in the same order they
+are listed and end with a newline. If `--json` is set, results are formatted as
+JSON. Otherwise, they are printed as raw strings. Targets which do not have
+output configured will be printed as an empty string or `null`.
+
+See `lake help build` for information on and examples of targets."
+
 def helpCheckBuild :=
 "Check if any default build targets are configured
 
@@ -402,6 +419,7 @@ def help : (cmd : String) → String
 | "init"                => helpInit
 | "build"               => helpBuild
 | "check-build"         => helpCheckBuild
+| "query"               => helpQuery
 | "update" | "upgrade"  => helpUpdate
 | "pack"                => helpPack
 | "unpack"              => helpUnpack

src/lake/Lake/CLI/Main.lean

@@ -48,6 +48,7 @@ structure LakeOptions where
   failLv : LogLevel := .error
   outLv? : Option LogLevel := .none
   ansiMode : AnsiMode := .auto
+  outFormat : OutFormat := .text
 
 def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
   opts.outLv?.getD opts.verbosity.minLogLv
@@ -175,6 +176,7 @@ def lakeShortOption : (opt : Char) → CliM PUnit
 | 'R' => modifyThe LakeOptions ({· with reconfigure := true})
 | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
 | 'H' => modifyThe LakeOptions ({· with trustHash := false})
+| 'J' => modifyThe LakeOptions ({· with outFormat := .json})
 | opt => throw <| CliError.unknownShortOption opt
 
 def lakeLongOption : (opt : String) → CliM PUnit
@@ -184,6 +186,8 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--keep-toolchain" => modifyThe LakeOptions ({· with updateToolchain := false})
 | "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
+| "--text"        => modifyThe LakeOptions ({· with outFormat := .text})
+| "--json"        => modifyThe LakeOptions ({· with outFormat := .json})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
 | "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
 | "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
@@ -349,6 +353,9 @@ protected def build : CliM PUnit := do
   let ws ← loadWorkspace config
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
+  specs.forM fun spec =>
+    unless spec.buildable do
+      throw <| .invalidBuildTarget spec.info.key.toSimpleString
   let buildConfig := mkBuildConfig opts (out := .stdout)
   let showProgress := buildConfig.showProgress
   ws.runBuild (buildSpecs specs) buildConfig
@@ -360,6 +367,18 @@ protected def checkBuild : CliM PUnit := do
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
   noArgsRem do exit <| if pkg.defaultTargets.isEmpty then 1 else 0
 
+protected def query : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  let targetSpecs ← takeArgs
+  let specs ← parseTargetSpecs ws targetSpecs
+  let fmt := opts.outFormat
+  let buildConfig := mkBuildConfig opts
+  let results ← ws.runBuild (querySpecs specs fmt) buildConfig
+  results.forM (IO.println ·)
+
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
@@ -597,6 +616,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "init"                => lake.init
 | "build"               => lake.build
 | "check-build"         => lake.checkBuild
+| "query"               => lake.query
 | "update" | "upgrade"  => lake.update
 | "resolve-deps"        => lake.resolveDeps
 | "pack"                => lake.pack

src/lake/Lake/Config/FacetConfig.lean

@@ -5,25 +5,31 @@ Authors: Mac Malone, Mario Carneiro
 -/
 prelude
 import Lake.Build.Fetch
+import Lake.Config.OutFormat
 
 namespace Lake
 open Lean (Name)
 
 /-- A facet's declarative configuration. -/
 structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where
-  /-- The facet's build function. -/
-  build : ι → FetchM (Job (DataFam name))
-  /-- Does this facet  compatible with the `lake build` CLI? -/
-  cli : Bool := true
+  /-- The facet's fetch function. -/
+  fetchFn : ι → FetchM (Job (DataFam name))
+  /-- Is this facet compatible with the `lake build` CLI? -/
+  buildable : Bool := true
+  /-- Format this facet's output (e.g., for `lake query`). -/
+  format : OutFormat → DataFam name → String
   deriving Inhabited
 
 protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
 
 /-- A smart constructor for facet configurations that generate jobs for the CLI. -/
 @[inline] def mkFacetJobConfig
-  (build : ι → FetchM (Job α)) [h : FamilyOut Fam facet α]
-: FacetConfig Fam ι facet  where
-  build := cast (by rw [← h.family_key_eq_type]) build
+  [FormatQuery α] [h : FamilyOut Fam facet α]
+  (build : ι → FetchM (Job α)) (buildable := true)
+: FacetConfig Fam ι facet where
+  buildable
+  fetchFn := h.family_key_eq_type ▸ build
+  format := h.family_key_eq_type ▸ formatQuery
 
 /-- A dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where

src/lake/Lake/Config/Module.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 prelude
 import Lake.Build.Trace
 import Lake.Config.LeanLib
+import Lake.Config.OutFormat
 import Lake.Util.OrdHashSet
 
 namespace Lake
@@ -21,6 +22,9 @@ structure Module where
   -/
   keyName : Name := name
 
+instance : ToText Module := ⟨(·.name.toString)⟩
+instance : ToJson Module := ⟨(toJson ·.name)⟩
+
 instance : Hashable Module where hash m := hash m.keyName
 instance : BEq Module where beq m n := m.keyName == n.keyName
 

src/lake/Lake/Config/OutFormat.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Data.Json
+import Lake.Build.Job.Basic
+
+open Lean
+
+namespace Lake
+
+/-- Target output formats supported by the Lake CLI (e.g., `lake query`). -/
+inductive OutFormat
+| /-- Format target output as text. -/ text
+| /-- Format target output as JSON. -/ json
+
+class ToText (α : Type u) where
+  toText : α → String
+
+export ToText (toText)
+
+instance (priority := 0) [ToString α] : ToText α := ⟨toString⟩
+
+instance : ToText Json := ⟨Json.compress⟩
+instance [ToText α] : ToText (List α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropRight 1)⟩
+instance [ToText α] : ToText (Array α) := ⟨(·.foldl (s!"{·}{toText ·}\n") "" |>.dropRight 1)⟩
+
+/-- Class used to format target output for `lake query`. -/
+class FormatQuery (α : Type u) where
+  formatQuery : OutFormat → α → String
+
+export FormatQuery (formatQuery)
+
+/-- A format function that produces "null" output. -/
+def nullFormat (fmt : OutFormat) (_ : α) : String :=
+  match fmt with
+  | .text => ""
+  | .json => Json.null.compress
+
+instance (priority := 0) : FormatQuery α := ⟨nullFormat⟩
+
+/-- Format function that uses `ToText` and `ToJson` to print output. -/
+@[specialize] def stdFormat [ToText α] [ToJson α]  (fmt : OutFormat) (a : α) : String :=
+  match fmt with
+  | .text => toText a
+  | .json => toJson a |>.compress
+
+instance [ToText α] [ToJson α] : FormatQuery α := ⟨stdFormat⟩
+instance: FormatQuery Unit := ⟨nullFormat⟩

src/lake/Lake/Config/Package.lean

@@ -6,6 +6,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 prelude
 import Lake.Config.Opaque
 import Lake.Config.Defaults
+import Lake.Config.OutFormat
 import Lake.Config.LeanLibConfig
 import Lake.Config.LeanExeConfig
 import Lake.Config.ExternLibConfig
@@ -413,7 +414,6 @@ structure Package where
   /-- The driver used for `lake lint` when this package is the workspace root. -/
   lintDriver : String := config.lintDriver
 
-
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
   ⟨by constructor <;> exact default⟩
@@ -431,6 +431,9 @@ abbrev OrdPackageSet := OrdHashSet Package
 abbrev Package.name (self : Package) : Name :=
   self.config.name
 
+instance : ToText Package := ⟨(·.name.toString)⟩
+instance : ToJson Package := ⟨(toJson ·.name)⟩
+
 /-- A package with a name known at type-level. -/
 structure NPackage (name : Name) extends Package where
   name_eq : toPackage.name = name

src/lake/Lake/Config/TargetConfig.lean

@@ -5,22 +5,27 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Build.Fetch
+import Lake.Config.OutFormat
+
+open Lean
 
 namespace Lake
-open Lean (Name)
 
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
-  /-- The target's build function. -/
-  build : (pkg : NPackage pkgName) → FetchM (Job (CustomData (pkgName, name)))
+  /-- The target's fetch function. -/
+  fetchFn : (pkg : NPackage pkgName) → FetchM (Job (CustomData (pkgName, name)))
+  /-- Format the target's output (e.g., for `lake query`). -/
+  format : OutFormat → CustomData (pkgName, name) → String
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-  (build : (pkg : NPackage pkgName) → FetchM (Job α))
-  [h : FamilyOut CustomData (pkgName, name) α]
+  [FormatQuery α] [h : FamilyOut CustomData (pkgName, name) α]
+  (fetch : (pkg : NPackage pkgName) → FetchM (Job α))
 : TargetConfig pkgName name where
-  build := cast (by rw [← h.family_key_eq_type]) build
+  fetchFn := h.family_key_eq_type ▸ fetch
+  format := h.family_key_eq_type ▸ formatQuery
 
 /-- A dependently typed configuration based on its registered package and name. -/
 structure TargetDecl where

src/lake/Lake/DSL/Targets.lean

@@ -24,7 +24,7 @@ syntax buildDeclSig :=
 
 abbrev mkModuleFacetDecl
   (α) (facet : Name)
-  [FamilyDef ModuleData facet α]
+  [FormatQuery α] [FamilyDef ModuleData facet α]
   (f : Module → FetchM (Job α))
 : ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do
   withRegisterJob (mod.facet facet |>.key.toSimpleString)
@@ -59,7 +59,7 @@ kw:"module_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkPackageFacetDecl
   (α) (facet : Name)
-  [FamilyDef PackageData facet α]
+  [FormatQuery α] [FamilyDef PackageData facet α]
   (f : Package → FetchM (Job α))
 : PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do
   withRegisterJob (pkg.facet facet |>.key.toSimpleString)
@@ -94,7 +94,7 @@ kw:"package_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkLibraryFacetDecl
   (α) (facet : Name)
-  [FamilyDef LibraryData facet α]
+  [FormatQuery α] [FamilyDef LibraryData facet α]
   (f : LeanLib → FetchM (Job α))
 : LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do
   withRegisterJob (lib.facet facet |>.key.toSimpleString)
@@ -133,7 +133,7 @@ kw:"library_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkTargetDecl
   (α) (pkgName target : Name)
-  [FamilyDef CustomData (pkgName, target) α]
+  [FormatQuery α] [FamilyDef CustomData (pkgName, target) α]
   (f : NPackage pkgName → FetchM (Job α))
 : TargetDecl := .mk pkgName target <| mkTargetJobConfig fun pkg => do
   withRegisterJob (pkg.target target |>.key.toSimpleString)

src/lake/tests/query/clean.sh

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

src/lake/tests/query/exe.lean

@@ -0,0 +1 @@
+def main : IO Unit := pure ()

src/lake/tests/query/lakefile.lean

@@ -0,0 +1,17 @@
+import Lake
+open System Lake DSL
+
+package test
+
+lean_lib lib where
+  srcDir := "lib"
+  roots := #[`A, `B, `C]
+
+lean_exe a where
+  root := `exe
+
+lean_exe b where
+  root := `exe
+
+target foo : String :=
+  return .pure "foo"

src/lake/tests/query/lib/A.lean

@@ -0,0 +1 @@
+import B

src/lake/tests/query/lib/B.lean

@@ -0,0 +1 @@
+import C

src/lake/tests/query/test.sh

@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# ---
+# Test the behavior of `lake query`
+# ---
+
+# Check that logs are not written to stdout
+$LAKE query | diff - /dev/null
+
+# Test failure to build a query-only target
+($LAKE build +A:imports 2>&1 && exit 1 || true) | grep --color "not a build target"
+
+# Test querying a custom target
+test "`$LAKE query foo`" = foo
+test "`$LAKE query foo --json`" = '"foo"'
+
+# Test querying imports
+test "`$LAKE query +A:imports`" = B
+test "`$LAKE query +A:transImports --json`" = '["C","B"]'
+
+# Test querying library modules
+$LAKE query lib:modules | sort | diff -u --strip-trailing-cr <(cat << 'EOF'
+A
+B
+C
+EOF
+) -
+
+# Test that querying an executable
+# returns its path which can then be executed
+`$LAKE query a`
+
+# Test querying multiple targets
+test `$LAKE query foo foo | wc -l` = 2
+test `$LAKE query a b | wc -l` = 2