diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean
index a7e62e838ca1..93b5b502e1fb 100644
--- a/src/lake/Lake/Build/Basic.lean
+++ b/src/lake/Lake/Build/Basic.lean
@@ -24,68 +24,170 @@ structure BuildConfig where
   noBuild : Bool := false
   verbosity : Verbosity := .normal
   /--
-  Fail the top-level build if warnings have been logged.
-  Unlike some build systems, this does **NOT** convert warnings to errors,
-  and it does not abort jobs when warnings are logged (i.e., dependent jobs
-  will still continue unimpeded).
+  Fail the top-level build if entries of at least this level have been logged.
+
+  Unlike some build systems, this does **NOT** convert such log entries to
+  errors, and it does not abort jobs when warnings are logged (i.e.,
+  dependent jobs will still continue unimpeded).
+  -/
+  failLv : LogLevel := .error
+  /--
+  The stream to which Lake reports build progress.
+  By default, Lake uses `stderr`.
   -/
-  failIfWarnings : Bool := false
-  /-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
-  useStdout : Bool := false
+  out : OutStream := .stderr
+  /-- Whether to use ANSI escape codes in build output. -/
+  ansiMode : AnsiMode := .auto
+
+/-- The minimum log level for an log entry to be reported. -/
+@[inline] def BuildConfig.outLv (cfg : BuildConfig) : LogLevel :=
+  cfg.verbosity.minLogLv
+
+/--
+Whether the build should show progress information.
+
+`Verbosity.quiet` hides progress and, for a `noBuild`,
+`Verbosity.verbose` shows progress.
+-/
+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
+
+@[inline] 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"
+
+/-- 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
+
+/--
+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 (_ : JobState) : JobState where
+  log := {}
+  action := .unknown
+
+def JobState.merge (a b : JobState) : JobState where
+  log := a.log ++ b.log
+  action := a.action.merge b.action
+
+@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) :=
+  {s with log := f s.log}
+
+/-- The result of a Lake job. -/
+abbrev JobResult α := EResult Log.Pos JobState α
 
-abbrev JobResult α := ELogResult α
+/-- The `Task` of a Lake job. -/
 abbrev JobTask α := BaseIOTask (JobResult α)
 
 /-- A Lake job. -/
 structure Job (α : Type u)  where
   task : JobTask α
+  caption : String
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  registeredJobs : IO.Ref (Array (String × Job Unit))
+  registeredJobs : IO.Ref (Array (Job Unit))
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
 
