refactor: lake: all targets produce jobs (#6780)

This PR makes all targets and all `fetch` calls produce a `Job` of some
value. As part of this change, facet definitions (e.g., `library_data`,
`module_data`, `package_data`) and Lake type families (e.g.,
`FamilyOut`) should no longer include `Job` in their types (as this is
now implicit).

Author: tydeu

src/lake/Lake/Build/Facets.lean

@@ -53,7 +53,7 @@ The facet which builds all of a module's dependencies
 Returns the list of shared libraries to load along with their search path.
 -/
 abbrev Module.depsFacet := `deps
-module_data deps : Job (SearchPath × Array FilePath)
+module_data deps : SearchPath × Array FilePath
 
 /--
 The core build facet of a Lean file.
@@ -62,58 +62,58 @@ of the module (i.e., `olean`, `ilean`, `c`).
 Its trace just includes its dependencies.
 -/
 abbrev Module.leanArtsFacet := `leanArts
-module_data leanArts : Job Unit
+module_data leanArts : Unit
 
 /-- The `olean` file produced by `lean`. -/
 abbrev Module.oleanFacet := `olean
-module_data olean : Job FilePath
+module_data olean : FilePath
 
 /-- The `ilean` file produced by `lean`. -/
 abbrev Module.ileanFacet := `ilean
-module_data ilean : Job FilePath
+module_data ilean : FilePath
 
 /-- The C file built from the Lean file via `lean`. -/
 abbrev Module.cFacet := `c
-module_data c : Job FilePath
+module_data c : FilePath
 
 /-- The LLVM BC file built from the Lean file via `lean`. -/
 abbrev Module.bcFacet := `bc
-module_data bc : Job FilePath
+module_data bc : FilePath
 
 /--
 The object file `.c.o` built from `c`.
 On Windows, this is `c.o.noexport`, on other systems it is `c.o.export`).
 -/
 abbrev Module.coFacet := `c.o
-module_data c.o : Job FilePath
+module_data c.o : FilePath
 
 /-- The object file `.c.o.export` built from `c` (with `-DLEAN_EXPORTING`). -/
 abbrev Module.coExportFacet := `c.o.export
-module_data c.o.export : Job FilePath
+module_data c.o.export : FilePath
 
 /-- The object file `.c.o.noexport` built from `c` (without `-DLEAN_EXPORTING`). -/
 abbrev Module.coNoExportFacet := `c.o.noexport
-module_data c.o.noexport : Job FilePath
+module_data c.o.noexport : FilePath
 
 /-- The object file `.bc.o` built from `bc`. -/
 abbrev Module.bcoFacet := `bc.o
-module_data bc.o : Job FilePath
+module_data bc.o : FilePath
 
 /--
 The object file built from `c`/`bc`.
 On Windows with the C backend, no Lean symbols are exported.
 On every other configuration, symbols are exported.
 -/
 abbrev Module.oFacet := `o
-module_data o : Job FilePath
+module_data o : FilePath
 
 /-- The object file built from `c`/`bc` (with Lean symbols exported). -/
 abbrev Module.oExportFacet := `o.export
-module_data o.export : Job FilePath
+module_data o.export : FilePath
 
 /-- The object file built from `c`/`bc` (without Lean symbols exported). -/
 abbrev Module.oNoExportFacet := `o.noexport
-module_data o.noexport : Job FilePath
+module_data o.noexport : FilePath
 
 
 /-! ## Package Facets -/
@@ -123,35 +123,35 @@ A package's *optional* cached build archive (e.g., from Reservoir or GitHub).
 Will NOT cause the whole build to fail if the archive cannot be fetched.
 -/
 abbrev Package.optBuildCacheFacet := `optCache
-package_data optCache : Job Bool
+package_data optCache : Bool
 
 /--
 A package's cached build archive (e.g., from Reservoir or GitHub).
 Will cause the whole build to fail if the archive cannot be fetched.
 -/
 abbrev Package.buildCacheFacet := `cache
-package_data cache : Job Unit
+package_data cache : Unit
 
 /--
 A package's *optional* build archive from Reservoir.
 Will NOT cause the whole build to fail if the barrel cannot be fetched.
 -/
 abbrev Package.optReservoirBarrelFacet := `optBarrel
-package_data optBarrel : Job Bool
+package_data optBarrel : Bool
 
 /--
 A package's Reservoir build archive from Reservoir.
 Will cause the whole build to fail if the barrel cannot be fetched.
 -/
 abbrev Package.reservoirBarrelFacet := `barrel
-package_data barrel : Job Unit
+package_data barrel : Unit
 
 /--
 A package's *optional* build archive from a GitHub release.
 Will NOT cause the whole build to fail if the release cannot be fetched.
 -/
 abbrev Package.optGitHubReleaseFacet := `optRelease
