feat: lake: ANSI monitor: only display progress + running job info (#4232)

The ANSI mode build monitor now now longer displays built jobs (instead
only those that print info or failed). Also upgrades the progress ticker
with a spinner icon and information on the number of running jobs.

src/lake/Lake/Build/Actions.lean

@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 import Lake.Util.Proc
 import Lake.Util.NativeLib
-import Lake.Build.Basic
+import Lake.Build.Job
 
 /-! # Common Build Actions
 Low level actions to build common Lean artifacts via the Lean toolchain.

src/lake/Lake/Build/Basic.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Util.Log
 import Lake.Util.Exit
-import Lake.Util.Task
 import Lake.Util.Lift
 import Lake.Config.Context
 import Lake.Build.Trace
@@ -52,96 +51,17 @@ Whether the build should show progress information.
 def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
   (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
 
-/-- Information on what this job did. -/
-inductive JobAction
-/-- No information about this job's action is available. -/
-| unknown
-/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
-| replay
-/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
-| fetch
-/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
-| build
-deriving Inhabited, Repr, DecidableEq, Ord
-
-instance : LT JobAction := ltOfOrd
-instance : LE JobAction := leOfOrd
-instance : Min JobAction := minOfLe
-instance : Max JobAction := maxOfLe
-
-@[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 α
-
-/-- The `Task` of a Lake job. -/
-abbrev JobTask α := BaseIOTask (JobResult α)
-
-/-- A Lake job. -/
-structure Job (α : Type u)  where
-  task : JobTask α
-  caption : String
+/-- A Lake job with an opaque value type in `Type`. -/
+declare_opaque_type OpaqueJob
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  registeredJobs : IO.Ref (Array (Job Unit))
+  registeredJobs : IO.Ref (Array OpaqueJob)
 
 /-- 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
-
-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
@@ -175,19 +95,3 @@ abbrev MonadBuild (m : Type → Type u) :=
 
 /-- The internal core monad of Lake builds.  Not intended for user use. -/
 abbrev CoreBuildM := BuildT LogIO
-
-/-- 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/Fetch.lean

@@ -81,32 +81,35 @@ def ensureJob (x : FetchM (Job α))
     let (log, jobLog) := log.split iniPos
     return (.ok (.error jobLog) log, store)
 
+/--
+Registers the job for the top-level build monitor,
+(e.g., the Lake CLI progress UI), assigning it `caption`.
+-/
+def registerJob (caption : String) (job : Job α) : FetchM (Job α) := do
+  let job := job.setCaption caption
+  (← getBuildContext).registeredJobs.modify (·.push job)
+  return job.renew
+
 /--
 Registers the produced job for the top-level build monitor
 (e.g., the Lake CLI progress UI), assigning it `caption`.
 
 Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
 -/
-@[inline] def withRegisterJob
+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
+  registerJob caption job
 
 /--
 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 α)
+  (caption : 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
+    registerJob caption job
   else
     return job

src/lake/Lake/Build/Job.lean

@@ -3,13 +3,136 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Trace
+import Lake.Util.Task
 import Lake.Build.Basic
 
 open System
 
 namespace Lake
 
+/-- 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
+  deriving Inhabited
+
+/--
+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 α
+
+/-- The `Task` of a Lake job. -/
+abbrev JobTask α := BaseIOTask (JobResult α)
+
+/-- 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
+
+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}
+
+/-- 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
+
+/-- A Lake job. -/
+structure Job (α : Type u)  where
+  task : JobTask α
+  caption : String
+  deriving Inhabited
+
+structure BundledJob where
+  {type : Type u}
+  job : Job type
+  deriving Inhabited
+
+instance : CoeOut (Job α) BundledJob := ⟨.mk⟩
+
+hydrate_opaque_type OpaqueJob BundledJob
+
+abbrev OpaqueJob.type (job : OpaqueJob) : Type :=
+  job.get.type
+
+abbrev OpaqueJob.toJob (job : OpaqueJob) : Job job.type :=
+  job.get.job
+
+abbrev OpaqueJob.task (job : OpaqueJob) : JobTask job.type :=
+  job.toJob.task
+
+abbrev OpaqueJob.caption (job : OpaqueJob) : String :=
+  job.toJob.caption
+
+instance : CoeDep OpaqueJob job (Job job.type) := ⟨job.toJob⟩
+
 namespace Job
 
 @[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=

src/lake/Lake/Build/Run.lean

@@ -25,6 +25,10 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext
     leanTrace := Hash.ofString ws.lakeEnv.leanGithash
   }
 
+/-- Unicode icons that make up the spinner in animation order. -/
+def Monitor.spinnerFrames :=
+  #['⣾','⣷','⣯','⣟','⡿','⢿','⣻','⣽']
+
 /-- Context of the Lake build monitor. -/
 structure MonitorContext where
   totalJobs : Nat
@@ -35,15 +39,15 @@ structure MonitorContext where
   useAnsi : Bool
   showProgress : Bool
   /-- How often to poll jobs (in milliseconds). -/
-  updateFrequency : Nat := 100
+  updateFrequency : Nat
 
 /-- State of the Lake build monitor. -/
 structure MonitorState where
   jobNo : Nat := 1
-  jobs : Array (Job Unit)
   failures : Array String
   resetCtrl : String
   lastUpdate : Nat
+  spinnerIdx : Fin Monitor.spinnerFrames.size := ⟨0, by decide⟩
 
 /-- Monad of the Lake build monitor. -/
 abbrev MonitorM := ReaderT MonitorContext <| StateT MonitorState BaseIO
@@ -77,29 +81,35 @@ namespace Monitor
 @[inline] nonrec def flush : MonitorM PUnit := do
   flush (← read).out
 
-def renderProgress : MonitorM PUnit := do
-  let {jobNo, jobs, ..} ← get
+def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.size) : MonitorM PUnit := do
+  let {jobNo, ..} ← 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}] Running {caption}"
-      flush
+    let spinnerIcon ← modifyGet fun s =>
+        (spinnerFrames[s.spinnerIdx], {s with spinnerIdx := s.spinnerIdx + ⟨1, by decide⟩})
+    let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := Ansi.resetLine})
+    let caption :=
+      if _ : 0 < running.size then
+        s!"Running {running[0].caption} (+ {running.size - 1} more)"
+      else
+        s!"Running {unfinished[0].caption}"
+    print s!"{resetCtrl}{spinnerIcon} [{jobNo}/{totalJobs}] {caption}"
+    flush
 
