feat: lake: build times & --no-build jobs (#9677)

This PR adds build times to each build step of the build monitor (under
`-v` or in CI) and delays exiting on a `--no-build` until after the
build monitor finishes. Thus, a `--no-build` failure will now report
which targets blocked Lake by needing a rebuild.

src/lake/Lake/Build/Common.lean

@@ -25,9 +25,6 @@ instance : MonadWorkspace JobM := inferInstance
 
 scoped instance : ToJson PUnit := ⟨fun _ => Json.null⟩
 
-/-- Exit code to return if `--no-build` is set and a build is required. -/
-def noBuildCode : ExitCode := 3
-
 open System.Platform in
 /--
 Build trace for the host platform.
@@ -230,14 +227,22 @@ and log are saved to `traceFile`, if the build completes without a fatal error
   (action : JobAction := .build)
 : JobM α := do
   if (← getNoBuild) then
-    IO.Process.exit noBuildCode.toUInt8
+    updateAction .build
+    error "target is out-of-date and needs to be rebuilt"
   else
     updateAction action
-    let iniPos ← getLogPos
-    let outputs ← build -- fatal errors will abort here
-    let log := (← getLog).takeFrom iniPos
-    writeBuildTrace traceFile depTrace outputs log
-    return outputs
+    let startTime ← IO.monoMsNow
+    try
+      let iniPos ← getLogPos
+      let outputs ← build -- fatal errors will abort here
+      let log := (← getLog).takeFrom iniPos
+      writeBuildTrace traceFile depTrace outputs log
+      return outputs
+    finally
+      let endTime ← IO.monoMsNow
+      let elapsed := endTime - startTime
+      modify fun s => {s with buildTime := s.buildTime + elapsed}
+
 
 /--
 Checks whether `info` is up-to-date, and runs `build` to recreate it if not.

src/lake/Lake/Build/Job/Basic.lean

@@ -59,12 +59,15 @@ structure JobState where
   action : JobAction := .unknown
   /-- Current trace of a build job. -/
   trace : BuildTrace := .nil
+  /-- How long the job spent building (in milliseconds). -/
+  buildTime : Nat := 0
   deriving Inhabited
 
 def JobState.merge (a b : JobState) : JobState where
   log := a.log ++ b.log
   action := a.action.merge b.action
   trace := mixTrace a.trace b.trace
+  buildTime := a.buildTime + b.buildTime
 
 @[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) : JobState :=
   {s with log := f s.log}

src/lake/Lake/Build/Run.lean

@@ -42,6 +42,7 @@ structure MonitorContext where
   showOptional : Bool
   useAnsi : Bool
   showProgress : Bool
+  showTime : Bool
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat
 
@@ -49,6 +50,7 @@ structure MonitorContext where
 structure MonitorState where
   jobNo : Nat := 0
   totalJobs : Nat := 0
+  didBuild : Bool := false
   failures : Array String
   resetCtrl : String
   lastUpdate : Nat
@@ -104,24 +106,29 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
     print s!"{resetCtrl}{spinnerIcon} [{jobNo}/{totalJobs}] {caption}"
     flush
 
+
+
 def reportJob (job : OpaqueJob) : MonitorM PUnit := do
-  let {jobNo, totalJobs, ..} ← get
-  let {failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, ..} ← read
+  let {jobNo, totalJobs, didBuild, ..} ← get
+  let {failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, showTime, ..} ← read
   let {task, caption, optional, ..} := job
-  let {log, action, ..} := task.get.state
+  let {log, action, buildTime, ..} := task.get.state
   let maxLv := log.maxLv
-  let failed := log.hasEntries ∧ maxLv ≥ failLv
-  if failed ∧ ¬optional then
+  let failed := strictAnd log.hasEntries (maxLv ≥ failLv)
+   if !didBuild && action = .build then
+    modify fun s => {s with didBuild := true}
+  if failed && !optional then
     modify fun s => {s with failures := s.failures.push caption}
-  let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
+  let hasOutput := failed || (log.hasEntries && maxLv ≥ outLv)
   let showJob :=
-    (¬ optional ∨ showOptional) ∧
-    (hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction))
+    (!optional || showOptional) &&
+    (hasOutput || (showProgress && !useAnsi && action ≥ minAction))
   if showJob then
     let verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
     let opt := if optional then " (Optional)" else ""
