feat: lake query

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 (Job (BuildData self.info.key)) := do
+  maybeRegisterJob self.info.key.toSimpleString (← self.info.fetch)
 
-@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM OpaqueJob := 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)