-package_data optRelease : Job Bool
+package_data optRelease : Bool
 
 @[deprecated optGitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.optReleaseFacet := optGitHubReleaseFacet
@@ -161,49 +161,49 @@ A package's build archive from a GitHub release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
 abbrev Package.gitHubReleaseFacet := `release
-package_data release : Job Unit
+package_data release : Unit
 
 @[deprecated gitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.releaseFacet := gitHubReleaseFacet
 
 /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
 abbrev Package.extraDepFacet := `extraDep
-package_data extraDep : Job Unit
+package_data extraDep : Unit
 
 /-! ## Target Facets -/
 
 /-- A Lean library's Lean artifacts (i.e., `olean`, `ilean`, `c`). -/
 abbrev LeanLib.leanArtsFacet := `leanArts
-library_data leanArts : Job Unit
+library_data leanArts : Unit
 
 /-- A Lean library's static artifact. -/
 abbrev LeanLib.staticFacet := `static
-library_data static : Job FilePath
+library_data static : FilePath
 
 /-- A Lean library's static artifact (with exported symbols). -/
 abbrev LeanLib.staticExportFacet := `static.export
-library_data static.export : Job FilePath
+library_data static.export : FilePath
 
 /-- A Lean library's shared artifact. -/
 abbrev LeanLib.sharedFacet := `shared
-library_data shared : Job FilePath
+library_data shared : FilePath
 
 /-- A Lean library's `extraDepTargets` mixed with its package's. -/
 abbrev LeanLib.extraDepFacet := `extraDep
-library_data extraDep : Job Unit
+library_data extraDep : Unit
 
 /-- A Lean binary executable. -/
 abbrev LeanExe.exeFacet := `leanExe
-target_data leanExe : Job FilePath
+target_data leanExe : FilePath
 
 /-- A external library's static binary. -/
 abbrev ExternLib.staticFacet := `externLib.static
-target_data externLib.static : Job FilePath
+target_data externLib.static : FilePath
 
 /-- A external library's shared binary. -/
 abbrev ExternLib.sharedFacet := `externLib.shared
-target_data externLib.shared : Job FilePath
+target_data externLib.shared : FilePath
 
 /-- A external library's dynlib. -/
 abbrev ExternLib.dynlibFacet := `externLib.dynlib
-target_data externLib.dynlib : Job Dynlib
+target_data externLib.dynlib : Dynlib

src/lake/Lake/Build/Fetch.lean

@@ -59,8 +59,8 @@ abbrev RecBuildM := RecBuildT LogIO
 
 /-- A build function for any element of the Lake build index. -/
 abbrev IndexBuildFn (m : Type → Type v) :=
-  -- `DFetchFn BuildInfo (BuildData ·.key) m` with less imports
-  (info : BuildInfo) → m (BuildData info.key)
+  -- `DFetchFn BuildInfo (Job <| BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (Job (BuildData info.key))
 
 /-- A transformer to equip a monad with a build function for the Lake index. -/
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn RecBuildM) m
@@ -78,7 +78,7 @@ abbrev FetchM := FetchT LogIO
 @[deprecated FetchM (since := "2024-04-30")] abbrev BuildM := BuildT LogIO
 
 /-- Fetch the result associated with the info using the Lake build index. -/
-@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α :=
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM (Job α) :=
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)

src/lake/Lake/Build/Index.lean

@@ -26,13 +26,13 @@ dynamically-typed equivalent.
 -/
 @[macro_inline] def mkTargetFacetBuild
   (facet : Name) (build : FetchM (Job α))
-  [h : FamilyOut TargetData facet (Job α)]
-: FetchM (TargetData facet) :=
+  [h : FamilyOut TargetData facet α]
+: FetchM (Job (TargetData facet)) :=
   cast (by rw [← h.family_key_eq_type]) build
 
 def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
   withRegisterJob s!"{lib.staticTargetName.toString}:static" do
-  lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
+  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
 
 def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
   withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
@@ -47,7 +47,7 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex : (info : BuildInfo) → FetchM (BuildData info.key)
+def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
     config.build mod
@@ -82,4 +82,5 @@ Run a recursive Lake build using the Lake build index
 and a topological / suspending scheduler.
 -/
 def FetchM.run (x : FetchM α) : RecBuildM α :=
-  x (inline <| recFetchMemoize BuildInfo.key recBuildWithIndex)
+  x <| inline <|
+    recFetchMemoize (β := (Job <| BuildData ·)) BuildInfo.key recBuildWithIndex

src/lake/Lake/Build/Info.lean