+/-- The monad of asynchronous Lake jobs. Lifts into `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
 
-@[inline] def getBuildContext [Monad m] : BuildT m BuildContext :=
+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}
+
+/-- A monad equipped with a Lake build context. -/
+abbrev MonadBuild (m : Type → Type u) :=
+  MonadReaderOf BuildContext m
+
+@[inline] def getBuildContext [MonadBuild m] : m BuildContext :=
   readThe BuildContext
 
-@[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
+@[inline] def getLeanTrace [Functor m] [MonadBuild m] : m BuildTrace :=
   (·.leanTrace) <$> getBuildContext
 
-@[inline] def getBuildConfig [Monad m] : BuildT m BuildConfig :=
+@[inline] def getBuildConfig [Functor m] [MonadBuild m] : m BuildConfig :=
   (·.toBuildConfig) <$> getBuildContext
 
-@[inline] def getIsOldMode [Monad m] : BuildT m Bool :=
+@[inline] def getIsOldMode [Functor m] [MonadBuild m] : m Bool :=
   (·.oldMode) <$> getBuildConfig
 
-@[inline] def getTrustHash [Monad m] : BuildT m Bool :=
+@[inline] def getTrustHash [Functor m] [MonadBuild m] : m Bool :=
   (·.trustHash) <$> getBuildConfig
 
-@[inline] def getNoBuild [Monad m] : BuildT m Bool :=
+@[inline] def getNoBuild [Functor m] [MonadBuild m] : m Bool :=
   (·.noBuild) <$> getBuildConfig
 
-@[inline] def getVerbosity [Monad m] : BuildT m Verbosity :=
+@[inline] def getVerbosity [Functor m] [MonadBuild m] : m Verbosity :=
   (·.verbosity) <$> getBuildConfig
 
-@[inline] def getIsVerbose [Monad m] : BuildT m Bool :=
+@[inline] def getIsVerbose [Functor m] [MonadBuild m] : m Bool :=
   (· == .verbose) <$> getVerbosity
 
-@[inline] def getIsQuiet [Monad m] : BuildT m Bool :=
+@[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
 
-/-- The monad of asynchronous Lake jobs. -/
-abbrev JobM := CoreBuildM
-
 /-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
 abbrev SpawnM := BuildT BaseIO
 
 /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
 @[deprecated SpawnM] abbrev SchedulerM := SpawnM
+
+/--
+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] def logStep (message : String) : JobM Unit := do
+  logVerbose message
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 8a316fac8875..cdeb36a11908 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -24,13 +24,23 @@ and will be rebuilt on different host platforms.
 -/
 def platformTrace := pureHash System.Platform.target
 
-/-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
+/--
+Checks if the `info` is up-to-date by comparing `depTrace` with `traceFile`.
+If old mode is enabled (e.g., `--old`), uses the modification time of `oldTrace`
+as the point of comparison instead.
+-/
 @[specialize] def BuildTrace.checkUpToDate
   [CheckExists ι] [GetMTime ι]
   (info : ι) (depTrace : BuildTrace) (traceFile : FilePath)
+  (oldTrace := depTrace)
 : JobM Bool := do
   if (← getIsOldMode) then
-    depTrace.checkAgainstTime info
+    if (← oldTrace.checkAgainstTime info) then
+      return true
+    else if let some hash ← Hash.load? traceFile then
+      depTrace.checkAgainstHash info hash
+    else
+      return false
   else
     depTrace.checkAgainstFile info traceFile
 
@@ -42,12 +52,14 @@ Returns whether `info` was already up-to-date.
 @[inline] def buildUnlessUpToDate?
   [CheckExists ι] [GetMTime ι] (info : ι)
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+  (action : JobAction := .build) (oldTrace := depTrace)
 : JobM Bool := do
-  if (← depTrace.checkUpToDate info traceFile) then
+  if (← depTrace.checkUpToDate info traceFile oldTrace) then
     return true
   else if (← getNoBuild) then
     IO.Process.exit noBuildCode.toUInt8
   else
+    updateAction action
     build
     depTrace.writeToFile traceFile
     return false
@@ -122,6 +134,7 @@ def buildFileUnlessUpToDate
   let logFile := FilePath.mk <| file.toString ++ ".log.json"
   let build := cacheBuildLog logFile build
   if (← buildUnlessUpToDate? file depTrace traceFile build) then
+    updateAction .replay
     replayBuildLog logFile
     fetchFileTrace file
   else
diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean
index 8a97de3d74ec..e751ae4265d1 100644
--- a/src/lake/Lake/Build/Executable.lean
+++ b/src/lake/Lake/Build/Executable.lean
@@ -12,7 +12,7 @@ The build function definition for a Lean executable.
 -/
 
 def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
-  withRegisterJob s!"Linking {self.fileName}" do
+  withRegisterJob s!"{self.name}" do
   let imports ← self.root.transImports.fetch
   let mut linkJobs := #[← self.root.o.fetch]
   for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 95013cbc8264..44c8efd3c3ad 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -116,6 +116,13 @@ module_data o.noexport : BuildJob FilePath
 
 /-! ## Package Facets -/
 
+/--
+A package's *optional* cloud build release.
+Does not fail if the release cannot be fetched.
+-/
+abbrev Package.optReleaseFacet := `optRelease
+package_data optRelease : BuildJob Bool
+
 /-- A package's cloud build release. -/
 abbrev Package.releaseFacet := `release
 package_data release : BuildJob Unit
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index b0129718cf64..977bca9c6fad 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -23,12 +23,7 @@ namespace Lake
 abbrev RecBuildM :=
   CallStackT BuildKey <| BuildT <| ELogT <| StateT BuildStore <| BaseIO
 
-instance : MonadLift IO RecBuildM := ⟨MonadError.runIO⟩
-
-@[inline] def RecBuildM.runLogIO (x : LogIO α) : RecBuildM α :=
-  fun _ _ log store => (·, store) <$> x log
-
-instance : MonadLift LogIO RecBuildM := ⟨RecBuildM.runLogIO⟩
+instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
 
 /-- Run a recursive build. -/
 @[inline] def RecBuildM.run
@@ -64,7 +59,7 @@ abbrev FetchM := IndexT RecBuildM
 @[deprecated FetchM] abbrev IndexBuildM := FetchM
 
 /-- The old build monad. **Uses should generally be replaced by `FetchM`.** -/
-@[deprecated FetchM] abbrev BuildM := CoreBuildM
+@[deprecated FetchM] 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 α :=
@@ -72,19 +67,46 @@ abbrev FetchM := IndexT RecBuildM
 
 export BuildInfo (fetch)
 
-/-- Register the produced job for the CLI progress UI.  -/
-def withRegisterJob
-  (caption : String) (x : FetchM (Job α))
+/-- 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, store) =>
     let (log, jobLog) := log.split iniPos
-    let regJob := job.mapResult (discard <| ·.modifyState (jobLog ++  ·))
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok job.clearLog log, store)
+    let job := if jobLog.isEmpty then job else job.mapResult (sync := true)
+      (·.modifyState (.modifyLog (jobLog ++  ·)))
+    return (.ok job log, store)
   | (.error _ log, store) =>
     let (log, jobLog) := log.split iniPos
-    let regJob := ⟨Task.pure <| .error 0 jobLog⟩
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok .error log, store)
+    return (.ok (.error jobLog) log, store)
+
+/--
+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.
+-/
+@[inline] def withRegisterJob
+  (caption : String) (x : FetchM (Job α))
+: FetchM (Job α) := do
+  let job ← ensureJob x
+  let job := job.setCaption caption
+  let regJob := job.mapResult (sync := true) discard
+  (← readThe BuildContext).registeredJobs.modify (·.push regJob)
+  return job.renew
+
+/--
+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
+  (fallbackCaption : String) (job : Job α)
+: FetchM (Job α) := do
+  if job.caption.isEmpty then
+    let job := job.setCaption fallbackCaption
+    let regJob := job.mapResult (sync := true) discard
+    (← readThe BuildContext).registeredJobs.modify (·.push regJob)
+    return job.renew
+  else
+    return job
diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean
index 14d93a232a1b..f0b2895552d3 100644
--- a/src/lake/Lake/Build/Imports.lean
+++ b/src/lake/Lake/Build/Imports.lean
@@ -19,7 +19,7 @@ by `lake lean` to build the imports of a file.
 Returns the set of module dynlibs built (so they can be loaded by Lean).
 -/
 def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
-  withRegisterJob s!"Building imports of '{leanFile}'" do
+  withRegisterJob s!"imports ({leanFile})" do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
     (← getRootPackage).extraDep.fetch <&> (·.map fun _ => #[])
diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean
index 22a536ccb157..31f5516eb064 100644
--- a/src/lake/Lake/Build/Index.lean
+++ b/src/lake/Lake/Build/Index.lean
@@ -29,15 +29,15 @@ dynamically-typed equivalent.
   cast (by rw [← h.family_key_eq_type]) build
 
 def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (BuildJob FilePath) :=
-  withRegisterJob s!"Building {lib.staticTargetName.toString}" do
+  withRegisterJob s!"{lib.staticTargetName.toString}:static" do
   lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
 
 def ExternLib.recBuildShared (lib : ExternLib) : FetchM (BuildJob FilePath) :=
-  withRegisterJob s!"Linking {lib.staticTargetName.toString}" do
+  withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
   buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
 
 def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (BuildJob Dynlib) := do
-  withRegisterJob s!"Computing {lib.staticTargetName.toString} dynlib" do
+  withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
   computeDynlibOfShared (← lib.shared.fetch)
 
 /-!
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index cb2aa08e616f..9427e367b1e2 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -220,6 +220,10 @@ abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
 abbrev Package.release (self : Package) : BuildInfo :=
   self.facet releaseFacet
 
+@[inherit_doc optReleaseFacet]
+abbrev Package.optRelease (self : Package) : BuildInfo :=
+  self.facet optReleaseFacet
+
 @[inherit_doc extraDepFacet]
 abbrev Package.extraDep (self : Package) : BuildInfo :=
   self.facet extraDepFacet
diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean
index 3e5a5c7d216c..3ea28eebf872 100644
--- a/src/lake/Lake/Build/Job.lean
+++ b/src/lake/Lake/Build/Job.lean
@@ -12,23 +12,39 @@ namespace Lake
 
 namespace Job
 
-@[inline] protected def pure (a : α) : Job α :=
-  {task := Task.pure (.ok a {})}
+@[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 : Job Unit :=
-  pure ()
+@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
+  .pure () log caption
+
+/-- Sets the job's caption. -/
+@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
+  {job with caption}
 
-@[inline] protected def error (l : Log := {}) : Job α :=
-  {task := Task.pure (.error 0 l)}
+/-- 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 β :=
-  {task := self.task.map f prio sync}
+  {self with task := self.task.map f prio sync}
+
+@[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 α)
@@ -38,25 +54,20 @@ instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
 
 instance : Functor Job where map := Job.map
 
-@[inline] def clearLog (self : Job α) : Job α :=
-  self.mapResult (sync := true) fun
-  | .ok a _ => .ok a {}
-  | .error .. => .error 0 {}
-
-@[inline] def attempt (self : Job α) : Job Bool :=
-  self.mapResult (sync := true) fun
-  | .error n l => .ok false (l.dropFrom n)
-  | .ok _ l => .ok true l
-
-@[inline] def attempt? (self : Job α) : Job (Option α) :=
+/--
+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
-  | .error n l => .ok none (l.dropFrom n)
-  | .ok a l => .ok (some a) l
+  | .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 => Job.mk <$> do
+: SpawnM (Job α) := fun ctx => .ofTask <$> do
   BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
 
 /-- Wait a the job to complete and return the result. -/
@@ -76,8 +87,8 @@ 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 l => l.replay; throw n
-  | .ok a l => l.replay; pure a
+  | .error n {log, ..} => log.replay; throw n
+  | .ok a {log, ..} => log.replay; pure a
 
 /--
 `let c ← a.bindSync b` asynchronously performs the action `b`
@@ -86,10 +97,10 @@ after the job `a` completes.
 @[inline] protected def bindSync
   (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := fun ctx => Job.mk <$> do
-  BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun
-    | EResult.ok a l => (withLoggedIO (f a)) ctx l
-    | EResult.error n l => return .error n l
+: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
+  BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
+    | EResult.ok a s => (withLoggedIO (f a)) ctx s
+    | EResult.error n s => return .error n s
 
 /--
 `let c ← a.bindAsync b` asynchronously performs the action `b`
@@ -98,14 +109,13 @@ after the job `a` completes and then merges into the job produced by `b`.
 @[inline] protected def bindAsync
   (self : Job α) (f : α → SpawnM (Job β))
   (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := fun ctx => Job.mk <$> do
-  BaseIO.bindTask self.task (prio := prio) (sync := sync) fun
-    | .ok a l => do
+: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
+  BaseIO.bindTask task (prio := prio) (sync := sync) fun
+    | .ok a sa => do
       let job ← f a ctx
-      if l.isEmpty then return job.task else
       return job.task.map (prio := prio) (sync := true) fun
-      | EResult.ok a l' => .ok a (l ++ l')
-      | EResult.error n l' => .error ⟨l.size + n.val⟩ (l ++ l')
+      | EResult.ok a sb => .ok a (sa.merge sb)
+      | EResult.error n sb => .error ⟨sa.log.size + n.val⟩ (sa.merge sb)
     | .error n l => return Task.pure (.error n l)
 
 /--
@@ -115,12 +125,12 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 @[inline] def zipWith
   (f : α → β → γ) (x : Job α) (y : Job β)
   (prio := Task.Priority.default) (sync := false)
-: BaseIO (Job γ) := Job.mk <$> do
-  BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx =>
-  BaseIO.mapTask (t := y.task) (prio := prio) (sync := sync) fun ry =>
+: Job γ := Job.ofTask $
+  x.task.bind (prio := prio) (sync := true) fun rx =>
+  y.task.map (prio := prio) (sync := sync) fun ry =>
   match rx, ry with
-  | .ok a la, .ok b lb => return .ok (f a b) (la ++ lb)
-  | rx, ry => return .error 0 (rx.state ++ ry.state)
+  | .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
+  | rx, ry => .error 0 (rx.state.merge ry.state)
 
 end Job
 
@@ -146,16 +156,6 @@ namespace BuildJob
 
 instance : Pure BuildJob := ⟨BuildJob.pure⟩
 
-@[inline] def attempt (self : BuildJob α) : BuildJob Bool :=
-  {task := self.toJob.task.map fun
-    | .error _ l => .ok (false, nilTrace) l
-    | .ok (_, t) l => .ok (true, t) l}
-
-@[inline] def attempt? (self : BuildJob α) : BuildJob (Option α) :=
-  {task := self.toJob.task.map fun
-    | .error _ l => .ok (none, nilTrace) l
-    | .ok (a, t) l => .ok (some a, t) l}
-
 @[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
   mk <| (fun (a,t) => (f a,t)) <$> self.toJob
 
@@ -180,25 +180,25 @@ instance : Functor BuildJob where
 @[inline] protected def wait? (self : BuildJob α) : BaseIO (Option α) :=
   (·.map (·.1)) <$> self.toJob.wait?
 
-def add (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob α) :=
-  mk <$> t1.toJob.zipWith (fun a _ => a) t2.toJob
+def add (t1 : BuildJob α) (t2 : BuildJob β) : BuildJob α :=
+  mk <| t1.toJob.zipWith (fun a _ => a) t2.toJob
 
-def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
-  mk <$> t1.toJob.zipWith (fun (_,t) (_,t') => ((), mixTrace t t')) t2.toJob
+def mix (t1 : BuildJob α) (t2 : BuildJob β) : BuildJob Unit :=
+  mk <| t1.toJob.zipWith (fun (_,t) (_,t') => ((), mixTrace t t')) t2.toJob
 
-def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
-  jobs.foldrM (·.toJob.zipWith (fun (_,t') t => mixTrace t t') ·) (pure nilTrace)
+def mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) := ofJob $
+  jobs.foldr (·.toJob.zipWith (fun (_,t') t => mixTrace t t') ·) (pure nilTrace)
 
-def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
-  jobs.foldlM (·.zipWith (fun t (_,t') => mixTrace t t') ·.toJob) (pure nilTrace)
+def mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) := ofJob $
+  jobs.foldl (·.zipWith (fun t (_,t') => mixTrace t t') ·.toJob) (pure nilTrace)
 
-protected def zipWith
+def zipWith
   (f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β)
-: BaseIO (BuildJob γ) :=
-  mk <$> t1.toJob.zipWith (fun (a,t) (b,t') => (f a b, mixTrace t t'))  t2.toJob
+: BuildJob γ :=
+  mk <| t1.toJob.zipWith (fun (a,t) (b,t') => (f a b, mixTrace t t')) t2.toJob
 
-def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) :=
-  jobs.foldrM (BuildJob.zipWith List.cons) (pure [])
+def collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
+  return jobs.foldr (zipWith List.cons) (pure [])
 
-def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) :=
-  jobs.foldlM (BuildJob.zipWith Array.push) (pure #[])
+def collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
+  return jobs.foldl (zipWith Array.push) (pure #[])
diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean
index 6b1ebd9377ef..c3b540d01cfe 100644
--- a/src/lake/Lake/Build/Key.lean
+++ b/src/lake/Lake/Build/Key.lean
@@ -23,6 +23,18 @@ def toString : (self : BuildKey) → String
 | targetFacet p t f => s!"{p}/{t}:{f}"
 | customTarget p t => s!"{p}/{t}"
 
+/-- Like the default `toString`, but without disambiguation markers. -/
+def toSimpleString : (self : BuildKey) → String
+| moduleFacet m f => s!"{m}:{f}"
+| packageFacet p f => s!"{p}:{f}"
+| targetFacet p t f => s!"{p}/{t}:{eraseHead f}"
+| customTarget p t => s!"{p}/{t}"
+where
+  eraseHead : Name → Name
+    | .anonymous | .str .anonymous _  | .num .anonymous _  => .anonymous
+    | .str p s => .str (eraseHead p) s
+    | .num p s => .num (eraseHead p) s
+
 instance : ToString BuildKey := ⟨(·.toString)⟩
 
 def quickCmp (k k' : BuildKey) : Ordering :=
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 49b66f9ae743..6c48bddc08e4 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -45,7 +45,7 @@ protected def LeanLib.recBuildLean
 (self : LeanLib) : FetchM (BuildJob Unit) := do
   let mods ← self.modules.fetch
   mods.foldlM (init := BuildJob.nil) fun job mod => do
-    job.mix <| ← mod.leanArts.fetch
+    return job.mix <| ← mod.leanArts.fetch
 
 /-- The `LibraryFacetConfig` for the builtin `leanArtsFacet`. -/
 def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
@@ -53,8 +53,12 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
 
 @[specialize] protected def LeanLib.recBuildStatic
 (self : LeanLib) (shouldExport : Bool) : FetchM (BuildJob FilePath) := do
-  let exports := if shouldExport then "w/ exports" else "w/o exports"
-  withRegisterJob s!"Building {self.staticLibFileName} ({exports})" do
+  let suffix :=
+    if (← getIsVerbose) then
+      if shouldExport then " (with exports)" else " (without exports)"
+    else
+      ""
+  withRegisterJob s!"{self.name}:static{suffix}" do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
@@ -74,7 +78,7 @@ def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet :=
 
 protected def LeanLib.recBuildShared
 (self : LeanLib) : FetchM (BuildJob FilePath) := do
-  withRegisterJob s!"Linking {self.sharedLibFileName}" do
+  withRegisterJob s!"{self.name}:shared" do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
     mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
@@ -91,7 +95,7 @@ def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
 /-- Build the `extraDepTargets` for the library and its package. -/
 def LeanLib.recBuildExtraDepTargets (self : LeanLib) : FetchM (BuildJob Unit) := do
   self.extraDepTargets.foldlM (init := ← self.pkg.extraDep.fetch) fun job target => do
-    job.mix <| ← self.pkg.fetchTargetJob target
+    return job.mix <| ← self.pkg.fetchTargetJob target
 
 /-- The `LibraryFacetConfig` for the builtin `extraDepFacet`. -/
 def LeanLib.extraDepFacetConfig : LibraryFacetConfig extraDepFacet :=
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 267d5a88a83f..d79ee7de3b08 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -149,12 +149,12 @@ Fetch its dependencies and then elaborate the Lean source file, producing
 all possible artifacts (i.e., `.olean`, `ilean`, `.c`, and `.bc`).
 -/
 def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
-  withRegisterJob s!"Building {mod.name}" do
+  withRegisterJob mod.name.toString do
   (← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
     let argTrace : BuildTrace := pureHash mod.leanArgs
     let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
     let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-    let upToDate ← buildUnlessUpToDate? mod modTrace mod.traceFile do
+    let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace) mod modTrace mod.traceFile do
       let hasLLVM := Lean.Internal.hasLLVMBackend ()
       let bcFile? := if hasLLVM then some mod.bcFile else none
       cacheBuildLog mod.logFile do
@@ -166,6 +166,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
       if hasLLVM then
         discard <| cacheFileHash mod.bcFile
     if upToDate then
+      updateAction .replay
       replayBuildLog mod.logFile
     return ((), depTrace)
 
@@ -203,8 +204,9 @@ def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
 Recursively build the module's object file from its C file produced by `lean`
 with `-DLEAN_EXPORTING` set, which exports Lean symbols defined within the C files.
 -/
-def Module.recBuildLeanCToOExport (self : Module) : FetchM (BuildJob FilePath) :=
-  withRegisterJob s!"Compiling {self.name}" do
+def Module.recBuildLeanCToOExport (self : Module) : FetchM (BuildJob FilePath) := do
+  let suffix := if (← getIsVerbose) then " (with exports)" else ""
+  withRegisterJob s!"{self.name}:c.o{suffix}" do
   -- TODO: add option to pass a target triplet for cross compilation
   let leancArgs := self.leancArgs ++ #["-DLEAN_EXPORTING"]
   buildLeanO self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
@@ -217,8 +219,9 @@ def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
 Recursively build the module's object file from its C file produced by `lean`.
 This version does not export any Lean symbols.
 -/
-def Module.recBuildLeanCToONoExport (self : Module) : FetchM (BuildJob FilePath) :=
-  withRegisterJob s!"Compiling {self.name}" do
+def Module.recBuildLeanCToONoExport (self : Module) : FetchM (BuildJob FilePath) := do
+  let suffix := if (← getIsVerbose) then " (without exports)" else ""
+  withRegisterJob s!"{self.name}:c.o{suffix}" do
   -- TODO: add option to pass a target triplet for cross compilation
   buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
 
@@ -233,7 +236,7 @@ def Module.coFacetConfig : ModuleFacetConfig coFacet :=
 
 /-- Recursively build the module's object file from its bitcode file produced by `lean`. -/
 def Module.recBuildLeanBcToO (self : Module) : FetchM (BuildJob FilePath) := do
-  withRegisterJob s!"Compiling {self.name}" do
+  withRegisterJob s!"{self.name}:bc.o" do
   -- TODO: add option to pass a target triplet for cross compilation
   buildLeanO self.bcoFile (← self.bc.fetch) self.weakLeancArgs self.leancArgs
 
@@ -265,7 +268,7 @@ def Module.oFacetConfig : ModuleFacetConfig oFacet :=
 -- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`
 /-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/
 def Module.recBuildDynlib (mod : Module) : FetchM (BuildJob Dynlib) :=
