feat: lake: pretty progress

leanprover · Apr 18, 2024 · 8135218 · 8135218
1 parent 10e4a92
commit 8135218
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 21 deletions.
diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean
@@ -39,32 +39,33 @@ def FetchM.run (x : FetchM α) : RecBuildM α :=
 def monitorBuildJobs
   (ctx : BuildContext) (out : IO.FS.Stream) (spawner : CoreBuildM α)
 : IO (Option α) := do
-  print "[?/?] Computing build jobs"
+  out.putStr "[?/?] Computing build jobs"
   let (io, a?, log) ← IO.FS.withIsolatedStreams (spawner.run ctx).captureLog
   if io.isEmpty && log.isEmpty then
     resetLine
   else
-    print "\n"
-    unless log.isEmpty do
+    out.putStr "\n"
+    if log.hasVisibleEntries ctx.verbosity then
       log.replay (logger := MonadLog.stream out ctx.verbosity)
     unless io.isEmpty do
       out.putStr "stdout/stderr:\n"
       out.putStr io
+  out.flush
   let jobs ← ctx.buildJobs.get
   let numJobs := jobs.size
   numJobs.forM fun i => do
     let (caption, job) := jobs[i]!
-    print s!"[{i+1}/{numJobs}] {caption}"
+    out.putStr s!"[{i+1}/{numJobs}] {caption}"
     let log := (← IO.wait job.task).state
-    if log.isEmpty then
+    if !log.hasVisibleEntries ctx.verbosity then
       resetLine
     else
-      print "\n"
+      out.putStr "\n"
       log.replay (logger := MonadLog.stream out ctx.verbosity)
+    out.flush
   return a?
 where
-  print s := out.putStr s
-  resetLine := print "\n" --"\x1B[2K\r"
+  resetLine := do if (← out.isTty) then out.putStr "\x1B[2K\r" else out.putStr "\n"
 
 /-- The name of the Lake build lock file name (i.e., `lake.lock`). -/
 def lockFileName : String :=

diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
@@ -8,6 +8,14 @@ import Lake.Util.EStateT
 
 namespace Lake
 
+inductive Verbosity
+| quiet
+| normal
+| verbose
+deriving Repr, DecidableEq, Ord
+
+instance : Inhabited Verbosity := ⟨.normal⟩
+
 inductive LogLevel
 | trace
 | info
@@ -23,13 +31,11 @@ protected def LogLevel.toString : LogLevel → String
 
 instance : ToString LogLevel := ⟨LogLevel.toString⟩
 
-inductive Verbosity
-| quiet
-| normal
-| verbose
-deriving Repr, DecidableEq, Ord
-
-instance : Inhabited Verbosity := ⟨.normal⟩
+def LogLevel.visibleAtVerbosity (self : LogLevel) (verbosity : Verbosity) : Bool :=
+  match self with
+  | .trace => verbosity == .verbose
+  | .info => verbosity != .quiet
+  | _ => true
 
 structure LogEntry where
   level : LogLevel
@@ -162,6 +168,12 @@ 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)
+
+def hasVisibleEntries (log : Log) (verbosity := Verbosity.normal) : Bool :=
+  log.entries.any (·.level.visibleAtVerbosity verbosity)
+
 end Log
 
 abbrev LogT (m : Type → Type) :=
@@ -206,12 +218,6 @@ instance [Monad m] : MonadError (ELogT m) := ⟨ELogT.error⟩
   | .error n log => let (h,t) := log.split n; f h t
   | .ok a log => return (a, log)
 
-def filterByVerbosity (log : Log) (verbosity := Verbosity.normal) : Log := log.filter fun e =>
-  match e.level with
-  | .trace => verbosity == .verbose
-  | .info => verbosity != .quiet
-  | _ => true
-
 @[inline] def captureLog [Monad m] (self : ELogT m α) : m (Option α × Log) := do
  match (← self {}) with
  | .ok a log => return (some a, log)