feat: lake: job count in build success message (#9436)

This PR adds the number of jobs run to the final message Lake produces
on a successfully run of `lake build`.


**Examples**
```
Build completed successfully (1 job).
Build completed successfully (6 jobs).
```

src/lake/Lake/Build/Context.lean

@@ -37,6 +37,8 @@ structure BuildConfig where
   out : OutStream := .stderr
   /-- Whether to use ANSI escape codes in build output. -/
   ansiMode : AnsiMode := .auto
+  /-- Whether to print a message when the build finishes successfully (if not quiet). -/
+  showSuccess : Bool := false
 
 /--
 Whether the build should show progress information.

src/lake/Lake/Build/Run.lean

@@ -176,6 +176,10 @@ def main (init : Array OpaqueJob) : MonitorM PUnit := do
 
 end Monitor
 
+structure MonitorResult where
+  failures : Array String
+  numJobs : Nat
+
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
 def monitorJobs
   (initJobs : Array OpaqueJob)
@@ -187,7 +191,7 @@ def monitorJobs
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
   (updateFrequency := 100)
-: BaseIO (Array String) := do
+: BaseIO MonitorResult := do
   let ctx := {
     jobs, out, failLv, outLv, minAction, showOptional
     useAnsi, showProgress, updateFrequency
@@ -198,7 +202,7 @@ def monitorJobs
     failures := initFailures
   }
   let (_,s) ← Monitor.main initJobs |>.run ctx s
-  return s.failures
+  return {failures := s.failures, numJobs := s.totalJobs}
 
 /-- Save input mappings to the local Lake artifact cache (if enabled). -/
 def Workspace.saveInputs (ws : Workspace) : LogIO Unit := do
@@ -222,6 +226,7 @@ def Workspace.runFetchM
   let outLv := cfg.outLv
   let failLv := cfg.failLv
   let showProgress := cfg.showProgress
+  let showSuccess := cfg.showSuccess
   let ctx ← mkBuildContext ws cfg
   -- Job Computation
   let caption := "job computation"
@@ -230,7 +235,7 @@ def Workspace.runFetchM
   -- Job Monitor
   let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
   let showOptional := cfg.verbosity = .verbose
-  let failures ← monitorJobs #[job] ctx.registeredJobs
+  let {failures, numJobs} ← monitorJobs #[job] ctx.registeredJobs
     out failLv outLv minAction showOptional useAnsi showProgress
   -- Save input mappings to cache
   match (← ws.saveInputs {}) with
@@ -246,6 +251,9 @@ def Workspace.runFetchM
   if failures.isEmpty then
     let some a ← job.wait?
       | error "top-level build failed"
+    if showProgress && showSuccess then
+      let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
+      print! out s!"Build completed successfully ({jobs}).\n"
     return a
   else
     print! out "Some required builds logged failures:\n"

src/lake/Lake/CLI/Main.lean

@@ -92,7 +92,9 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig := d
   }
 
 /-- Make a `BuildConfig` from a `LakeOptions`. -/
-def LakeOptions.mkBuildConfig (opts : LakeOptions) (out := OutStream.stderr) : BuildConfig where
+def LakeOptions.mkBuildConfig
+  (opts : LakeOptions) (out := OutStream.stderr) (showSuccess := false)
+: BuildConfig where
   oldMode := opts.oldMode
   trustHash := opts.trustHash
   noBuild := opts.noBuild
@@ -100,7 +102,7 @@ def LakeOptions.mkBuildConfig (opts : LakeOptions) (out := OutStream.stderr) : B
   failLv := opts.failLv
   outLv := opts.outLv
   ansiMode := opts.ansiMode
-  out := out
+  out; showSuccess
 
 export LakeOptions (mkLoadConfig mkBuildConfig)
 
@@ -361,11 +363,8 @@ protected def build : CliM PUnit := do
   specs.forM fun spec =>
     unless spec.buildable do
       throw <| .invalidBuildTarget spec.info.key.toSimpleString
-  let buildConfig := mkBuildConfig opts (out := .stdout)
-  let showProgress := buildConfig.showProgress
+  let buildConfig := mkBuildConfig opts (out := .stdout) (showSuccess := true)
   ws.runBuild (buildSpecs specs) buildConfig
-  if showProgress then
-    IO.println "Build completed successfully."
 
 protected def checkBuild : CliM PUnit := do
   processOptions lakeOption

src/lake/examples/targets/test.sh

@@ -31,7 +31,7 @@ EOF
 $LAKE build targets/bark_bark | awk '/Ran/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
 ℹ [1/2] Ran targets/bark
 info: Bark!
-Build completed successfully.
+Build completed successfully (2 jobs).
 EOF
 ) -
 $LAKE build targets:print_name | awk '/Ran/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF'

src/lake/tests/noRelease/test.sh

@@ -48,7 +48,7 @@ test_out_diff <(cat << EOF
 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.
+Build completed successfully (6 jobs).
 EOF
 ) build Test
 
@@ -58,7 +58,7 @@ test_run update # re-fetch release tag
 test_err "curl" -v build dep:release
 
 # Test automatic cloud release unpacking
-echo "# TEST: Automaticcloud release unpacking"
+echo "# TEST: Automatic cloud release unpacking"
 mkdir -p .lake/packages/dep/.lake/build
 test_out "packing" -d .lake/packages/dep pack
 test_exp -f .lake/packages/dep/.lake/release.tgz
@@ -70,14 +70,14 @@ test_exp -d .lake/packages/dep/.lake/build
 # Test that the job prints nothing if the archive is already fetched and unpacked
 echo "# TEST: Quiet if fetched"
 test_out_diff <(cat << 'EOF'
-Build completed successfully.
+Build completed successfully (2 jobs).
 EOF
 ) build dep:release
 
 # Test that releases do not contaminate downstream jobs
 echo "# TEST: Downstream job contamination"
 test_out_diff <(cat << 'EOF'
-Build completed successfully.
+Build completed successfully (5 jobs).
 EOF
 ) build Test