@@ -125,27 +125,27 @@ definitions.
 
 /-- The direct local imports of the Lean module. -/
 abbrev Module.importsFacet := `lean.imports
-module_data lean.imports : Job (Array Module)
+module_data lean.imports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
 abbrev Module.transImportsFacet := `lean.transImports
-module_data lean.transImports : Job (Array Module)
+module_data lean.transImports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
 abbrev Module.precompileImportsFacet := `lean.precompileImports
-module_data lean.precompileImports : Job (Array Module)
+module_data lean.precompileImports : Array Module
 
 /-- Shared library for `--load-dynlib`. -/
 abbrev Module.dynlibFacet := `dynlib
-module_data dynlib : Job Dynlib
+module_data dynlib : Dynlib
 
 /-- A Lean library's Lean modules. -/
 abbrev LeanLib.modulesFacet := `modules
-library_data modules : Job (Array Module)
+library_data modules : Array Module
 
 /-- The package's complete array of transitive dependencies. -/
 abbrev Package.depsFacet := `deps
-package_data deps : Job (Array Package)
+package_data deps : Array Package
 
 
 /-!

src/lake/Lake/Build/Package.lean

@@ -147,7 +147,7 @@ def Package.fetchBuildArchive
 private def Package.mkOptBuildArchiveFacetConfig
   {facet : Name} (archiveFile : Package → FilePath)
   (getUrl : Package → JobM String) (headers : Array String := #[])
-  [FamilyDef PackageData facet (Job Bool)]
+  [FamilyDef PackageData facet Bool]
 : PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
   withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
   try
@@ -161,8 +161,8 @@ private def Package.mkOptBuildArchiveFacetConfig
 @[inline]
 private def Package.mkBuildArchiveFacetConfig
   {facet : Name} (optFacet : Name) (what : String)
-  [FamilyDef PackageData facet (Job Unit)]
-  [FamilyDef PackageData optFacet (Job Bool)]
+  [FamilyDef PackageData facet Unit]
+  [FamilyDef PackageData optFacet Bool]
 : PackageFacetConfig facet :=
   mkFacetJobConfig fun pkg =>
     withRegisterJob s!"{pkg.name}:{facet}" do

src/lake/Lake/Build/Store.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Build.Data
+import Lake.Build.Job.Basic
 import Lake.Util.StoreInsts
 
 /-!
@@ -19,23 +20,21 @@ namespace Lake
 open Lean (Name NameMap)
 
 /-- A monad equipped with a Lake build store. -/
-abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
+abbrev MonadBuildStore (m) := MonadDStore BuildKey (Job <| BuildData ·) m
 
 /-- The type of the Lake build store. -/
 abbrev BuildStore :=
-  DRBMap BuildKey BuildData BuildKey.quickCmp
+  DRBMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp
 
 @[inline] def BuildStore.empty : BuildStore := DRBMap.empty
 
 namespace BuildStore
 
--- Linter reports false positives on the `v` variables below
-set_option linter.unusedVariables false
-
 /-- Derive an array of built module facets from the store. -/
-def collectModuleFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut ModuleData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectModuleFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
@@ -46,9 +45,10 @@ def collectModuleFacetArray (self : BuildStore)
   return res
 
 /-- Derive a map of module names to built facets from the store. -/
-def collectModuleFacetMap (self : BuildStore)
-(facet : Name) [FamilyOut ModuleData facet α] : NameMap α := Id.run do
-  let mut res := Lean.mkNameMap α
+def collectModuleFacetMap
+  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+: NameMap (Job α) := Id.run do
+  let mut res := Lean.mkNameMap (Job α)
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
@@ -59,9 +59,10 @@ def collectModuleFacetMap (self : BuildStore)
   return res
 
 /-- Derive an array of built package facets from the store. -/
-def collectPackageFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut PackageData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectPackageFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut PackageData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .packageFacet _ f =>
@@ -72,9 +73,10 @@ def collectPackageFacetArray (self : BuildStore)
   return res
 
 /-- Derive an array of built target facets from the store. -/
-def collectTargetFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut TargetData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectTargetFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut TargetData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .targetFacet _ _ f =>
@@ -85,6 +87,6 @@ def collectTargetFacetArray (self : BuildStore)
   return res
 
 /-- Derive an array of built external shared libraries from the store. -/
-def collectSharedExternLibs (self : BuildStore)
-[FamilyOut TargetData `externLib.shared α] : Array α :=
-  self.collectTargetFacetArray `externLib.shared
+def collectSharedExternLibs
+  (self : BuildStore) [FamilyOut TargetData `externLib.shared α]
+: Array (Job α) := self.collectTargetFacetArray `externLib.shared