diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean index dbc3b5c007..919ed3b9e7 100644 --- a/src/lake/Lake/Build/Context.lean +++ b/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. diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 5489b2dd91..06916ec8ce 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/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" diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 4ac6becef7..6e688ef66c 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/examples/targets/test.sh b/src/lake/examples/targets/test.sh index 9bd3f5ca9d..d598dbb657 100755 --- a/src/lake/examples/targets/test.sh +++ b/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' diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh index 71d92db2cf..7ff6ed7538 100755 --- a/src/lake/tests/noRelease/test.sh +++ b/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