-  withRegisterJob s!"Linking {mod.name} dynlib" do
+  withRegisterJob s!"{mod.name}:dynlib" do
 
   -- Compute dependencies
   let transImports ← mod.transImports.fetch
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index 6652e291a79e..8e20ab14ecbb 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -32,16 +32,16 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
   let mut job := BuildJob.nil
   -- Build dependencies' extra dep targets
   for dep in self.deps do
-    job ← job.mix <| ← dep.extraDep.fetch
+    job := job.mix <| ← dep.extraDep.fetch
   -- Fetch pre-built release if desired and this package is a dependency
   if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
-    job ← job.add <| ← (← self.release.fetch).attempt.bindSync fun success t => do
+    job := job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do
       unless success do
-        logWarning "fetching cloud release failed; falling back to local build"
+        logWarning "failed to fetch cloud release; falling back to local build"
       return ((), t)
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
-    job ← job.mix <| ← self.fetchTargetJob target
+    job := job.mix <| ← self.fetchTargetJob target
   return job
 
 /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
@@ -49,31 +49,42 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) :=
-  withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do
+def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
+  updateAction .fetch
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
-    | error <| s!"{self.name}: wanted prebuilt release, " ++
-      "but package's repository URL was not known; it may need to set `releaseRepo?`"
+    | logInfo s!"{self.name}: wanted prebuilt release, \
+        but package's repository URL was not known; it may need to set 'releaseRepo'"
+      return (false, .nil)
   let some tag ← repo.findTag?
-    | error <| s!"{self.name}: wanted prebuilt release, " ++
-      "but could not find an associated tag for the package's revision"
+    | logInfo s!"{self.name}: wanted prebuilt release, \
+        but could not find an associated tag for the package's revision"
+      return (false, .nil)
   let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
   let logName := s!"{self.name}/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
   let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
-  let upToDate ← buildUnlessUpToDate? self.buildArchiveFile depTrace traceFile do
+  let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
     logVerbose s!"downloading {logName}"
     download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do
     logVerbose s!"unpacking {logName}"
     untar self.buildArchiveFile self.buildDir
-  return ((), .nil)
+  return (true, .nil)
+
+/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
+def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
+  mkFacetJobConfig (·.fetchOptRelease)
 
 /-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
 def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
-  mkFacetJobConfig (·.fetchRelease)
+  mkFacetJobConfig fun pkg =>
+    withRegisterJob s!"{pkg.name}:release" do
+      (← pkg.optRelease.fetch).bindSync fun success t => do
+        unless success do
+          error "failed to fetch cloud release"
+        return ((), t)
 
 /-- Perform a build job after first checking for a cloud release for the package. -/
 def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
@@ -98,4 +109,5 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
   DNameMap.empty
   |>.insert depsFacet depsFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
+  |>.insert optReleaseFacet optReleaseFacetConfig
   |>.insert releaseFacet releaseFacetConfig
diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean
index a795bf28172f..01e8eedb642c 100644
--- a/src/lake/Lake/Build/Run.lean
+++ b/src/lake/Lake/Build/Run.lean
@@ -25,6 +25,150 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext
     leanTrace := Hash.ofString ws.lakeEnv.leanGithash
   }
 