-def reportJob (job : Job Unit) : MonitorM PUnit := do
+def reportJob (job : OpaqueJob) : MonitorM PUnit := do
   let {jobNo, ..} ← get
   let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
-  let {log, action, ..} := job.task.get.state
+  let {task, caption} := job.toJob
+  let {log, action, ..} := 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}
+    modify fun s => {s with failures := s.failures.push caption}
   let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
-  if hasOutput ∨ (showProgress ∧ (action ≥ minAction)) then
+  if hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction) 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 := s!"{icon} [{jobNo}/{totalJobs}] {verb} {caption}"
     let caption :=
       if useAnsi then
         let color := if hasOutput then maxLv.ansiColor else "32"
@@ -113,33 +123,36 @@ def reportJob (job : Job Unit) : MonitorM PUnit := do
       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
+def poll (jobs : Array OpaqueJob): MonitorM (Array OpaqueJob × Array OpaqueJob) := do
+  jobs.foldlM (init := (#[], #[])) fun (running, unfinished) job => do
+    match (← IO.getTaskState job.task) with
+    | .finished =>
       reportJob job
       modify fun s => {s with jobNo := s.jobNo + 1}
-    else
-      modify fun s => {s with jobs := s.jobs.push job}
+      return (running, unfinished)
+    | .running =>
+      return (running.push job, unfinished.push job)
+    | .waiting =>
+      return (running, unfinished.push job)
 
 def sleep : MonitorM PUnit := do
   let now ← IO.monoMsNow
-  let lastUpdate ← modifyGet fun s => (s.lastUpdate, {s with lastUpdate := now})
+  let lastUpdate := (← get).lastUpdate
   let sleepTime : Nat := (← read).updateFrequency - (now - lastUpdate)
   if sleepTime > 0 then
     IO.sleep sleepTime.toUInt32
+  let now ← IO.monoMsNow
+  modify fun s => {s with lastUpdate := now}
 
-partial def loop : MonitorM PUnit := do
-  renderProgress
-  pollJobs
-  if 0 < (← get).jobs.size then
-    renderProgress
+partial def loop (jobs : Array OpaqueJob) : MonitorM PUnit := do
+  let (running, unfinished) ← poll jobs
+  if h : 0 < unfinished.size then
+    renderProgress running unfinished h
     sleep
-    loop
+    loop unfinished
 
-def main : MonitorM PUnit := do
-  loop
+def main (jobs : Array OpaqueJob) : MonitorM PUnit := do
+  loop jobs
   let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
   unless resetCtrl.isEmpty do
     print resetCtrl
@@ -149,7 +162,7 @@ end Monitor
 
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
 def monitorJobs
-  (jobs : Array (Job Unit))
+  (jobs : Array OpaqueJob)
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (minAction : JobAction)
@@ -164,11 +177,11 @@ def monitorJobs
     useAnsi, showProgress, updateFrequency
   }
   let s := {
-    jobs, resetCtrl
+    resetCtrl
     lastUpdate := ← IO.monoMsNow
     failures := initFailures
   }
-  let (_,s) ← Monitor.main.run ctx s
+  let (_,s) ← Monitor.main jobs |>.run ctx s
   return s.failures
 
 /--

src/lake/Lake/Util/Log.lean

@@ -242,6 +242,7 @@ instance : FromJson Log := ⟨(Log.mk <$> fromJson? ·)⟩
 /-- A position in a `Log` (i.e., an array index). Can be past the log's end. -/
 structure Log.Pos where
   val : Nat
+  deriving Inhabited
 
 instance : OfNat Log.Pos (nat_lit 0) := ⟨⟨0⟩⟩
 

src/lake/Lake/Util/Opaque.lean

@@ -34,7 +34,6 @@ macro (name := hydrateOpaqueType)
   let unsafeMk := mkIdent `unsafeMk
   let get := mkIdent `get
   let unsafeGet := mkIdent `unsafeGet
-  let get_mk := mkIdent `get_mk
   `(
   namespace $oty
   unsafe def $unsafeMk : $ty $args* → $oty $args* := unsafeCast
@@ -46,7 +45,5 @@ macro (name := hydrateOpaqueType)
   instance : Coe ($oty $args*) ($ty $args*) := ⟨$get⟩
 
   instance [Inhabited ($ty $args*)] : Inhabited ($oty $args*) := ⟨$mk default⟩
-
-  @[simp] axiom $get_mk $[{$args}]* {x : $ty $args*} : $get ($mk x) = x
   end $oty
   )

src/lake/Lake/Util/Task.lean

@@ -15,6 +15,7 @@ abbrev OptionTask := OptionT Task
 
 def BaseIOTask := Task
 instance : Monad BaseIOTask := inferInstanceAs <| Monad Task
+instance [Inhabited α] : Inhabited (BaseIOTask α) := inferInstance
 
 abbrev EIOTask ε := ExceptT ε BaseIOTask
 abbrev OptionIOTask := OptionT BaseIOTask