-    let caption := s!"{icon} [{jobNo}/{totalJobs}]{opt} {verb} {caption}"
+    let time := if showTime && buildTime > 0 then s!" ({formatTime buildTime})" else ""
+    let caption := s!"{icon} [{jobNo}/{totalJobs}]{opt} {verb} {caption}{time}"
     let caption :=
       if useAnsi then
         let color := if hasOutput then maxLv.ansiColor else "32"
@@ -134,6 +141,11 @@ def reportJob (job : OpaqueJob) : MonitorM PUnit := do
       let outLv := if failed then .trace else outLv
       log.replay (logger := .stream out outLv useAnsi)
     flush
+where
+  formatTime ms :=
+    if ms > 10000 then s!"{ms / 1000}s"
+    else if ms > 1000 then s!"{(ms) / 1000}.{(ms+50) / 100 % 10}s"
+    else s!"{ms}ms"
 
 def poll (unfinished : Array OpaqueJob) : MonitorM (Array OpaqueJob × Array OpaqueJob) := do
   let newJobs ← (← read).jobs.modifyGet ((·, #[]))
@@ -177,6 +189,7 @@ def main (init : Array OpaqueJob) : MonitorM PUnit := do
 end Monitor
 
 structure MonitorResult where
+  didBuild : Bool
   failures : Array String
   numJobs : Nat
 
@@ -187,14 +200,14 @@ def monitorJobs
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
   (minAction : JobAction)
-  (showOptional useAnsi showProgress : Bool)
+  (showOptional useAnsi showProgress showTime : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
   (updateFrequency := 100)
 : BaseIO MonitorResult := do
   let ctx := {
     jobs, out, failLv, outLv, minAction, showOptional
-    useAnsi, showProgress, updateFrequency
+    useAnsi, showProgress, showTime, updateFrequency
   }
   let s := {
     resetCtrl
@@ -202,7 +215,11 @@ def monitorJobs
     failures := initFailures
   }
   let (_,s) ← Monitor.main initJobs |>.run ctx s
-  return {failures := s.failures, numJobs := s.totalJobs}
+  return {
+    failures := s.failures
+    numJobs := s.totalJobs
+    didBuild := s.didBuild
+  }
 
 /-- Save input mappings to the local Lake artifact cache (if enabled). -/
 def Workspace.saveInputs (ws : Workspace) : LogIO Unit := do
@@ -212,6 +229,9 @@ def Workspace.saveInputs (ws : Workspace) : LogIO Unit := do
         let inputsFile := pkg.inputsFileIn ws.lakeCache
         (← ref.get).save inputsFile
 
+/-- Exit code to return if `--no-build` is set and a build is required. -/
+def noBuildCode : ExitCode := 3
+
 /--
 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
@@ -225,6 +245,7 @@ def Workspace.runFetchM
   let useAnsi ← cfg.ansiMode.isEnabled out
   let outLv := cfg.outLv
   let failLv := cfg.failLv
+  let isVerbose := cfg.verbosity = .verbose
   let showProgress := cfg.showProgress
   let showSuccess := cfg.showSuccess
   let ctx ← mkBuildContext ws cfg
@@ -233,33 +254,41 @@ def Workspace.runFetchM
   let compute := Job.async build (caption := caption)
   let job ← compute.run.run'.run ctx |>.run nilTrace
   -- Job Monitor
-  let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
-  let showOptional := cfg.verbosity = .verbose
-  let {failures, numJobs} ← monitorJobs #[job] ctx.registeredJobs
-    out failLv outLv minAction showOptional useAnsi showProgress
+  let minAction := if isVerbose then .unknown else .fetch
+  let showOptional := isVerbose
+  let showTime := isVerbose || !useAnsi
+  let {failures, numJobs, didBuild} ← monitorJobs #[job] ctx.registeredJobs
+    out failLv outLv minAction showOptional useAnsi showProgress showTime
   -- Save input mappings to cache
   match (← ws.saveInputs {}) with
   | .ok _ log =>
-    if !log.isEmpty && cfg.verbosity = .verbose then
+    if !log.isEmpty && isVerbose then
       print! out "There were issues saving input mappings to the local artifact cache:\n"
       log.replay (logger := .stream out outLv useAnsi)
   | .error _ log =>
     print! out "Failed to save input mappings to the local artifact cache.\n"
-    if cfg.verbosity = .verbose then
+    if isVerbose then
       log.replay (logger := .stream out outLv useAnsi)
-  -- Failure Report
+  -- Report
+  let isNoBuild := cfg.noBuild
   if failures.isEmpty then
     let some a ← job.wait?
-      | error "top-level build failed"
+      | error "uncaught top-level build failure (this is likely a bug in Lake)"
     if showProgress && showSuccess then
       let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
-      print! out s!"Build completed successfully ({jobs}).\n"
+      if isNoBuild then
+        print! out s!"All targets up-to-date ({jobs}).\n"
+      else
+        print! out s!"Build completed successfully ({jobs}).\n"
     return a
   else
-    print! out "Some required builds logged failures:\n"
+    print! out "Some required targets logged failures:\n"
     failures.forM (print! out s!"- {·}\n")
     flush out
-    error "build failed"
+    if isNoBuild && didBuild then
+      IO.Process.exit noBuildCode.toUInt8
+    else
+      error "build failed"
 
 /-- Run a build function in the Workspace's context and await the result. -/
 @[inline] def Workspace.runBuild

src/lake/tests/common.sh

@@ -200,9 +200,9 @@ test_err() {
   expected=$1; shift
   if lake_out "$@"; then rc=$?; else rc=$?; fi
   if match_text "$expected" produced.out; then
-    if [ $rc != 1 ]; then
+    if [ $rc == 0 ]; then
       echo "FAILURE: Lake unexpectedly succeeded"
-      return 1
+      return $rc
     fi
   else
     return 1
@@ -256,14 +256,13 @@ test_err_diff() {
   echo '$' lake "$@"
   if "$LAKE" "$@" >produced.out 2>&1; then rc=$?; else rc=$?; fi
   if check_diff_core produced.expected.out produced.out; then
-    if [ $rc != 1 ]; then
+    if [ $rc == 0 ]; then
       echo "FAILURE: Lake unexpectedly succeeded"
       return 1
     fi
+    echo "Lake exited with code $rc"
   else
-    if [ $rc != 1 ]; then
-      echo "Lake exited with code $rc."
-    fi
+    echo "Lake exited with code $rc"
     return 1
   fi
 }

src/lake/tests/noBuild/test.sh

@@ -11,6 +11,7 @@ NO_BUILD_CODE=3
 # Test `--no-build` for setup-file and module builds (`buildUnlessUpToDate`)
 echo "# TEST: --no-build setup-file & modules"
 test_status $NO_BUILD_CODE setup-file ImportTest.lean --no-build
+test_err "Building Test" setup-file ImportTest.lean --no-build
 test ! -f .lake/build/lib/lean/Test.olean
 test_run build Test
 test -f .lake/build/lib/lean/Test.olean
@@ -19,10 +20,11 @@ test_run setup-file ImportTest.lean --no-build
 # Test `--no-build` for file builds (`buildFileUnlessUpToDate`)
 echo "# TEST: --no-build file"
 test_status $NO_BUILD_CODE build +Test:c.o.export --no-build
+test_err "Building Test:c.o" build +Test:c.o.export --no-build
 test ! -f .lake/build/ir/Test.c.o.export
 test_run build +Test:c.o.export
 test -f .lake/build/ir/Test.c.o.export
-test_run build +Test:c.o.export --no-build
+test_out "All targets up-to-date" build +Test:c.o.export --no-build
 
 # cleanup
 rm -f produced.out

src/lake/tests/noRelease/test.sh

@@ -35,7 +35,7 @@ echo "# TEST: Direct fetch"
 test_err_diff <(cat << EOF
 ✖ [2/2] Running dep:release
 error: failed to fetch GitHub release (run with '-v' for details)
-Some required builds logged failures:
+Some required targets logged failures:
 - dep:release
 error: build failed
 EOF
@@ -46,11 +46,8 @@ echo "# TEST: Indirect fetch"
 test_out_diff <(cat << EOF
 ⚠ [3/6] Ran dep:extraDep
 warning: building from source; failed to fetch GitHub release (run with '-v' for details)
-✔ [4/6] Built Dep
-✔ [5/6] Built Test
-Build completed successfully (6 jobs).
 EOF
-) build Test
+) build Test -q
 
 # Test download failure
 echo "# TEST: Download failure"