feat: lake: build monitor improvements (#4127)

The new Lake build monitor is now more selective, accurate, and prettier
in what it prints.

**Key Changes:**

* Poll jobs at a fixed frequency (100ms), updating the caption and
finished job count.
* Add `action` field to jobs to record information about what jobs do.
It enables distinguishing between jobs which build something, fetch from
a store, or reload logs from the cache.
* At standard verbosity, print build captions only when a job is know to
build or fetch something (i.e., `action >= .fetch`).
* Add an icon and color to job captions based on their log-level / build
status. Also add color to levels in logs.
* Add `--ansi`/`--no-ansi` to toggle Lake's use of ANSI escape codes.
* Fix some `v4.8.0-rc1` bugs and `--old`.

Closes #2822.

(cherry picked from commit 7648bf2)

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

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

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

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

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,27 +59,54 @@ 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 α :=
   fun build => cast (by simp) <| build self
 
 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

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 _ => #[])

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)
 
 /-!

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