feat: lake: lift FetchM into JobM (and vice versa) (#6771)

This PR enables `FetchM` to be run from `JobM` / `SpawnM` and
vice-versa. This allows calls of `fetch` to asynchronously depend on the
outputs of other jobs.

src/lake/Lake/Build.lean

@@ -10,3 +10,4 @@ import Lake.Build.Package
 import Lake.Build.Library
 import Lake.Build.Imports
 import Lake.Build.Targets
+import Lake.Build.Job

src/lake/Lake/Build/Common.lean

@@ -5,8 +5,9 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Config.Monad
-import Lake.Build.Actions
 import Lake.Util.JsonObject
+import Lake.Build.Actions
+import Lake.Build.Job
 
 /-! # Common Build Tools
 This file defines general utilities that abstract common
@@ -19,6 +20,9 @@ namespace Lake
 
 /-! ## General Utilities -/
 
+/-- Exit code to return if `--no-build` is set and a build is required. -/
+def noBuildCode : ExitCode := 3
+
 /--
 Build trace for the host platform.
 If an artifact includes this trace, it is platform-dependent

src/lake/Lake/Build/Basic.lean → src/lake/Lake/Build/Context.lean

@@ -4,20 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Util.Log
-import Lake.Util.Exit
-import Lake.Util.Lift
-import Lake.Util.Task
-import Lake.Util.Opaque
 import Lake.Config.Context
-import Lake.Build.Trace
+import Lake.Build.Job.Basic
 
 open System
 namespace Lake
 
-/-- Exit code to return if `--no-build` is set and a build is required. -/
-def noBuildCode : ExitCode := 3
-
 /-- Configuration options for a Lake build. -/
 structure BuildConfig where
   /-- Use modification times for trace checking. -/
@@ -55,58 +47,6 @@ Whether the build should show progress information.
 def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
   (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
 
-/-- Information on what this job did. -/
-inductive JobAction
-/-- No information about this job's action is available. -/
-| unknown
-/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
-| replay
-/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
-| fetch
-/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
-| build
-deriving Inhabited, Repr, DecidableEq, Ord
-
-instance : LT JobAction := ltOfOrd
-instance : LE JobAction := leOfOrd
-instance : Min JobAction := minOfLe
-instance : Max JobAction := maxOfLe
-
-def JobAction.merge (a b : JobAction) : JobAction :=
-  max a b
-
-/-- Mutable state of a Lake job. -/
-structure JobState where
-  /-- The job's log. -/
-  log : Log := {}
-  /-- Tracks whether this job performed any significant build action. -/
-  action : JobAction := .unknown
-  /-- Current trace of a build job. -/
-  trace : BuildTrace := .nil
-  deriving Inhabited
-
-/-- The result of a Lake job. -/
-abbrev JobResult α := EResult Log.Pos JobState α
-
-/-- The `Task` of a Lake job. -/
-abbrev JobTask α := BaseIOTask (JobResult α)
-
-/-- A Lake job. -/
-structure Job (α : Type u)  where
-  /-- The Lean `Task` object for the job. -/
-  task : JobTask α
-  /--
-  A caption for the job in Lake's build monitor.
-  Will be formatted like `✔ [3/5] Ran <caption>`.
-  -/
-  caption : String
-  /-- Whether this job failing should cause the build to fail. -/
-  optional : Bool := false
-  deriving Inhabited
-
-/-- A Lake job with an opaque value in `Type`. -/
-abbrev OpaqueJob := Job Opaque
-
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
@@ -119,6 +59,9 @@ abbrev BuildT := ReaderT BuildContext
 abbrev MonadBuild (m : Type → Type u) :=
   MonadReaderOf BuildContext m
 
+instance [Pure m] : MonadLift LakeM (BuildT m) where
+  monadLift x := fun ctx => pure <| x.run ctx.toContext
+
 @[inline] def getBuildContext [MonadBuild m] : m BuildContext :=
   readThe BuildContext
 
@@ -145,17 +88,3 @@ abbrev MonadBuild (m : Type → Type u) :=
 
 @[inline] def getIsQuiet [Functor m] [MonadBuild m] : m Bool :=
   (· == .quiet) <$> getVerbosity
-
-/-- The internal core monad of Lake builds.  Not intended for user use. -/
-abbrev CoreBuildM := BuildT LogIO
-
-/--
-Logs a build step with `message`.
-
-**Deprecated:**  Build steps are now managed by a top-level build monitor.
-As a result, this no longer functions the way it used to. It now just logs the
-`message` via `logVerbose`.
--/
-@[deprecated "See doc-string for deprecation information." (since := "2024-05-25"), inline]
-def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do
-  logVerbose message

src/lake/Lake/Build/Facets.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lake.Build.Job
 import Lake.Build.Data
+import Lake.Build.Job.Basic
 
 /-!
 # Simple Builtin Facet Declarations

src/lake/Lake/Build/Fetch.lean

@@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
+import Lake.Util.Lift
 import Lake.Util.Error
 import Lake.Util.Cycle
 import Lake.Util.EquipT
 import Lake.Build.Info
 import Lake.Build.Store
+import Lake.Build.Context
 
 /-! # Recursive Building
 
@@ -20,60 +22,54 @@ using the `fetch` function defined in this module.
 
 namespace Lake
 
-/-- A recursive build of a Lake build store that may encounter a cycle. -/
-abbrev RecBuildM :=
-  CallStackT BuildKey <| BuildT <| ELogT <| StateRefT BuildStore BaseIO
-
-instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
+/-- The internal core monad of Lake builds. Not intended for user use. -/
+abbrev CoreBuildM := BuildT LogIO
 
 /--
-Run a `JobM` action in `RecBuildM` (and thus `FetchM`).
+A recursive build of a Lake build store that may encounter a cycle.
 
-Generally, this should not be done, and instead a job action
-should be run asynchronously in a Job (e.g., via `Job.async`).
+An internal monad. Not intended for user use.
 -/
-@[inline] def RecBuildM.runJobM (x : JobM α) : RecBuildM α := fun _ ctx log => do
-  match (← x ctx {log}) with
-  | .ok a s => return .ok a s.log
-  | .error e s => return .error e s.log
+abbrev RecBuildT (m : Type → Type) :=
+  CallStackT BuildKey <| StateRefT' IO.RealWorld BuildStore <| BuildT m
+
+/-- Log build cycle and error. -/
+@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
+  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
+
+instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
+  throwCycle := buildCycleError
 
-instance : MonadLift JobM RecBuildM := ⟨RecBuildM.runJobM⟩
+/--
+A recursive build of a Lake build store that may encounter a cycle.
+
+An internal monad. Not intended for user use.
+-/
+abbrev RecBuildM := RecBuildT LogIO
 
 /-- Run a recursive build. -/
 @[inline] def RecBuildM.run
   (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
-: CoreBuildM (α × BuildStore) := fun ctx log => do
-  match (← (build stack ctx log).run store) with
-  | (.ok a log, store) => return .ok (a, store) log
-  | (.error e log, _) => return .error e log
+: CoreBuildM (α × BuildStore) :=
+  build stack |>.run store
 
 /-- Run a recursive build in a fresh build store. -/
 @[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
   (·.1) <$> build.run {} {}
 
-/-- Log build cycle and error. -/
-@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
-  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
-
-instance : MonadCycleOf BuildKey RecBuildM where
-  throwCycle := buildCycleError
-
 /-- 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)
 
 /-- A transformer to equip a monad with a build function for the Lake index. -/
-abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
-
-/-- The top-level monad for Lake build functions. -/
-abbrev FetchM := IndexT RecBuildM
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn RecBuildM) m
 
-/-- Ensures that `JobM` lifts into `FetchM`. -/
-example : MonadLiftT JobM FetchM := inferInstance
+/-- The top-level monad transformer for Lake build functions. -/
+abbrev FetchT (m : Type → Type) := IndexT <| RecBuildT m
 
-/-- Ensures that `SpawnM` lifts into `FetchM`. -/
-example : MonadLiftT SpawnM FetchM := inferInstance
+/-- The top-level monad for Lake build functions. -/
+abbrev FetchM := FetchT LogIO
 
 /-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
 @[deprecated FetchM (since := "2024-04-30")] abbrev IndexBuildM := FetchM
@@ -86,52 +82,3 @@ example : MonadLiftT SpawnM FetchM := inferInstance
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)
-
-/-- Wraps stray I/O, logs, and errors in `x` into the produced job.  -/
-def ensureJob (x : FetchM (Job α))
-: FetchM (Job α) := fun fetch stack ctx log store => do
-  let iniPos := log.endPos
-  match (← (withLoggedIO x) fetch stack ctx log store) with
-  | .ok job log =>
-    if iniPos < log.endPos then
-      let (log, jobLog) := log.split iniPos
-      let job := job.mapResult (sync := true) (·.prependLog jobLog)
-      return .ok job log
-    else
-      return .ok job log
-  | .error _ log =>
-    let (log, jobLog) := log.split iniPos
-    return .ok (.error jobLog) log
-
-/--
-Registers the job for the top-level build monitor,
-(e.g., the Lake CLI progress UI), assigning it `caption`.
--/
-def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
-  let job : Job α := {job with caption, optional}
-  (← getBuildContext).registeredJobs.modify (·.push job)
-  return job.renew
-
-/--
-Registers the produced job for the top-level build monitor
-(e.g., the Lake CLI progress UI), assigning it `caption`.
-
-Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
--/
-def withRegisterJob
-  (caption : String) (x : FetchM (Job α)) (optional := false)
-: FetchM (Job α) := do
-  let job ← ensureJob x
-  registerJob caption job optional
-
-/--
-Registers the produced job for the top-level build monitor
-if it is not already (i.e., it has an empty caption).
--/
-@[inline] def maybeRegisterJob
-  (caption : String) (job : Job α)
-: FetchM (Job α) := do
-  if job.caption.isEmpty then
-    registerJob caption job
-  else
-    return job