From 7ece5d56e37bbc7561174c842b05910ba4cc7533 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 20 May 2024 16:29:21 -0400 Subject: [PATCH] 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 | 2 +- src/lake/Lake/Build/Basic.lean | 102 +------------------------ src/lake/Lake/Build/Fetch.lean | 23 +++--- src/lake/Lake/Build/Job.lean | 125 ++++++++++++++++++++++++++++++- src/lake/Lake/Build/Run.lean | 79 +++++++++++-------- src/lake/Lake/Util/Log.lean | 1 + src/lake/Lake/Util/Opaque.lean | 3 - src/lake/Lake/Util/Task.lean | 1 + 8 files changed, 189 insertions(+), 147 deletions(-) diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 8abfcee8d1..6edc0024a9 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/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. diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index 93b5b502e1..4e54ebbf4b 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/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 diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index 977bca9c6f..e6b94e3fa3 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/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 diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 3ea28eebf8..00617dcf59 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/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 α := diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 4f9dabcd96..d49c93fa75 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/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 /-- diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index 9d705a4ee5..f1136fee89 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/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⟩⟩ diff --git a/src/lake/Lake/Util/Opaque.lean b/src/lake/Lake/Util/Opaque.lean index a60486e58f..9905ab5954 100644 --- a/src/lake/Lake/Util/Opaque.lean +++ b/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 ) diff --git a/src/lake/Lake/Util/Task.lean b/src/lake/Lake/Util/Task.lean index 5d988737fb..c986852fd1 100644 --- a/src/lake/Lake/Util/Task.lean +++ b/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