diff --git a/src/lake/Lake/Build.lean b/src/lake/Lake/Build.lean
index 2bc56f42c0..07002a3b4a 100644
--- a/src/lake/Lake/Build.lean
+++ b/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
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 5f45e64cfb..36c8de46f1 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/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
diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Context.lean
similarity index 55%
rename from src/lake/Lake/Build/Basic.lean
rename to src/lake/Lake/Build/Context.lean
index 8f02bf5cea..dbc3b5c007 100644
--- a/src/lake/Lake/Build/Basic.lean
+++ b/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 : 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
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index da9c577120..28227c1ff7 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/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
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 668bfc84b8..ee4b89beb1 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/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
-
-instance : MonadLift JobM RecBuildM := ⟨RecBuildM.runJobM⟩
-
-/-- 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
-
-/-- Run a recursive build in a fresh build store. -/
-@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
- (·.1) <$> build.run {} {}
+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 : MonadCycleOf BuildKey RecBuildM where
+instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where
throwCycle := buildCycleError
+/--
+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) :=
+ build stack |>.run store
+
+/-- Run a recursive build in a fresh build store. -/
+@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
+ (·.1) <$> build.run {} {}
+
/-- 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
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn RecBuildM) m
+
+/-- The top-level monad transformer for Lake build functions. -/
+abbrev FetchT (m : Type → Type) := IndexT <| RecBuildT m
/-- The top-level monad for Lake build functions. -/
-abbrev FetchM := IndexT RecBuildM
-
-/-- Ensures that `JobM` lifts into `FetchM`. -/
-example : MonadLiftT JobM FetchM := inferInstance
-
-/-- Ensures that `SpawnM` lifts into `FetchM`. -/
-example : MonadLiftT SpawnM FetchM := inferInstance
+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
diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean
index ff5a5f50af..9ea3bfd4f0 100644
--- a/src/lake/Lake/Build/Job.lean
+++ b/src/lake/Lake/Build/Job.lean
@@ -1,387 +1,9 @@
/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
+Copyright (c) 2025 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
prelude
-import Lake.Build.Basic
-
-open System
-
-namespace Lake
-
-def JobAction.verb (failed : Bool) : JobAction → String
-| .unknown => if failed then "Running" else "Ran"
-| .replay => if failed then "Replaying" else "Replayed"
-| .fetch => if failed then "Fetching" else "Fetched"
-| .build => if failed then "Building" else "Built"
-
-/--
-Resets the job state after a checkpoint (e.g., registering the job).
-Preserves state that downstream jobs want to depend on while resetting
-job-local state that should not be inherited by downstream jobs.
--/
-@[inline] def JobState.renew (s : JobState) : JobState where
- trace := s.trace
-
-def JobState.merge (a b : JobState) : JobState where
- log := a.log ++ b.log
- action := a.action.merge b.action
- trace := mixTrace a.trace b.trace
-
-@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) :=
- {s with log := f s.log}
-
-@[inline] def JobState.logEntry (e : LogEntry) (s : JobState) :=
- s.modifyLog (·.push e)
-
-/-- Add log entries to the beginning of the job's log. -/
-def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
- match self with
- | .ok a s => .ok a <| s.modifyLog (log ++ ·)
- | .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
-
-/--
-The monad of asynchronous Lake jobs.
-
-While this can be lifted into `FetchM`, job action should generally
-be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
-run directly in `FetchM`.
--/
-abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO
-
-instance [Pure m] : MonadLift LakeM (BuildT m) where
- monadLift x := fun ctx => pure <| x.run ctx.toContext
-
-instance : MonadStateOf Log JobM where
- get := (·.log) <$> get
- set log := modify fun s => {s with log}
- modifyGet f := modifyGet fun s => let (a, log) := f s.log; (a, {s with log})
-
-instance : MonadStateOf JobState JobM := inferInstance
-
-instance : MonadLog JobM := .ofMonadState
-instance : MonadError JobM := ELog.monadError
-instance : Alternative JobM := ELog.alternative
-instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
-
-/-- Record that this job is trying to perform some action. -/
-@[inline] def updateAction (action : JobAction) : JobM PUnit :=
- modify fun s => {s with action := s.action.merge action}
-
-/-- Returns the current job's build trace. -/
-@[inline] def getTrace : JobM BuildTrace :=
- (·.trace) <$> get
-
-/-- Sets the current job's build trace. -/
-@[inline] def setTrace (trace : BuildTrace) : JobM PUnit :=
- modify fun s => {s with trace := trace}
-
-/-- Mix a trace into the current job's build trace. -/
-@[inline] def addTrace (trace : BuildTrace) : JobM PUnit :=
- modify fun s => {s with trace := s.trace.mix trace}
-
-/-- Returns the current job's build trace and removes it from the state. -/
-@[inline] def takeTrace : JobM BuildTrace :=
- modifyGet fun s => (s.trace, {s with trace := nilTrace})
-
-/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
-abbrev SpawnM := BuildT <| ReaderT BuildTrace <| BaseIO
-
-@[inline] def JobM.runSpawnM (x : SpawnM α) : JobM α := fun ctx s =>
- return .ok (← x ctx s.trace) s
-
-instance : MonadLift SpawnM JobM := ⟨JobM.runSpawnM⟩
-
-/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
-@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
-
-@[inline] private unsafe def Job.toOpaqueImpl (job : Job α) : OpaqueJob :=
- unsafeCast job
-
-/-- Forget the value of a job. Implemented as a no-op cast. -/
-@[implemented_by toOpaqueImpl]
-def Job.toOpaque (job : Job α) : OpaqueJob :=
- {job with task := job.task.map (·.map Opaque.mk)}
-
-instance : CoeOut (Job α) OpaqueJob := ⟨.toOpaque⟩
-
-namespace Job
-
-@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
- {task, caption}
-
-@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
- {task := Task.pure (.error 0 {log}), caption}
-
-@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
- {task := Task.pure (.ok a {log}), caption}
-
-instance : Pure Job := ⟨Job.pure⟩
-instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
-
-@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
- .pure () log caption
-
-@[inline] def nil : Job Unit :=
- .pure ()
-
-/-- Sets the job's caption. -/
-@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
- {job with caption}
-
-/-- Sets the job's caption if the job's current caption is empty. -/
-@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
- if job.caption.isEmpty then {job with caption} else job
-
-@[inline] def mapResult
- (f : JobResult α → JobResult β) (self : Job α)
- (prio := Task.Priority.default) (sync := false)
-: Job β := {self with task := self.task.map f prio sync}
-
-@[inline] def mapOk
- (f : α → JobState → JobResult β) (self : Job α)
- (prio := Task.Priority.default) (sync := false)
-: Job β :=
- self.mapResult (prio := prio) (sync := sync) fun
- | .ok a s => f a s
- | .error e s => .error e s
-
-@[inline] def bindTask [Monad m]
- (f : JobTask α → m (JobTask β)) (self : Job α)
-: m (Job β) := return {self with task := ← f self.task}
-
-@[inline] protected def map
- (f : α → β) (self : Job α)
- (prio := Task.Priority.default) (sync := false)
-: Job β := self.mapResult (·.map f) prio sync
-
-instance : Functor Job where map := Job.map
-
-/--
-Resets the job's state after a checkpoint (e.g., registering the job).
-Preserves information that downstream jobs want to depend on while resetting
-job-local information that should not be inherited by downstream jobs.
--/
-def renew (self : Job α) : Job α :=
- self.mapResult (sync := true) fun
- | .ok a s => .ok a s.renew
- | .error _ s => .error 0 s.renew
-
-/-- Spawn a job that asynchronously performs `act`. -/
-@[inline] protected def async
- (act : JobM α) (prio := Task.Priority.default)
-: SpawnM (Job α) := fun ctx => .ofTask <$> do
- BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
-
-/-- Wait a the job to complete and return the result. -/
-@[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
- IO.wait self.task
-
-/--
-Wait for a job to complete and return the produced value.
-If an error occurred, return `none` and discarded any logs produced.
--/
-@[inline] protected def wait? (self : Job α) : BaseIO (Option α) := do
- return (← self.wait).result?
-
-/--
-Wait for a job to complete and return the produced value.
-Logs the job's log and throws if there was an error.
--/
-@[inline] protected def await (self : Job α) : LogIO α := do
- match (← self.wait) with
- | .error n {log, ..} => log.replay; throw n
- | .ok a {log, ..} => log.replay; pure a
-
-/-- Apply `f` asynchronously to the job's output. -/
-protected def mapM
- (self : Job α) (f : α → JobM β)
- (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) :=
- fun ctx trace => do
- self.bindTask fun task => do
- BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
- | .ok a s =>
- let trace := mixTrace trace s.trace
- withLoggedIO (f a) ctx {s with trace}
- | .error n s => return .error n s
-
-@[deprecated Job.mapM (since := "2024-12-06")]
-protected abbrev bindSync
- (self : Job α) (f : α → JobM β)
- (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := self.mapM f prio sync
-
-/--
-Apply `f` asynchronously to the job's output
-and asynchronously await the resulting job.
--/
-def bindM
- (self : Job α) (f : α → JobM (Job β))
- (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) :=
- fun ctx trace => do
- self.bindTask fun task => do
- BaseIO.bindTask task (prio := prio) (sync := sync) fun
- | .ok a sa => do
- let trace := mixTrace trace sa.trace
- match (← withLoggedIO (f a) ctx {sa with trace}) with
- | .ok job sa =>
- return job.task.map (prio := prio) (sync := true) fun
- | .ok b sb => .ok b {sa.merge sb with trace := sb.trace}
- | .error e sb => .error ⟨sa.log.size + e.val⟩ {sa.merge sb with trace := sb.trace}
- | .error e sa => return Task.pure (.error e sa)
- | .error e sa => return Task.pure (.error e sa)
-
-@[deprecated bindM (since := "2024-12-06")]
-protected abbrev bindAsync
- (self : Job α) (f : α → SpawnM (Job β))
- (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := self.bindM (fun a => f a) prio sync
-
-/--
-`a.zipWith f b` produces a new job `c` that applies `f` to the
-results of `a` and `b`. The job `c` errors if either `a` or `b` error.
--/
-@[inline] def zipResultWith
- (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
- (prio := Task.Priority.default) (sync := true)
-: Job γ := Job.ofTask $
- self.task.bind (prio := prio) (sync := true) fun rx =>
- other.task.map (prio := prio) (sync := sync) fun ry =>
- f rx ry
-
-/--
-`a.zipWith f b` produces a new job `c` that applies `f` to the
-results of `a` and `b`. The job `c` errors if either `a` or `b` error.
--/
-@[inline] def zipWith
- (f : α → β → γ) (self : Job α) (other : Job β)
- (prio := Task.Priority.default) (sync := true)
-: Job γ :=
- self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
- | .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
- | ra, rb => .error 0 (ra.state.merge rb.state)
-
-
-/-- Merges this job with another, discarding its output and trace. -/
-def add (self : Job α) (other : Job β) : Job α :=
- self.zipResultWith (other := other) fun
- | .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
- | ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
-
-/-- Merges this job with another, discarding both outputs. -/
-def mix (self : Job α) (other : Job β) : Job Unit :=
- self.zipWith (fun _ _ => ()) other
-
-/-- Merge a `List` of jobs into one, discarding their outputs. -/
-def mixList (jobs : List (Job α)) : Job Unit :=
- jobs.foldr (·.mix ·) nil
-
-/-- Merge an `Array` of jobs into one, discarding their outputs. -/
-def mixArray (jobs : Array (Job α)) : Job Unit :=
- jobs.foldl (·.mix ·) nil
-
-/-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
-def collectList (jobs : List (Job α)) : Job (List α) :=
- jobs.foldr (zipWith List.cons) (pure [])
-
-/-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
-def collectArray (jobs : Array (Job α)) : Job (Array α) :=
- jobs.foldl (zipWith Array.push) (pure (Array.mkEmpty jobs.size))
-
-end Job
-
-/-- A Lake build job. -/
-abbrev BuildJob α := Job α
-
-namespace BuildJob
-
-@[inline, deprecated "Obsolete." (since := "2024-12-06")]
-def mk (job : Job (α × BuildTrace)) : BuildJob α :=
- job.mapOk fun (a, trace) s => .ok a {s with trace}
-
-@[inline, deprecated "Obsolete." (since := "2024-12-06")]
-def ofJob (job : Job BuildTrace) : BuildJob Unit :=
- job.mapOk fun trace s => .ok () {s with trace}
-
-abbrev toJob (self : BuildJob α) : Job α :=
- self
-
-@[deprecated Job.nil (since := "2024-12-06")]
-abbrev nil : BuildJob Unit :=
- Job.pure ()
-
-@[deprecated Job.map (since := "2024-12-06")]
-protected abbrev pure (a : α) : BuildJob α :=
- Job.pure a
-
-instance : Pure BuildJob := ⟨Job.pure⟩
-
-@[deprecated Job.map (since := "2024-12-06")]
-protected abbrev map (f : α → β) (self : BuildJob α) : BuildJob β :=
- self.toJob.map f
-
-instance : Functor BuildJob where
- map := Job.map
-
-@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
-def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
- self.toJob.mapOk fun a s =>
- let (b, trace) := f a s.trace
- .ok b {s with trace}
-
-@[inline, deprecated Job.mapM (since := "2024-12-06")]
-protected def bindSync
- (self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
- (prio : Task.Priority := .default) (sync := false)
-: SpawnM (Job β) :=
- self.toJob.mapM (prio := prio) (sync := sync) fun a => do
- let (b, trace) ← f a (← getTrace)
- setTrace trace
- return b
-
-@[inline, deprecated Job.bindM (since := "2024-12-06")]
-protected def bindAsync
- (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
- (prio : Task.Priority := .default) (sync := false)
- : SpawnM (Job β) :=
- self.toJob.bindM (prio := prio) (sync := sync) fun a => do
- f a (← getTrace)
-
-@[deprecated Job.wait? (since := "2024-12-06")]
-protected abbrev wait? (self : BuildJob α) : BaseIO (Option α) :=
- self.toJob.wait?
-
-@[deprecated Job.add (since := "2024-12-06")]
-abbrev add (self : BuildJob α) (other : BuildJob β) : BuildJob α :=
- self.toJob.add other.toJob
-
-@[deprecated Job.mix (since := "2024-12-06")]
-abbrev mix (self : BuildJob α) (other : BuildJob β) : BuildJob Unit :=
- self.toJob.mix other.toJob
-
-@[deprecated Job.mixList (since := "2024-12-06")]
-abbrev mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) :=
- return Job.mixList jobs
-
-@[deprecated Job.mixArray (since := "2024-12-06")]
-abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
- return Job.mixArray jobs
-
-@[deprecated Job.zipWith (since := "2024-12-06")]
-abbrev zipWith
- (f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
-: BuildJob γ :=
- self.toJob.zipWith f other.toJob
-
-@[deprecated Job.collectList (since := "2024-12-06")]
-abbrev collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
- return Job.collectList jobs
-
-@[deprecated Job.collectArray (since := "2024-12-06")]
-abbrev collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
- return Job.collectArray jobs
-
-attribute [deprecated Job (since := "2024-12-06")] BuildJob
+import Lake.Build.Job.Basic
+import Lake.Build.Job.Monad
+import Lake.Build.Job.Register
diff --git a/src/lake/Lake/Build/Job/Basic.lean b/src/lake/Lake/Build/Job/Basic.lean
new file mode 100644
index 0000000000..7f34072d39
--- /dev/null
+++ b/src/lake/Lake/Build/Job/Basic.lean
@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Util.Log
+import Lake.Util.Task
+import Lake.Util.Opaque
+import Lake.Build.Trace
+
+/-! # Job Primitives
+
+This module contains the basic definitions of a Lake `Job`. In particular,
+it defines `OpaqueJob`, which is needed for `BuildContext`. More complex
+utilities are defined in `Lake.Build.Job.Monad`, which depends on `BuildContext`.
+-/
+
+open System
+
+namespace Lake
+
+/-! ## JobAction -/
+
+/-- 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
+
+def JobAction.verb (failed : Bool) : JobAction → String
+| .unknown => if failed then "Running" else "Ran"
+| .replay => if failed then "Replaying" else "Replayed"
+| .fetch => if failed then "Fetching" else "Fetched"
+| .build => if failed then "Building" else "Built"
+
+/-! ## JobState -/
+
+/-- 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
+
+def JobState.merge (a b : JobState) : JobState where
+ log := a.log ++ b.log
+ action := a.action.merge b.action
+ trace := mixTrace a.trace b.trace
+
+@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) : JobState :=
+ {s with log := f s.log}
+
+@[inline] def JobState.logEntry (e : LogEntry) (s : JobState) :=
+ s.modifyLog (·.push e)
+
+/-! ## JobTask -/
+
+/-- The result of a Lake job. -/
+abbrev JobResult α := EResult Log.Pos JobState α
+
+/-- Add log entries to the beginning of the job's log. -/
+def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
+ match self with
+ | .ok a s => .ok a <| s.modifyLog (log ++ ·)
+ | .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
+
+/-- The `Task` of a Lake job. -/
+abbrev JobTask α := BaseIOTask (JobResult α)
+
+/-! ## Job -/
+
+/-- 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 : String
+ /-- Whether this job failing should cause the build to fail. -/
+ optional : Bool := false
+ deriving Inhabited
+
+namespace Job
+
+@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
+ {task, caption}
+
+@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
+ {task := Task.pure (.error 0 {log}), caption}
+
+@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
+ {task := Task.pure (.ok a {log}), caption}
+
+instance : Pure Job := ⟨Job.pure⟩
+
+@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
+ .pure () log caption
+
+@[inline] def nil : Job Unit :=
+ .pure ()
+
+/-- Sets the job's caption. -/
+@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
+ {job with caption}
+
+/-- Sets the job's caption if the job's current caption is empty. -/
+@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
+ if job.caption.isEmpty then {job with caption} else job
+
+@[inline] def mapResult
+ (f : JobResult α → JobResult β) (self : Job α)
+ (prio := Task.Priority.default) (sync := false)
+: Job β := {self with task := self.task.map f prio sync}
+
+@[inline] def mapOk
+ (f : α → JobState → JobResult β) (self : Job α)
+ (prio := Task.Priority.default) (sync := false)
+: Job β :=
+ self.mapResult (prio := prio) (sync := sync) fun
+ | .ok a s => f a s
+ | .error e s => .error e s
+
+@[inline] protected def map
+ (f : α → β) (self : Job α)
+ (prio := Task.Priority.default) (sync := false)
+: Job β := self.mapResult (·.map f) prio sync
+
+instance : Functor Job where map := Job.map
+
+end Job
+
+/-! ## OpaqueJob -/
+
+/-- A Lake job with an opaque value in `Type`. -/
+abbrev OpaqueJob := Job Opaque
+
+@[inline] private unsafe def Job.toOpaqueImpl (job : Job α) : OpaqueJob :=
+ unsafeCast job
+
+/-- Forget the value of a job. Implemented as a no-op cast. -/
+@[implemented_by toOpaqueImpl]
+def Job.toOpaque (job : Job α) : OpaqueJob :=
+ {job with task := job.task.map (·.map Opaque.mk)}
+
+instance : CoeOut (Job α) OpaqueJob := ⟨.toOpaque⟩
diff --git a/src/lake/Lake/Build/Job/Monad.lean b/src/lake/Lake/Build/Job/Monad.lean
new file mode 100644
index 0000000000..68940c84f7
--- /dev/null
+++ b/src/lake/Lake/Build/Job/Monad.lean
@@ -0,0 +1,328 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Build.Fetch
+
+open System
+
+/-! # Job Monad
+
+This module contains additional definitions for Lake `Job`.
+In particular, it defines `JobM`, which uses `BuildContext`, which contains
+`OpaqueJob`s, hence the module split.
+-/
+
+namespace Lake
+
+/--
+The monad of asynchronous Lake jobs.
+
+While this can be lifted into `FetchM`, job action should generally
+be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
+run directly in `FetchM`.
+-/
+abbrev JobM := FetchT <| EStateT Log.Pos JobState BaseIO
+
+instance (priority := high) : MonadStateOf JobState JobM := inferInstance
+
+instance : MonadStateOf Log JobM where
+ get := (·.log) <$> get
+ set log := modify fun s => {s with log}
+ modifyGet f := modifyGet fun s => let (a, log) := f s.log; (a, {s with log})
+
+instance : MonadLog JobM := .ofMonadState
+instance : MonadError JobM := ELog.monadError
+instance : Alternative JobM := ELog.alternative
+instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
+
+/-- Record that this job is trying to perform some action. -/
+@[inline] def updateAction (action : JobAction) : JobM PUnit :=
+ modify fun s => {s with action := s.action.merge action}
+
+/-- Returns the current job's build trace. -/
+@[inline] def getTrace : JobM BuildTrace :=
+ (·.trace) <$> get
+
+/-- Sets the current job's build trace. -/
+@[inline] def setTrace (trace : BuildTrace) : JobM PUnit :=
+ modify fun s => {s with trace := trace}
+
+/-- Mix a trace into the current job's build trace. -/
+@[inline] def addTrace (trace : BuildTrace) : JobM PUnit :=
+ modify fun s => {s with trace := s.trace.mix trace}
+
+/-- Returns the current job's build trace and removes it from the state. -/
+@[inline] def takeTrace : JobM BuildTrace :=
+ modifyGet fun s => (s.trace, {s with trace := nilTrace})
+
+/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
+abbrev SpawnM := FetchT <| ReaderT BuildTrace <| BaseIO
+
+@[inline] def JobM.runSpawnM (x : SpawnM α) : JobM α := fun fn stack store ctx s =>
+ return .ok (← x fn stack store ctx s.trace) s
+
+instance : MonadLift SpawnM JobM := ⟨JobM.runSpawnM⟩
+
+/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
+@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
+
+/--
+Run a `JobM` action in `FetchM`.
+
+Generally, this should not be done, and instead a job action
+should be run asynchronously in a Job (e.g., via `Job.async`).
+-/
+@[inline] def FetchM.runJobM (x : JobM α) : FetchM α := fun fetch stack store ctx log => do
+ match (← x fetch stack store ctx {log}) with
+ | .ok a s => return .ok a s.log
+ | .error e s => return .error e s.log
+
+instance : MonadLift JobM FetchM := ⟨FetchM.runJobM⟩
+
+/-- Ensures that `JobM` lifts into `FetchM`. -/
+example : MonadLiftT JobM FetchM := inferInstance
+
+/-- Ensures that `SpawnM` lifts into `FetchM`. -/
+example : MonadLiftT SpawnM FetchM := inferInstance
+
+/-- Run a `FetchM` action in `JobM`. -/
+@[inline] def JobM.runFetchM (x : FetchM α) : JobM α := fun fetch stack store ctx s => do
+ match (← x fetch stack store ctx s.log) with
+ | .ok a log => return .ok a {s with log}
+ | .error e log => return .error e {s with log}
+
+instance : MonadLift FetchM JobM := ⟨JobM.runFetchM⟩
+
+/-- Ensures that `FetchM` lifts into `JobM`. -/
+example : MonadLiftT FetchM JobM := inferInstance
+
+/-- Ensures that `FetchM` lifts into `SpawnM`. -/
+example : MonadLiftT SpawnM FetchM := inferInstance
+
+namespace Job
+
+@[inline] def bindTask [Monad m]
+ (f : JobTask α → m (JobTask β)) (self : Job α)
+: m (Job β) := return {self with task := ← f self.task}
+
+/-- Spawn a job that asynchronously performs `act`. -/
+@[inline] protected def async
+ (act : JobM α) (prio := Task.Priority.default)
+: SpawnM (Job α) := fun fetch stack store ctx => .ofTask <$> do
+ BaseIO.asTask (prio := prio) do (withLoggedIO act) fetch stack store ctx {}
+
+/-- Wait a the job to complete and return the result. -/
+@[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
+ IO.wait self.task
+
+/--
+Wait for a job to complete and return the produced value.
+If an error occurred, return `none` and discarded any logs produced.
+-/
+@[inline] protected def wait? (self : Job α) : BaseIO (Option α) := do
+ return (← self.wait).result?
+
+/--
+Wait for a job to complete and return the produced value.
+Logs the job's log and throws if there was an error.
+-/
+@[inline] protected def await (self : Job α) : LogIO α := do
+ match (← self.wait) with
+ | .error n {log, ..} => log.replay; throw n
+ | .ok a {log, ..} => log.replay; pure a
+
+/-- Apply `f` asynchronously to the job's output. -/
+protected def mapM
+ (self : Job α) (f : α → JobM β)
+ (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) :=
+ fun fetch stack store ctx trace => do
+ self.bindTask fun task => do
+ BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
+ | .ok a s =>
+ let trace := mixTrace trace s.trace
+ withLoggedIO (f a) fetch stack store ctx {s with trace}
+ | .error n s => return .error n s
+
+@[deprecated Job.mapM (since := "2024-12-06")]
+protected abbrev bindSync
+ (self : Job α) (f : α → JobM β)
+ (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) := self.mapM f prio sync
+
+/--
+Apply `f` asynchronously to the job's output
+and asynchronously await the resulting job.
+-/
+def bindM
+ (self : Job α) (f : α → JobM (Job β))
+ (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) :=
+ fun fetch stack store ctx trace => do
+ self.bindTask fun task => do
+ BaseIO.bindTask task (prio := prio) (sync := sync) fun
+ | .ok a sa => do
+ let trace := mixTrace trace sa.trace
+ match (← withLoggedIO (f a) fetch stack store ctx {sa with trace}) with
+ | .ok job sa =>
+ return job.task.map (prio := prio) (sync := true) fun
+ | .ok b sb => .ok b {sa.merge sb with trace := sb.trace}
+ | .error e sb => .error ⟨sa.log.size + e.val⟩ {sa.merge sb with trace := sb.trace}
+ | .error e sa => return Task.pure (.error e sa)
+ | .error e sa => return Task.pure (.error e sa)
+
+@[deprecated bindM (since := "2024-12-06")]
+protected abbrev bindAsync
+ (self : Job α) (f : α → SpawnM (Job β))
+ (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) := self.bindM (fun a => f a) prio sync
+
+/--
+`a.zipWith f b` produces a new job `c` that applies `f` to the
+results of `a` and `b`. The job `c` errors if either `a` or `b` error.
+-/
+@[inline] def zipResultWith
+ (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
+ (prio := Task.Priority.default) (sync := true)
+: Job γ := Job.ofTask $
+ self.task.bind (prio := prio) (sync := true) fun rx =>
+ other.task.map (prio := prio) (sync := sync) fun ry =>
+ f rx ry
+
+/--
+`a.zipWith f b` produces a new job `c` that applies `f` to the
+results of `a` and `b`. The job `c` errors if either `a` or `b` error.
+-/
+@[inline] def zipWith
+ (f : α → β → γ) (self : Job α) (other : Job β)
+ (prio := Task.Priority.default) (sync := true)
+: Job γ :=
+ self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
+ | .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
+ | ra, rb => .error 0 (ra.state.merge rb.state)
+
+/-- Merges this job with another, discarding its output and trace. -/
+def add (self : Job α) (other : Job β) : Job α :=
+ self.zipResultWith (other := other) fun
+ | .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
+ | ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
+
+/-- Merges this job with another, discarding both outputs. -/
+def mix (self : Job α) (other : Job β) : Job Unit :=
+ self.zipWith (fun _ _ => ()) other
+
+/-- Merge a `List` of jobs into one, discarding their outputs. -/
+def mixList (jobs : List (Job α)) : Job Unit :=
+ jobs.foldr (·.mix ·) nil
+
+/-- Merge an `Array` of jobs into one, discarding their outputs. -/
+def mixArray (jobs : Array (Job α)) : Job Unit :=
+ jobs.foldl (·.mix ·) nil
+
+/-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
+def collectList (jobs : List (Job α)) : Job (List α) :=
+ jobs.foldr (zipWith List.cons) (pure [])
+
+/-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
+def collectArray (jobs : Array (Job α)) : Job (Array α) :=
+ jobs.foldl (zipWith Array.push) (pure (Array.mkEmpty jobs.size))
+
+end Job
+
+/-! ## BuildJob (deprecated) -/
+
+/-- A Lake build job. -/
+abbrev BuildJob α := Job α
+
+namespace BuildJob
+
+@[inline, deprecated "Obsolete." (since := "2024-12-06")]
+def mk (job : Job (α × BuildTrace)) : BuildJob α :=
+ job.mapOk fun (a, trace) s => .ok a {s with trace}
+
+@[inline, deprecated "Obsolete." (since := "2024-12-06")]
+def ofJob (job : Job BuildTrace) : BuildJob Unit :=
+ job.mapOk fun trace s => .ok () {s with trace}
+
+abbrev toJob (self : BuildJob α) : Job α :=
+ self
+
+@[deprecated Job.nil (since := "2024-12-06")]
+abbrev nil : BuildJob Unit :=
+ Job.pure ()
+
+@[deprecated Job.map (since := "2024-12-06")]
+protected abbrev pure (a : α) : BuildJob α :=
+ Job.pure a
+
+instance : Pure BuildJob := ⟨Job.pure⟩
+
+@[deprecated Job.map (since := "2024-12-06")]
+protected abbrev map (f : α → β) (self : BuildJob α) : BuildJob β :=
+ self.toJob.map f
+
+instance : Functor BuildJob where
+ map := Job.map
+
+@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
+def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
+ self.toJob.mapOk fun a s =>
+ let (b, trace) := f a s.trace
+ .ok b {s with trace}
+
+@[inline, deprecated Job.mapM (since := "2024-12-06")]
+protected def bindSync
+ (self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
+ (prio : Task.Priority := .default) (sync := false)
+: SpawnM (Job β) :=
+ self.toJob.mapM (prio := prio) (sync := sync) fun a => do
+ let (b, trace) ← f a (← getTrace)
+ setTrace trace
+ return b
+
+@[inline, deprecated Job.bindM (since := "2024-12-06")]
+protected def bindAsync
+ (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
+ (prio : Task.Priority := .default) (sync := false)
+ : SpawnM (Job β) :=
+ self.toJob.bindM (prio := prio) (sync := sync) fun a => do
+ f a (← getTrace)
+
+@[deprecated Job.wait? (since := "2024-12-06")]
+protected abbrev wait? (self : BuildJob α) : BaseIO (Option α) :=
+ self.toJob.wait?
+
+@[deprecated Job.add (since := "2024-12-06")]
+abbrev add (self : BuildJob α) (other : BuildJob β) : BuildJob α :=
+ self.toJob.add other.toJob
+
+@[deprecated Job.mix (since := "2024-12-06")]
+abbrev mix (self : BuildJob α) (other : BuildJob β) : BuildJob Unit :=
+ self.toJob.mix other.toJob
+
+@[deprecated Job.mixList (since := "2024-12-06")]
+abbrev mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) :=
+ return Job.mixList jobs
+
+@[deprecated Job.mixArray (since := "2024-12-06")]
+abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
+ return Job.mixArray jobs
+
+@[deprecated Job.zipWith (since := "2024-12-06")]
+abbrev zipWith
+ (f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
+: BuildJob γ :=
+ self.toJob.zipWith f other.toJob
+
+@[deprecated Job.collectList (since := "2024-12-06")]
+abbrev collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
+ return Job.collectList jobs
+
+@[deprecated Job.collectArray (since := "2024-12-06")]
+abbrev collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
+ return Job.collectArray jobs
+
+attribute [deprecated Job (since := "2024-12-06")] BuildJob
diff --git a/src/lake/Lake/Build/Job/Register.lean b/src/lake/Lake/Build/Job/Register.lean
new file mode 100644
index 0000000000..2502b08c29
--- /dev/null
+++ b/src/lake/Lake/Build/Job/Register.lean
@@ -0,0 +1,78 @@
+/-
+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 Lake.Build.Fetch
+
+/-! # Job Registration -/
+
+namespace Lake
+
+/--
+Resets the job state after a checkpoint (e.g., registering the job).
+Preserves state that downstream jobs want to depend on while resetting
+job-local state that should not be inherited by downstream jobs.
+-/
+@[inline] def JobState.renew (s : JobState) : JobState where
+ trace := s.trace
+
+/--
+Resets the job's state after a checkpoint (e.g., registering the job).
+Preserves information that downstream jobs want to depend on while resetting
+job-local information that should not be inherited by downstream jobs.
+-/
+def Job.renew (self : Job α) : Job α :=
+ self.mapResult (sync := true) fun
+ | .ok a s => .ok a s.renew
+ | .error _ s => .error 0 s.renew
+
+/--
+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
+
+/-- Wraps stray I/O, logs, and errors in `x` into the produced job. -/
+def ensureJob (x : FetchM (Job α))
+: FetchM (Job α) := fun fetch stack store ctx log => do
+ let iniPos := log.endPos
+ match (← (withLoggedIO x) fetch stack store ctx log) 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 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
diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean
index b6e5962ca6..688ea14fb1 100644
--- a/src/lake/Lake/Build/Topological.lean
+++ b/src/lake/Lake/Build/Topological.lean
@@ -47,12 +47,12 @@ we equip the monad `m` with a fetch function of its own.
-/
/-- A transformer that equips a monad with a `DFetchFn`. -/
-abbrev DFetchT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+abbrev DFetchFnT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
EquipT (DFetchFn α β m) m
-/-- A `DFetchT` that is not dependently typed. -/
-abbrev FetchT (α : Type u) (β : Type v) (m : Type v → Type w) :=
- DFetchT α (fun _ => β) m
+/-- A `DFetchFnT` that is not dependently typed. -/
+abbrev FetchFnT (α : Type u) (β : Type v) (m : Type v → Type w) :=
+ DFetchFnT α (fun _ => β) m
/-!
We can then use the such a monad as the basis for a fetch function itself.
@@ -64,11 +64,11 @@ fetch values. It is thus usually implemented recursively via some variation
of the `recFetch` function below, hence the "rec" in both names.
-/
abbrev DRecFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
- DFetchFn α β (DFetchT α β m)
+ DFetchFn α β (DFetchFnT α β m)
/-- A `DRecFetchFn` that is not dependently typed. -/
abbrev RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
- α → FetchT α β m β
+ α → FetchFnT α β m β
/-- A `DFetchFn` that provides its base `DRecFetchFn` with itself. -/
@[specialize] partial def recFetch
diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean
index 52887ab50a..eb777c9cbe 100644
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@@ -5,6 +5,7 @@ Authors: Mac Malone
-/
prelude
import Lake.Config.Monad
+import Lake.Build.Job
import Lake.CLI.Error
namespace Lake
diff --git a/src/lake/Lake/Config/ExternLibConfig.lean b/src/lake/Lake/Config/ExternLibConfig.lean
index 9ba4205e6d..3f9b47d8e8 100644
--- a/src/lake/Lake/Config/ExternLibConfig.lean
+++ b/src/lake/Lake/Config/ExternLibConfig.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
namespace Lake
open Lean System
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index 3e11a65e76..c1b78c1adc 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -267,6 +267,7 @@ end MonadLogT
/- A Lake log. An `Array` of log entries. -/
structure Log where
entries : Array LogEntry
+ deriving Inhabited
instance : ToJson Log := ⟨(toJson ·.entries)⟩
instance : FromJson Log := ⟨(Log.mk <$> fromJson? ·)⟩