+/-- Context of the Lake build monitor. -/
+structure MonitorContext where
+  totalJobs : Nat
+  out : IO.FS.Stream
+  outLv : LogLevel
+  failLv : LogLevel
+  showProgress : Bool
+  useAnsi : Bool
+  /-- How often to poll jobs (in milliseconds). -/
+  updateFrequency : Nat := 100
+
+/-- State of the Lake build monitor. -/
+structure MonitorState where
+  jobNo : Nat := 1
+  jobs : Array (Job Unit)
+  failures : Array String
+  resetCtrl : String
+  lastUpdate : Nat
+
+/-- Monad of the Lake build monitor. -/
+abbrev MonitorM := ReaderT MonitorContext <| StateT MonitorState BaseIO
+
+@[inline] def MonitorM.run
+  (ctx : MonitorContext) (s : MonitorState) (self : MonitorM α)
+: BaseIO (α × MonitorState) :=
+  self ctx s
+
+/--
+The ANSI escape sequence for clearing the current line
+and resetting the cursor back to the start.
+-/
+def Ansi.resetLine : String :=
+  "\x1B[2K\r"
+
+/-- Like `IO.FS.Stream.flush`, but ignores errors. -/
+@[inline] def flush (out : IO.FS.Stream) : BaseIO PUnit :=
+  out.flush |>.catchExceptions fun _ => pure ()
+
+/-- Like `IO.FS.Stream.putStr`, but panics on errors. -/
+@[inline] def print! (out : IO.FS.Stream) (s : String) : BaseIO PUnit :=
+  out.putStr s |>.catchExceptions fun e =>
+    panic! s!"[{decl_name%} failed: {e}] {repr s}"
+
+namespace Monitor
+
+@[inline] def print (s : String) : MonitorM PUnit := do
+  print! (← read).out s
+
+@[inline] nonrec def flush : MonitorM PUnit := do
+  flush (← read).out
+
+def renderProgress : MonitorM PUnit := do
+  let {jobNo, jobs, ..} ← get
+  let {totalJobs, useAnsi, showProgress, ..} ← read
+  if showProgress ∧ useAnsi then
+    if h : 0 < jobs.size then
+      let caption := jobs[0]'h |>.caption
+      let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := Ansi.resetLine})
+      print s!"{resetCtrl}[{jobNo}/{totalJobs}] Checking {caption}"
+      flush
+
+def reportJob (job : Job Unit) : MonitorM PUnit := do
+  let {jobNo, ..} ← get
+  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, ..} ← read
+  let {log, action, ..} := job.task.get.state
+  let maxLv := log.maxLv
+  let failed := log.hasEntries ∧ maxLv ≥ failLv
+  if failed then
+    modify fun s => {s with failures := s.failures.push job.caption}
+  let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
+  if hasOutput ∨ (showProgress ∧ action ≥ .fetch) then
+    let verb := action.verb failed
+    let icon := if hasOutput then maxLv.icon else '✔'
+    let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {job.caption}"
+    let caption :=
+      if useAnsi then
+        let color := if hasOutput then maxLv.ansiColor else "32"
+        Ansi.chalk color caption
+      else
+        caption
+    let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
+    print s!"{resetCtrl}{caption}\n"
+    if hasOutput then
+      let outLv := if failed then .trace else outLv
+      log.replay (logger := .stream out outLv useAnsi)
+    flush
+
+def pollJobs : MonitorM PUnit := do
+  let prevJobs ← modifyGet fun s => (s.jobs, {s with jobs := #[]})
+  for h : i in [0:prevJobs.size] do
+    let job := prevJobs[i]'h.upper
+    if (← IO.hasFinished job.task) then
+      reportJob job
+      modify fun s => {s with jobNo := s.jobNo + 1}
+    else
+      modify fun s => {s with jobs := s.jobs.push job}
+
+def sleep : MonitorM PUnit := do
+  let now ← IO.monoMsNow
+  let lastUpdate ← modifyGet fun s => (s.lastUpdate, {s with lastUpdate := now})
+  let sleepTime : Nat := (← read).updateFrequency - (now - lastUpdate)
+  if sleepTime > 0 then
+    IO.sleep sleepTime.toUInt32
+
+partial def loop : MonitorM PUnit := do
+  renderProgress
+  pollJobs
+  if 0 < (← get).jobs.size then
+    renderProgress
+    sleep
+    loop
+
+def main : MonitorM PUnit := do
+  loop
+  let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
+  unless resetCtrl.isEmpty do
+    print resetCtrl
+    flush
+
+end Monitor
+
+/-- The job monitor function. An auxiliary definition for `runFetchM`. -/
+def monitorJobs
+  (jobs : Array (Job Unit))
+  (out : IO.FS.Stream)
+  (failLv outLv : LogLevel)
+  (useAnsi showProgress : Bool)
+  (resetCtrl : String := "")
+  (initFailures : Array String := #[])
+  (totalJobs := jobs.size)
+  (updateFrequency := 100)
+: BaseIO (Array String) := do
+  let ctx := {
+    totalJobs, out, failLv, outLv,
+    useAnsi, showProgress, updateFrequency
+  }
+  let s := {
+    jobs, resetCtrl
+    lastUpdate := ← IO.monoMsNow
+    failures := initFailures
+  }
+  let (_,s) ← Monitor.main.run ctx s
+  return s.failures
+
 /--
 Run a build function in the Workspace's context using the provided configuration.
 Reports incremental build progress and build logs. In quiet mode, only reports
@@ -33,62 +177,51 @@ failing build jobs (e.g., when using `-q` or non-verbose `--no-build`).
 def Workspace.runFetchM
   (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {})
 : IO α := do
+  -- Configure
+  let out ← cfg.out.get
+  let useAnsi ← cfg.ansiMode.isEnabled out
+  let outLv := cfg.outLv
+  let failLv := cfg.failLv
+  let showProgress := cfg.showProgress
+  let showAnsiProgress := showProgress ∧ useAnsi
   let ctx ← mkBuildContext ws cfg
-  let out ← if cfg.useStdout then IO.getStdout else IO.getStderr
-  let useANSI ← out.isTty
-  let verbosity := cfg.verbosity
-  let showProgress :=
-    (cfg.noBuild && verbosity == .verbose) ||
-    verbosity != .quiet
+  -- Job Computation
   let caption := "Computing build jobs"
-  let header := s!"[?/?] {caption}"
-  if showProgress then
-    out.putStr header; out.flush
-  let (io, a?, log) ← IO.FS.withIsolatedStreams (build.run.run'.run ctx).captureLog
-  let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error
-  let failed := log.any (·.level ≥ failLv)
-  if !failed && io.isEmpty && !log.hasVisibleEntries verbosity then
-    if showProgress then
-      if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
-  else
-    unless showProgress do
-      out.putStr header
-    out.putStr "\n"
-    if failed || log.hasVisibleEntries verbosity then
-      let v := if failed then .verbose else verbosity
-      log.replay (logger := MonadLog.stream out v)
-    unless io.isEmpty do
-      out.putStr "stdout/stderr:\n"
-      out.putStr io
-    out.flush
-  let failures := if failed then #[caption] else #[]
-  let jobs ← ctx.registeredJobs.get
-  let numJobs := jobs.size
-  let failures ← numJobs.foldM (init := failures) fun i s => Prod.snd <$> StateT.run (s := s) do
-    let (caption, job) := jobs[i]!
-    let header := s!"[{i+1}/{numJobs}] {caption}"
-    if showProgress then
-      out.putStr header; out.flush
-    let log := (← job.wait).state
-    let failed := log.any (·.level ≥ failLv)
-    if failed then modify (·.push caption)
-    if !(failed || log.hasVisibleEntries verbosity) then
+  if showAnsiProgress then
+    print! out s!"[?/?] {caption}"
+    flush out
+  let (a?, log) ← ((withLoggedIO build).run.run'.run ctx).run?
+  let failed := log.hasEntries ∧ log.maxLv ≥ failLv
+  if failed ∨ (log.hasEntries ∧ log.maxLv ≥ outLv) then
+    let icon := log.maxLv.icon
+    let caption := s!"{icon} [?/?] {caption}"
+    if useAnsi then
+      let caption := Ansi.chalk log.maxLv.ansiColor caption
       if showProgress then
-        if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
+        print! out s!"{Ansi.resetLine}{caption}"
+      else
+        print! out caption
     else
-      unless showProgress do
-        out.putStr header
-      out.putStr "\n"
-      let v := if failed then .verbose else verbosity
-      log.replay (logger := MonadLog.stream out v)
-      out.flush
+      print! out caption
+    print! out "\n"
+    let outLv := if failed then .trace else outLv
+    log.replay (logger := .stream out outLv useAnsi)
+    flush out
+  let failures := if failed then #[caption] else #[]
+  -- Job Monitor
+  let jobs ← ctx.registeredJobs.get
+  let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
+  let failures ← monitorJobs jobs out failLv outLv useAnsi showProgress
+    (resetCtrl := resetCtrl) (initFailures := failures)
+  -- Failure Report
   if failures.isEmpty then
     let some a := a?
-      | error "build failed"
+      | error "top-level build failed"
     return a
   else
-    out.putStr "Some build steps logged failures:\n"
-    failures.forM (out.putStr s!"- {·}\n")
+    print! out "Some builds logged failures:\n"
+    failures.forM (print! out s!"- {·}\n")
+    flush out
     error "build failed"
 
 /-- Run a build function in the Workspace's context and await the result. -/
diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean
index f3dcac127cca..dee47451fc5e 100644
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@@ -29,8 +29,9 @@ structure BuildSpec where
     | throw <| CliError.nonCliFacet facetType facet
   return {info, getBuildJob := h ▸ getJob}
 
-@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) :=
-  self.getBuildJob <$> self.info.fetch
+@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) := do
+  maybeRegisterJob (self.info.key.toSimpleString) <| ← do
+    self.getBuildJob <$> self.info.fetch
 
 def buildSpecs (specs : Array BuildSpec) : FetchM (BuildJob Unit) := do
   BuildJob.mixArray (← specs.mapM (·.fetch))
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 985d10ce2c32..cd949306a0b4 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -43,7 +43,10 @@ OPTIONS:
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update, -U          update manifest before building
   --reconfigure, -R     elaborate configuration files instead of using OLeans
-  --wfail               report a build failure if warnings are logged
+  --wfail               fail build if warnings are logged
+  --iofail              fail build if any I/O or other info is logged
+  --ansi, --no-ansi     toggle the use of ANSI escape codes to prettify output
+  --no-build            exit immediately if a build target is not up-to-date
 
 See `lake help <command>` for more information on a specific command."
 
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index b99683e5cb68..326cfa747455 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -40,7 +40,8 @@ structure LakeOptions where
   oldMode : Bool := false
   trustHash : Bool := true
   noBuild : Bool := false
-  failIfWarnings : Bool := false
+  failLv : LogLevel := .error
+  ansiMode : AnsiMode := .auto
 
 /-- Get the Lean installation. Error if missing. -/
 def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
@@ -75,13 +76,14 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
   }
 
 /-- Make a `BuildConfig` from a `LakeOptions`. -/
-def LakeOptions.mkBuildConfig (opts : LakeOptions) (useStdout := false) : BuildConfig where
+def LakeOptions.mkBuildConfig (opts : LakeOptions) (out := OutStream.stderr) : BuildConfig where
   oldMode := opts.oldMode
   trustHash := opts.trustHash
   noBuild := opts.noBuild
   verbosity := opts.verbosity
-  failIfWarnings := opts.failIfWarnings
-  useStdout := useStdout
+  failLv := opts.failLv
+  ansiMode := opts.ansiMode
+  out := out
 
 export LakeOptions (mkLoadConfig mkBuildConfig)
 
@@ -98,7 +100,7 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
   main.run
 
 instance : MonadLift LogIO CliStateM :=
-  ⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
+  ⟨fun x => do MainM.runLogIO x (← get).verbosity.minLogLv (← get).ansiMode⟩
 
 /-! ## Argument Parsing -/
 
@@ -160,7 +162,10 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
 | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
-| "--wfail"       => modifyThe LakeOptions ({· with failIfWarnings := true})
+| "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
+| "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
+| "--ansi"        => modifyThe LakeOptions ({· with ansiMode := .ansi})
+| "--no-ansi"     => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
 | "--dir"         => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
 | "--file"        => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
 | "--lean"        => do setLean <| ← takeOptArg "--lean" "path or command"
@@ -302,8 +307,11 @@ protected def build : CliM PUnit := do
   let ws ← loadWorkspace config opts.updateDeps
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
-  let buildConfig := mkBuildConfig opts (useStdout := true)
+  let buildConfig := mkBuildConfig opts (out := .stdout)
+  let showProgress := buildConfig.showProgress
   ws.runBuild (buildSpecs specs) buildConfig
+  if showProgress then
+    IO.println "Build completed successfully."
 
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
@@ -333,7 +341,7 @@ protected def setupFile : CliM PUnit := do
   let buildConfig := mkBuildConfig opts
   let filePath ← takeArg "file path"
   let imports ← takeArgs
-  setupFile loadConfig filePath imports buildConfig opts.verbosity
+  setupFile loadConfig filePath imports buildConfig
 
 protected def test : CliM PUnit := do
   processOptions lakeOption
diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
index 8c48430ef573..9403f3f24f41 100644
--- a/src/lake/Lake/CLI/Serve.lean
+++ b/src/lake/Lake/CLI/Serve.lean
@@ -29,17 +29,20 @@ The `setup-file` command is used internally by the Lean 4 server.
 -/
 def setupFile
   (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
-  (buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal)
+  (buildConfig : BuildConfig := {})
 : MainM PUnit := do
   if (← configFileExists loadConfig.configFile) then
     if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
       IO.eprint errLog
       IO.eprintln s!"Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file."
       exit 1
-    let ws ← MainM.runLogIO (loadWorkspace loadConfig) verbosity
+    let outLv := buildConfig.verbosity.minLogLv
+    let ws ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
+      loadWorkspace loadConfig
     let imports := imports.foldl (init := #[]) fun imps imp =>
       if let some mod := ws.findModule? imp.toName then imps.push mod else imps
-    let dynlibs ← MainM.runLogIO (ws.runBuild (buildImportsAndDeps path imports) buildConfig) verbosity
+    let dynlibs ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
+      ws.runBuild (buildImportsAndDeps path imports) buildConfig
     let paths : LeanPaths := {
       oleanPath := ws.leanPath
       srcPath := ws.leanSrcPath
@@ -67,7 +70,7 @@ with the given additional `args`.
 -/
 def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
   let (extraEnv, moreServerArgs) ← do
-    let (ws?, log) ← (loadWorkspace config).captureLog
+    let (ws?, log) ← (loadWorkspace config).run?
     log.replay (logger := MonadLog.stderr)
     if let some ws := ws? then
       let ctx := mkLakeContext ws
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index f1f68d418253..a129aa7f20fa 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -20,10 +20,13 @@ syntax buildDeclSig :=
 /-! ## Facet Declarations                                                      -/
 --------------------------------------------------------------------------------
 
-@[inline] def mkModuleFacetJob
-  (mod : Module) (facet : Name) (f : Module → FetchM (BuildJob α))
-: FetchM (BuildJob α) := do
-  withRegisterJob s!"Building {mod.name}:{facet}" (f mod)
+abbrev mkModuleFacetDecl
+  (α) (facet : Name)
+  [FamilyDef ModuleData facet (BuildJob α)]
+  (f : Module → FetchM (BuildJob α))
+: ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do
+  withRegisterJob (mod.facet facet |>.key.toSimpleString)
+    (f mod)
 
 /--
 Define a new module facet. Has one form:
@@ -42,21 +45,22 @@ kw:"module_facet " sig:buildDeclSig : command => do
   | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| module_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
-    let name := Name.quoteFrom id id.getId
-    let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
+    let facet := Name.quoteFrom id id.getId
+    let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
     let mod ← expandOptSimpleBinder mod?
     `(module_data $id : BuildJob $ty
-      $[$doc?:docComment]? @[$attrs,*] abbrev $facetId : ModuleFacetDecl := {
-        name := $name
-        config := Lake.mkFacetJobConfig fun mod =>
-          Lake.DSL.mkModuleFacetJob (α := $ty) mod $name (fun $mod => $defn)
-      } $[$wds?:whereDecls]?)
+      $[$doc?:docComment]? @[$attrs,*] abbrev $declId :=
+        Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn)
+      $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
 
-@[inline] def mkPackageFacetJob
-  (pkg : Package) (facet : Name) (f : Package → FetchM (BuildJob α))
-: FetchM (BuildJob α) := do
-  withRegisterJob s!"Building {pkg.name}:{facet}" (f pkg)
+abbrev mkPackageFacetDecl
+  (α) (facet : Name)
+  [FamilyDef PackageData facet (BuildJob α)]
+  (f : Package → FetchM (BuildJob α))
+: PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do
+  withRegisterJob (pkg.facet facet |>.key.toSimpleString)
+    (f pkg)
 
 /--
 Define a new package facet. Has one form:
@@ -75,21 +79,22 @@ kw:"package_facet " sig:buildDeclSig : command => do
   | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| package_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
-    let name := Name.quoteFrom id id.getId
-    let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
+    let facet := Name.quoteFrom id id.getId
+    let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
     let pkg ← expandOptSimpleBinder pkg?
     `(package_data $id : BuildJob $ty
-      $[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := {
-        name := $name
-        config := Lake.mkFacetJobConfig fun pkg =>
-          Lake.DSL.mkPackageFacetJob (α := $ty) pkg $name (fun $pkg => $defn)
-      } $[$wds?:whereDecls]?)
+      $[$doc?]? @[$attrs,*] abbrev $declId :=
+        Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn)
+      $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
-@[inline] def mkLibraryFacetJob
-  (lib : LeanLib) (facet : Name) (f : LeanLib → FetchM (BuildJob α))
-: FetchM (BuildJob α) := do
-  withRegisterJob s!"Building {lib.name}:{facet}" (f lib)
+abbrev mkLibraryFacetDecl
+  (α) (facet : Name)
+  [FamilyDef LibraryData facet (BuildJob α)]
+  (f : LeanLib → FetchM (BuildJob α))
+: LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do
+  withRegisterJob (lib.facet facet |>.key.toSimpleString)
+    (f lib)
 
 /--
 Define a new library facet. Has one form:
@@ -108,25 +113,26 @@ kw:"library_facet " sig:buildDeclSig : command => do
   | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) =>
     let attr ← withRef kw `(Term.attrInstance| library_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
-    let name := Name.quoteFrom id id.getId
-    let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
+    let facet := Name.quoteFrom id id.getId
+    let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
     let lib ← expandOptSimpleBinder lib?
     `(library_data $id : BuildJob $ty
-      $[$doc?]? @[$attrs,*] abbrev $facetId : LibraryFacetDecl := {
-        name := $name
-        config := Lake.mkFacetJobConfig fun lib =>
-          Lake.DSL.mkLibraryFacetJob (α := $ty) lib $name (fun $lib => $defn)
-      } $[$wds?:whereDecls]?)
+      $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl :=
+        Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn)
+      $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
 
 --------------------------------------------------------------------------------
 /-! ## Custom Target Declaration                                              -/
 --------------------------------------------------------------------------------
 
-@[inline] def mkTargetJob
-  (pkg : NPackage n) (target : Name) (f : NPackage n → FetchM (BuildJob α))
-: FetchM (BuildJob α) := do
-  withRegisterJob s!"Building {n}/{target}" (f pkg)
+abbrev mkTargetDecl
+  (α) (pkgName target : Name)
+  [FamilyDef CustomData (pkgName, target) (BuildJob α)]
+  (f : NPackage pkgName → FetchM (BuildJob α))
+: TargetDecl := .mk pkgName target <| mkTargetJobConfig fun pkg => do
+  withRegisterJob (pkg.target target |>.key.toSimpleString)
+    (f pkg)
 
 /--
 Define a new custom target for the package. Has one form:
@@ -151,12 +157,9 @@ kw:"target " sig:buildDeclSig : command => do
     let pkgName := mkIdentFrom id `_package.name
     let pkg ← expandOptSimpleBinder pkg?
     `(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
-      $[$doc?]? @[$attrs,*] abbrev $id : TargetDecl := {
-        pkg := $pkgName
-        name := $name
-        config := Lake.mkTargetJobConfig fun pkg =>
-          Lake.DSL.mkTargetJob (α := $ty) pkg $name (fun $pkg => $defn)
-      }  $[$wds?:whereDecls]?)
+      $[$doc?]? @[$attrs,*] abbrev $id :=
+        Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
+      $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
 
 
diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean
index 4741eb371305..36bc5eab9498 100644
--- a/src/lake/Lake/Util/EStateT.lean
+++ b/src/lake/Lake/Util/EStateT.lean
@@ -34,6 +34,16 @@ instance [Inhabited ε] [Inhabited σ] : Inhabited (EResult ε σ α) where
 @[inline] def EResult.setState (s : σ') (r : EResult ε σ α) : EResult ε σ' α :=
   r.modifyState fun _ => s
 
+/-- Convert a `EResult ε σ α` into `Except ε α × σ`. -/
+@[inline] def EResult.toProd : EResult ε σ α → Except ε α × σ
+| .ok a s => (.ok a, s)
+| .error e s => (.error e, s)
+
+/-- Convert an `EResult ε σ α` into `Option α × σ`, discarding the exception contents. -/
+@[inline] def EResult.toProd? : EResult ε σ α → Option α × σ
+| .ok a s => (some a, s)
+| .error _ s => (none, s)
+
 /-- Extract the result `α` from a `EResult ε σ α`. -/
 @[inline] def EResult.result? : EResult ε σ α → Option α
 | .ok a _ => some a
@@ -65,36 +75,61 @@ def EStateT (ε : Type u) (σ : Type v) (m : Type max u v w → Type x) (α : Ty
   σ → m (EResult ε σ α)
 
 namespace EStateT
+variable {ε ε' : Type u} {σ : Type v} {α β : Type w}
 
 instance [Inhabited ε] [Pure m] : Inhabited (EStateT ε σ m α) where
   default := fun s => pure (EResult.error default s)
 
-/-- Lift the `m` monad into the `EStateT ε σ m` monad transformer. -/
+/-- Execute an `EStateT` on initial state `init` to get an `EResult` result. -/
 @[always_inline, inline]
-protected def lift {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α := fun s => do
-  let a ← x; pure (.ok a s)
+def run (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α) :=
+  self init
 
-@[inline] def toStateT {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) : StateT σ m (Except ε α) := fun s => do
-  match (← x s) with
-  | .ok a s => return (.ok a, s)
-  | .error e s => return (.error e, s)
+/--
+Execute an `EStateT` on initial state `init`
+to get an `Except` result, discarding the final state.
+-/
+@[always_inline, inline]
+def run' {σ : Type max u w} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Except ε α) :=
+  EResult.toExcept <$> x init
 
-@[inline] def toStateT? {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) : StateT σ m (Option α) := do
-  (·.toOption) <$> x.toStateT
+/-- Convert an `EStateT` to a `StateT`, returning an `Except` result. -/
+@[inline] def toStateT {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Except ε α) :=
+  fun s => EResult.toProd <$> x s
 
-instance [Monad m] : MonadLift m (EStateT ε σ m) := ⟨EStateT.lift⟩
+/-- Convert an `EStateT` to a `StateT`, returning an `Option` result. -/
+@[inline] def toStateT? {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Option α) :=
+  fun s => EResult.toProd? <$> x s
 
-variable {ε ε' : Type u} {σ : Type v} {α β : Type w}
+/--
+Execute an `EStateT` on initial state `init`
+to get an `Option` result, discarding the exception contents.
+-/
+@[always_inline, inline]
+def run? {ε : Type max v w} [Functor m]  (init : σ) (x : EStateT ε σ m α) : m (Option α × σ) :=
+  EResult.toProd? <$> x init
 
-/-- Execute an `EStateT` on initial state `s` to get an `EResult` result. -/
+/--
+Execute an `EStateT` on initial state `init` to get an `Option` result,
+discarding the final state.
+-/
 @[always_inline, inline]
-def run (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α) :=
-  self init
+def run?' {ε σ α : Type u} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α) :=
+  EResult.result? <$> x init
 
-/-- Execute an `EStateT` on initial state `s` to get an `Except` result. -/
+@[inline] def catchExceptions {ε σ α : Type u}
+  [Monad m] (x : EStateT ε σ m α) (h : ε → StateT σ m α)
+: StateT σ m α := fun s => do
+  match (← x s) with
+  | .ok a s => return (a, s)
+  | .error e s => h e s
+
+/-- Lift the `m` monad into the `EStateT ε σ m` monad transformer. -/
 @[always_inline, inline]
-def run' {σ : Type max u w} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Except ε α) :=
-  EResult.toExcept <$> x init
+protected def lift {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α := fun s => do
+  let a ← x; pure (.ok a s)
+
+instance {ε σ : Type u} [Monad m] : MonadLift m (EStateT ε σ m) := ⟨EStateT.lift⟩
 
 /-- The `pure` operation of the `EStateT` monad transformer. -/
 @[always_inline, inline]
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index 4f183ec645fb..9d705a4ee52b 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -25,6 +25,46 @@ instance : Max Verbosity := maxOfLe
 
 instance : Inhabited Verbosity := ⟨.normal⟩
 
+/-- Whether to ANSI escape codes. -/
+inductive AnsiMode
+/--
+Automatically determine whether to use ANSI escape codes
+based on whether the stream written to is a terminal.
+-/
+| auto
+/-- Use ANSI escape codes. -/
+| ansi
+/-- Do not use ANSI escape codes. -/
+| noAnsi
+
+/-- Returns whether to ANSI escape codes with the stream `out`. -/
+def AnsiMode.isEnabled (out : IO.FS.Stream) : AnsiMode → BaseIO Bool
+| .auto => out.isTty
+| .ansi => pure true
+| .noAnsi => pure false
+
+/--
+Wrap text in ANSI escape sequences to make it bold and color it the ANSI `colorCode`.
+Resets all terminal font attributes at the end of the text.
+-/
+def Ansi.chalk (colorCode text : String) : String :=
+  s!"\x1B[1;{colorCode}m{text}\x1B[m"
+
+/-- A pure representation of output stream. -/
+inductive OutStream
+| stdout
+| stderr
+| stream (s : IO.FS.Stream)
+
+/-- Returns the real output stream associated with `OutStream`. -/
+def OutStream.get : OutStream → BaseIO IO.FS.Stream
+| .stdout => IO.getStdout
+| .stderr => IO.getStderr
+| .stream s => pure s
+
+instance : Coe IO.FS.Stream OutStream := ⟨.stream⟩
+instance : Coe IO.FS.Handle OutStream := ⟨fun h => .stream (.ofHandle h)⟩
+
 inductive LogLevel
 | trace
 | info
@@ -37,6 +77,18 @@ instance : LE LogLevel := leOfOrd
 instance : Min LogLevel := minOfLe
 instance : Max LogLevel := maxOfLe
 
+/-- Unicode icon for representing the log level. -/
+def LogLevel.icon : LogLevel → Char
+| .trace | .info => 'ℹ'
+| .warning => '⚠'
+| .error => '✖'
+
+/-- ANSI escape code for coloring text of at the log level. -/
+def LogLevel.ansiColor : LogLevel → String
+| .trace | .info => "34"
+| .warning => "33"
+| .error => "31"
+
 protected def LogLevel.toString : LogLevel → String
 | .trace => "trace"
 | .info => "info"
@@ -50,19 +102,23 @@ protected def LogLevel.ofMessageSeverity : MessageSeverity → LogLevel
 
 instance : ToString LogLevel := ⟨LogLevel.toString⟩
 
-def LogLevel.visibleAtVerbosity (self : LogLevel) (verbosity : Verbosity) : Bool :=
-  match self with
-  | .trace => verbosity == .verbose
-  | .info => verbosity != .quiet
-  | _ => true
+def Verbosity.minLogLv : Verbosity → LogLevel
+| .quiet => .warning
+| .normal =>  .info
+| .verbose => .trace
 
 structure LogEntry where
   level : LogLevel
   message : String
   deriving Inhabited, ToJson, FromJson
 
-protected def LogEntry.toString (self : LogEntry) : String :=
-  s!"{self.level}: {self.message.trim}"
+protected def LogEntry.toString (self : LogEntry) (useAnsi := false) : String :=
+  if useAnsi then
+    let {level := lv, message := msg} := self
+    let pre := Ansi.chalk lv.ansiColor s!"{lv.toString}:"
+    s!"{pre} {msg.trim}"
+  else
+    s!"{self.level}: {self.message.trim}"
 
 instance : ToString LogEntry := ⟨LogEntry.toString⟩
 
@@ -83,75 +139,99 @@ export MonadLog (logEntry)
 @[inline] def logError  [MonadLog m] (message : String) : m PUnit :=
   logEntry {level := .error, message}
 
-def logToIO (e : LogEntry) (verbosity : Verbosity) : BaseIO PUnit := do
-  match e.level with
-  | .trace => if verbosity == .verbose then
-    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
-  | .info => if verbosity != .quiet then
-    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
-  | .warning => IO.eprintln s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-  | .error => IO.eprintln s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-
-def logToStream (e : LogEntry) (h : IO.FS.Stream) (verbosity : Verbosity) : BaseIO PUnit := do
-  match e.level with
-  | .trace => if verbosity == .verbose then
-    h.putStrLn s!"trace: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-  | .info => if verbosity != .quiet then
-    h.putStrLn s!"info: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-  | .warning => h.putStrLn s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-  | .error => h.putStrLn s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
-
 @[specialize] def logSerialMessage (msg : SerialMessage) [MonadLog m] : m PUnit :=
-  let str := msg.data
   let str := if msg.caption.trim.isEmpty then
-    str.trim else s!"{msg.caption.trim}:\n{str.trim}"
+     msg.data.trim else s!"{msg.caption.trim}:\n{msg.data.trim}"
   logEntry {
     level := .ofMessageSeverity msg.severity
-    message := mkErrorStringWithPos msg.fileName msg.pos str msg.endPos
+    message := mkErrorStringWithPos msg.fileName msg.pos str none
   }
 
-namespace MonadLog
+@[deprecated] def logToIO (e : LogEntry) (minLv : LogLevel)  : BaseIO PUnit := do
+  match e.level with
+  | .trace => if minLv ≥ .trace then
+    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
+  | .info => if minLv ≥ .info then
+    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
+  | .warning => IO.eprintln e.toString |>.catchExceptions fun _ => pure ()
+  | .error => IO.eprintln e.toString |>.catchExceptions fun _ => pure ()
 
-@[specialize] def nop [Pure m] : MonadLog m :=
-  ⟨fun _ => pure ()⟩
+def logToStream
+  (e : LogEntry) (out : IO.FS.Stream) (minLv : LogLevel) (useAnsi : Bool)
+: BaseIO PUnit := do
+  if e.level ≥ minLv then
+    out.putStrLn (e.toString useAnsi) |>.catchExceptions fun _ => pure ()
 
-instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
+namespace MonadLog
 
-@[specialize] def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
-  logEntry e := logToIO e verbosity
+abbrev nop [Pure m] : MonadLog m where
+  logEntry _  := pure ()
 
-@[inline] def stream [MonadLiftT BaseIO m] (h : IO.FS.Stream) (verbosity := Verbosity.normal) : MonadLog m where
-  logEntry e := logToStream e h verbosity
+instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
 
-@[inline] def stdout [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
-  logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStdout) verbosity
+abbrev lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
+  logEntry e := liftM <| self.logEntry e
 
-@[inline] def stderr [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
-  logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStderr) verbosity
+instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := methods.lift
 
-@[inline] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
-  logEntry e := liftM <| self.logEntry e
+set_option linter.deprecated false in
+@[deprecated] abbrev io [MonadLiftT BaseIO m] (minLv := LogLevel.info) : MonadLog m where
+  logEntry e := logToIO e minLv
 
-instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
+abbrev stream [MonadLiftT BaseIO m]
+  (out : IO.FS.Stream) (minLv := LogLevel.info) (useAnsi := false)
+: MonadLog m where logEntry e := logToStream e out minLv useAnsi
 
 end MonadLog
 
+def OutStream.logEntry
+  (self : OutStream) (e : LogEntry)
+  (minLv : LogLevel := .info) (ansiMode := AnsiMode.auto)
+: BaseIO PUnit := do
+  let out ← self.get
+  let useAnsi ← ansiMode.isEnabled out
+  logToStream e out minLv useAnsi
+
+abbrev OutStream.logger [MonadLiftT BaseIO m]
+  (out : OutStream) (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
+: MonadLog m where logEntry e := out.logEntry e minLv ansiMode
+
+abbrev MonadLog.stdout
+  [MonadLiftT BaseIO m] (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
+: MonadLog m := OutStream.stdout.logger minLv ansiMode
+
+abbrev MonadLog.stderr
+  [MonadLiftT BaseIO m] (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
+: MonadLog m := OutStream.stderr.logger minLv ansiMode
+
+@[inline] def OutStream.getLogger [MonadLiftT BaseIO m]
+  (out : OutStream) (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
+: BaseIO (MonadLog m) := do
+  let out ← out.get
+  let useAnsi ← ansiMode.isEnabled out
+  return .stream out minLv useAnsi
+
+/-- A monad equipped with a `MonadLog` instance -/
 abbrev MonadLogT (m : Type u → Type v) (n : Type v → Type w) :=
   ReaderT (MonadLog m) n
 
+namespace MonadLogT
+
 instance [Pure n] [Inhabited α] : Inhabited (MonadLogT m n α) :=
   ⟨fun _ => pure Inhabited.default⟩
 
 instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
   logEntry e := do (← read).logEntry e
 
-@[inline] def MonadLogT.adaptMethods [Monad n]
+@[inline] def adaptMethods [Monad n]
 (f : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α :=
   ReaderT.adapt f self
 
-@[inline] def  MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
+@[inline] def ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
   self MonadLog.nop
 
+end MonadLogT
+
 /- A Lake log. An `Array` of log entries. -/
 structure Log where
   entries : Array LogEntry
@@ -172,12 +252,15 @@ namespace Log
 
 instance : EmptyCollection Log := ⟨Log.empty⟩
 
-@[inline] def isEmpty (log : Log) : Bool :=
-  log.entries.isEmpty
-
 @[inline] def size (log : Log) : Nat :=
   log.entries.size
 
+@[inline] def isEmpty (log : Log) : Bool :=
+  log.size = 0
+
+@[inline] def hasEntries (log : Log) : Bool :=
+  log.size ≠ 0
+
 @[inline] def endPos (log : Log) : Log.Pos :=
   ⟨log.entries.size⟩
 
@@ -220,17 +303,22 @@ instance : ToString Log := ⟨Log.toString⟩
 @[inline] def filter (f : LogEntry → Bool) (log : Log) : Log :=
   .mk <| log.entries.filter f
 
-def filterByVerbosity (log : Log) (verbosity := Verbosity.normal) : Log :=
-  log.filter (·.level.visibleAtVerbosity verbosity)
-
 @[inline] def any (f : LogEntry → Bool) (log : Log) : Bool :=
   log.entries.any f
 
-def hasVisibleEntries (log : Log) (verbosity := Verbosity.normal) : Bool :=
-  log.any (·.level.visibleAtVerbosity verbosity)
+/-- The max log level of entries in this log. If empty, returns `trace`. -/
+def maxLv (log : Log) : LogLevel :=
+  log.entries.foldl (max · ·.level) .trace
 
 end Log
 
+/-- Add a `LogEntry` to the end of the monad's `Log`. -/
+@[inline] def pushLogEntry
+  [MonadStateOf Log m] (e : LogEntry)
+: m PUnit := modify (·.push e)
+
+abbrev MonadLog.ofMonadState [MonadStateOf Log m] : MonadLog m := ⟨pushLogEntry⟩
+
 /-- Returns the monad's log. -/
 @[inline] def getLog [MonadStateOf Log m] : m Log :=
   get
@@ -239,22 +327,26 @@ end Log
 @[inline] def getLogPos [Functor m] [MonadStateOf Log m] : m Log.Pos :=
   (·.endPos) <$> getLog
 
-/--
-Backtracks the monad's log to `pos`.
-Useful for discarding logged errors after catching an error position
-from an `ELogT` (e.g., `LogIO`).
--/
-@[inline] def dropLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m PUnit :=
-  modify (·.dropFrom pos)
+/-- Removes the section monad's log starting and returns it. -/
+@[inline] def takeLog [MonadStateOf Log m] : m Log :=
+  modifyGet fun log => (log, {})
 
 /--
-Removes the section monad's log starting at `pos` and returns it.
+Removes the monad's log starting at `pos` and returns it.
 Useful for extracting logged errors after catching an error position
 from an `ELogT` (e.g., `LogIO`).
 -/
 @[inline] def takeLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m Log :=
   modifyGet fun log => (log.takeFrom pos, log.dropFrom pos)
 
+/--
+Backtracks the monad's log to `pos`.
+Useful for discarding logged errors after catching an error position
+from an `ELogT` (e.g., `LogIO`).
+-/
+@[inline] def dropLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m PUnit :=
+  modify (·.dropFrom pos)
+
 /-- Returns the log from `x` while leaving it intact in the monad. -/
 @[inline] def extractLog [Monad m] [MonadStateOf Log m] (x : m PUnit) : m Log := do
   let iniPos ← getLogPos
@@ -284,17 +376,75 @@ from an `ELogT` (e.g., `LogIO`).
   try self catch _ => pure ()
   throw iniPos
 
+/-- Captures IO in `x` into an informational log entry. -/
+@[inline] def withLoggedIO
+  [Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
+: m α := do
+  let (out, a) ← IO.FS.withIsolatedStreams x
+  unless out.isEmpty do logInfo s!"stdout/stderr:\n{out}"
+  return a
+
+/-- Throw with the logged error `message`. -/
+@[inline] protected def ELog.error
+  [Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
+  (msg : String)
+: m α := errorWithLog (logError msg)
+
+/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/
+abbrev ELog.monadError
+  [Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
+: MonadError m := ⟨ELog.error⟩
+
+/-- Fail without logging anything. -/
+@[inline] protected def ELog.failure
+  [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
+: m α := do throw (← getLogPos)
+
+/-- Performs `x`. If it fails, drop its log and perform `y`. -/
+@[inline] protected def ELog.orElse
+  [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
+  (x : m α) (y : Unit → m α)
+: m α := try x catch errPos => dropLogFrom errPos; y ()
+
+/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/
+abbrev ELog.alternative
+  [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
+: Alternative m where
+  failure := ELog.failure
+  orElse  := ELog.orElse
+
 /-- A monad equipped with a log. -/
 abbrev LogT (m : Type → Type) :=
   StateT Log m
 
+instance [Monad m] : MonadLog (LogT m) := .ofMonadState
+
 namespace LogT
 
-@[inline] protected def log [Monad m] (e : LogEntry) : LogT m PUnit :=
-  modify (·.push e)
+abbrev run [Functor m] (self : LogT m α) (log : Log := {})  : m (α × Log) :=
+  StateT.run self log
+
+abbrev run' [Functor m] (self : LogT m α) (log : Log := {}) :  m α :=
+  StateT.run' self log
 
-instance [Monad m] : MonadLog (LogT m) := ⟨LogT.log⟩
+/--
+Run `self` with the log taken from the state of the monad `n`.
+
+**Warning:** If lifting `self` from `m` to `n` fails, the log will be lost.
+Thus, this is best used when the lift cannot fail.
+-/
+@[inline] def takeAndRun
+  [Monad n] [MonadStateOf Log n] [MonadLiftT m n] [MonadFinally n]
+  (self : LogT m α)
+: n α := do
+  let (a, log) ← self (← takeLog)
+  set log
+  return a
 
+/--
+Runs `self` in `n` and then replays the entries of the resulting log
+using the new monad's `logger`.
+-/
 @[inline] def replayLog [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : LogT m α) : n α := do
   let (a, log) ← self {}
   log.replay (logger := logger)
@@ -308,29 +458,49 @@ abbrev ELogT (m : Type → Type) :=
 
 abbrev ELogResult (α) := EResult Log.Pos Log α
 
+instance [Monad m] : MonadLog (ELogT m) := .ofMonadState
+instance [Monad m] : MonadError (ELogT m) := ELog.monadError
+instance [Monad m] : Alternative (ELogT m) := ELog.alternative
+
 namespace ELogT
 
-@[inline] protected def log [Monad m] (e : LogEntry) : ELogT m PUnit :=
-  modify (·.push e)
+abbrev run (self : ELogT m α) (log : Log := {})  : m (ELogResult α) :=
+  EStateT.run log self
 
-instance [Monad m] : MonadLog (ELogT m) := ⟨ELogT.log⟩
+abbrev run' [Functor m] (self : ELogT m α) (log : Log := {}) :  m (Except Log.Pos α) :=
+  EStateT.run' log self
 
-@[inline] protected def error [Monad m] (msg : String) : ELogT m α :=
-  errorWithLog (logError msg)
+abbrev toLogT [Functor m] (self : ELogT m α) : LogT m (Except Log.Pos α) :=
+  self.toStateT
 
-instance [Monad m] : MonadError (ELogT m) := ⟨ELogT.error⟩
+abbrev toLogT? [Functor m] (self : ELogT m α) : LogT m (Option α) :=
+  self.toStateT?
 
-/-- Fail without logging anything. -/
-@[inline] protected def ELogT.failure [Monad m] : ELogT m α := do
-  throw (← getLogPos)
+abbrev run? [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α × Log) :=
+  EStateT.run? log self
 
-/-- Performs `x`. If it fails, drop its log and perform `y`. -/
-@[inline] protected def ELogT.orElse [Monad m] (x : ELogT m α) (y : Unit → ELogT m α)  : ELogT m α :=
-  try x catch errPos => dropLogFrom errPos; y ()
+abbrev run?' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α) :=
+  EStateT.run?' log self
+
+@[inline] def catchLog [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := do
+  self.catchExceptions fun errPos => do f (← takeLogFrom errPos)
+
+@[deprecated run?] abbrev captureLog := @run?
 
-instance [Monad m] : Alternative (ELogT m) where
-  failure := ELogT.failure
-  orElse  := ELogT.orElse
+/--
+Run `self` with the log taken from the state of the monad `n`,
+
+**Warning:** If lifting `self` from `m` to `n` fails, the log will be lost.
+Thus, this is best used when the lift cannot fail. Note  excludes the
+native log position failure of `ELogT`, which are lifted safely.
+-/
+@[inline] def takeAndRun
+  [Monad n] [MonadStateOf Log n] [MonadExceptOf Log.Pos n] [MonadLiftT m n]
+  (self : ELogT m α)
+: n α := do
+  match (← self (← takeLog)) with
+  | .ok a log => set log; return a
+  | .error e log => set log; throw e
 
 /--
 Runs `self` in `n` and then replays the entries of the resulting log
@@ -352,36 +522,24 @@ a `failure` in the new monad.
   | .ok a log => log.replay (logger := logger) *> pure a
   | .error _ log => log.replay (logger := logger) *> failure
 
-@[inline] def catchFailure [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := fun log => do
-  match (← self log) with
-  | .error n log => let (h,t) := log.split n; f h t
-  | .ok a log => return (a, log)
-
-@[inline] def captureLog [Monad m] (self : ELogT m α) : m (Option α × Log) := do
- match (← self {}) with
- | .ok a log => return (some a, log)
- | .error _ log => return (none, log)
-
 end ELogT
 
+/-- A monad equipped with a log, a log error position, and the ability to perform I/O. -/
 abbrev LogIO := ELogT BaseIO
 
 instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
 
+namespace LogIO
+
+@[deprecated ELogT.run?] abbrev captureLog := @ELogT.run?
+
 /--
 Runs a `LogIO` action in `BaseIO`.
-Prints logs message at `verbosity` to stderr or stdout (if `useStdout`).
+Prints log entries of at least `minLv` to `out`.
 -/
-@[inline] def LogIO.toBaseIO
-  (x : LogIO α) (verbosity := Verbosity.normal) (useStdout := false)
-: BaseIO (Option α) :=
-  let logger := if useStdout then .stdout verbosity else .stderr verbosity
-  x.replayLog? (logger := logger)
+@[inline] def toBaseIO (self : LogIO α)
+  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
+: BaseIO (Option α) := do
+  self.replayLog? (logger := ← out.getLogger minLv ansiMode)
 
-/-- Captures IO in `x` into an informational log entry. -/
-@[inline] def withLoggedIO
-  [Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
-: m α := do
-  let (out, a) ← IO.FS.withIsolatedStreams x
-  unless out.isEmpty do logInfo s!"stdout/stderr:\n{out}"
-  return a
+end LogIO
diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean
index d9c65e733bf3..47f7c143d9b2 100644
--- a/src/lake/Lake/Util/MainM.lean
+++ b/src/lake/Lake/Util/MainM.lean
@@ -66,7 +66,7 @@ instance : Alternative MainM where
 
 /-! # Logging and IO -/
 
-instance : MonadLog MainM := MonadLog.stderr
+instance : MonadLog MainM := .stderr
 
 /-- Print out a error line with the given message and then exit with an error code. -/
 @[inline] protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
@@ -76,7 +76,9 @@ instance : MonadLog MainM := MonadLog.stderr
 instance : MonadError MainM := ⟨MainM.error⟩
 instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
 
-@[inline] def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
-  x.replayLog (logger := MonadLog.stderr verbosity)
+@[inline] def runLogIO (x : LogIO α)
+  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
+: MainM α := do
+  x.replayLog (logger := ← out.getLogger minLv ansiMode)
 
 instance : MonadLift LogIO MainM := ⟨runLogIO⟩
diff --git a/src/lake/examples/targets/test.sh b/src/lake/examples/targets/test.sh
index 55fc1f3de412..6fb188d8bee7 100755
--- a/src/lake/examples/targets/test.sh
+++ b/src/lake/examples/targets/test.sh
@@ -23,25 +23,25 @@ fi
 $LAKE build targets:noexistent && exit 1 || true
 
 # Test custom targets and package, library, and module facets
-$LAKE build bark | awk '/Building/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building targets/bark
+$LAKE build bark | awk '/Ran/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets/bark
 info: Bark!
 EOF
 ) -
-$LAKE build targets/bark_bark | awk '/Building/,/bark_bark/' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/2] Building targets/bark
+$LAKE build targets/bark_bark | awk '/Ran/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/2] Ran targets/bark
 info: Bark!
-[2/2] Building targets/bark_bark
+Build completed successfully.
 EOF
 ) -
-$LAKE build targets:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building targets:print_name
+$LAKE build targets:print_name | awk '/Ran/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets:print_name
 info: stdout/stderr:
 targets
 EOF
 ) -
-$LAKE build Foo:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
-[1/1] Building Foo:print_name
+$LAKE build Foo:print_name | awk '/Ran/,/^Foo/' | diff -u --strip-trailing-cr <(cat << 'EOF'
+ℹ [1/1] Ran targets/Foo:print_name
 info: stdout/stderr:
 Foo
 EOF
diff --git a/src/lake/tests/noRelease/clean.sh b/src/lake/tests/noRelease/clean.sh
new file mode 100755
index 000000000000..b6e54c681e54
--- /dev/null
+++ b/src/lake/tests/noRelease/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json
diff --git a/src/lake/tests/noRelease/dep/lakefile.lean b/src/lake/tests/noRelease/dep/lakefile.lean
new file mode 100644
index 000000000000..ce123925d29c
--- /dev/null
+++ b/src/lake/tests/noRelease/dep/lakefile.lean
@@ -0,0 +1,6 @@
+import Lake
+open Lake DSL
+
+package dep where
+  preferReleaseBuild := true
+  releaseRepo := "https://example.com"
diff --git a/src/lake/tests/noRelease/lakefile.lean b/src/lake/tests/noRelease/lakefile.lean
new file mode 100644
index 000000000000..8a0940dfdc52
--- /dev/null
+++ b/src/lake/tests/noRelease/lakefile.lean
@@ -0,0 +1,5 @@
+import Lake
+open Lake DSL
+
+package test
+require dep from "dep"
diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh
new file mode 100755
index 000000000000..1c54a6e508d3
--- /dev/null
+++ b/src/lake/tests/noRelease/test.sh
@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# ---
+# Test Lake's behavior when failing to fetch a cloud release
+# ---
+
+# Test that a direct invocation fo `lake build *:release` fails
+($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF'
+✖ [1/1] Fetching dep:release
+info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+error: failed to fetch cloud release
+Some builds logged failures:
+- dep:release
+EOF
+) -
+
+# Test that an indirect fetch on the release does not cause the build to fail
+$LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF'
+⚠ [1/1] Fetched test:extraDep
+info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+warning: failed to fetch cloud release; falling back to local build
+Build completed successfully.
+EOF
+) -
diff --git a/src/lake/tests/old/expected.out b/src/lake/tests/old/expected.out
deleted file mode 100644
index 09142516527f..000000000000
--- a/src/lake/tests/old/expected.out
+++ /dev/null
@@ -1,6 +0,0 @@
-Building Hello
-Compiling Hello
-Linking hello
-Building Hello
-Compiling Hello
-Linking hello
diff --git a/src/lake/tests/old/test.sh b/src/lake/tests/old/test.sh
index e69573700de0..b1aa6d8a8e88 100755
--- a/src/lake/tests/old/test.sh
+++ b/src/lake/tests/old/test.sh
@@ -5,23 +5,42 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
 
-# Tests the `--old` option for using outdate oleans
-# See https://github.com/leanprover/lake/issues/44
+# Test the `--old` option for using outdate oleans
+# https://github.com/leanprover/lake/issues/44
+# https://github.com/leanprover/lean4/issues/2822
+
+diff_out() {
+  grep 'Built' || true |
+  sed 's/^.*\[.*\] //' |
+  sed 's/\s*(.*)$//' |
+  LANG=POSIX sort |
+  diff -u --strip-trailing-cr "$1" -
+}
 
 $LAKE new hello
 $LAKE -d hello build
-sleep 0.5 # for some reason, delay needed for `--old` rebuild consistency
-echo 'def hello := "old"' > hello/Hello.lean
-$LAKE -d hello build --old | sed 's/\[.*\] //' | tee produced.out
-echo 'def hello := "normal"' > hello/Hello.lean
-$LAKE -d hello build | sed 's/\[.*\] //' | tee -a produced.out
-
-grep -i main produced.out
-grep -i hello produced.out > produced.out.tmp
-mv produced.out.tmp produced.out
-if [ "$OS" = Windows_NT ]; then
-  sed -i 's/.exe//g' produced.out
-  diff --strip-trailing-cr expected.out produced.out
-else
-  diff expected.out produced.out
-fi
+sleep 1 # sleep needed to guarantee modification time difference
+
+# Test basic `--old`
+echo 'def hello := "old"' > hello/Hello/Basic.lean
+$LAKE -d hello build --old | diff_out <(cat << 'EOF'
+Built Hello.Basic
+Built Hello.Basic:c
+Built hello
+EOF
+)
+
+# Test a normal build works after an `--old` build
+echo 'def hello := "normal"' > hello/Hello/Basic.lean
+$LAKE -d hello build | diff_out <(cat << 'EOF'
+Built Hello
+Built Hello.Basic
+Built Hello.Basic:c
+Built Main
+Built hello
+EOF
+)
+
+# Test that `--old` does not rebuild touched but unchanged files (lean4#2822)
+touch hello/Hello/Basic.lean
+$LAKE -d hello build --old | diff_out /dev/null
diff --git a/tests/pkg/test_extern/expected.txt b/tests/pkg/test_extern/expected.txt
index ca679c95755b..2ac13533aa5f 100644
--- a/tests/pkg/test_extern/expected.txt
+++ b/tests/pkg/test_extern/expected.txt
@@ -1,4 +1,4 @@
-error: ././././TestExtern.lean:5:0-5:27: native implementation did not agree with reference implementation!
+error: ././././TestExtern.lean:5:0: native implementation did not agree with reference implementation!
 Compare the outputs of:
 #eval Nat.not_add 4 5
  and