refactor: lake: --wfail & track jobs & logs & simplify build monads (#3835)

This is a major refactor of Lake's build code.  The key changes:

* **Job Registration**: Significant build jobs are now registered by
build functions. The DSL inserts this registration automatically into
user-defined targets and facets, so this change should require no
end-user adaption. Registered jobs are incrementally awaited by the main
build function and the progress counter now indicates how many of these
jobs are completed and left-to-await. On the positive side, this means
the counter is now always accurate. On the negative side, this means
that jobs are displayed even if they are no-ops (i.e., if the target is
already up-to-date).

* **Log Retention**: Logs are now part of a Lake monad's state instead
of being eagerly printed. As a result, build jobs retain their logs.
Using this change, logs are are now always printed after their
associated caption (e.g., `[X/Y] Building Foo`) and are not arbitrarily
interleaved with the output of other jobs.

* **Simplify the build monad stack**: Previously, there was a lot of
confused mixing between the various build monads in the codebase (i.e.,
`JobM`, `ScedulerM`, `BuildM`, `RecBuildM`, and `IndexBuildM` ). This
refactor attempts to make there use more consistent and straightforward:
* `FetchM` (formerly `IndexBuildM`) is the top-level build monad used by
targets and facets and is now uniformly used in the codebase for all
top-level build functions.
* `JobM` is the monad of asynchronous build jobs. It is more limited
than `FetchM` due to the fact that the build cache can not be modified
asynchronously.
* `SpawnM` (formerly `SchedulerM`) is the monad used to spawn build
jobs. It lifts into `FetchM`.
* `RecBuildM` and `CoreBuildM` (formerly `BuildM`) have been relegated
to internal details of how `FetchM` / `JobM` are implemented / run and
are no longer used outside of that context.

* **Pretty progress.** Build progress (e.g., `[X/Y] Building Foo`) is
now updated on a single line via ANSI escape sequences when Lake is
outputting to a terminal. Redirected Lake output still sees progress on
separate lines.

* **Warnings-as-error option.** Adds a `--wfail` option to Lake that
will cause a build to fail if Lake logs any warnings doing a build.
Unlike some systems, this does not convert warnings into errors and it
does not abort jobs which log warnings. Instead, only the top-level
build fails.

* **Build log cache.** Logs from builds are now cached to a file and
replayed when the build is revisited. For example, this means multiple
runs of a `--wfail` Lean build (without changes) will still produce the
same warnings even though there is now an up-to-date `.olean` for the
module.

 Closes #2349. Closes #2764.

src/lake/Lake/Build.lean

@@ -3,10 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Monad
-import Lake.Build.Actions
-import Lake.Build.Index
+import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Build.Package
 import Lake.Build.Library
 import Lake.Build.Imports
+import Lake.Build.Targets

src/lake/Lake/Build/Actions.lean

@@ -5,22 +5,24 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 import Lake.Util.Proc
 import Lake.Util.NativeLib
-import Lake.Build.Context
+import Lake.Build.Basic
 
 /-! # Common Build Actions
-Low level actions to build common Lean artfiacts via the Lean toolchain.
+Low level actions to build common Lean artifacts via the Lean toolchain.
 -/
 
-namespace Lake
 open System
+open Lean hiding SearchPath
 
-def compileLeanModule (name : String) (leanFile : FilePath)
-(oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
-(leanPath : SearchPath := []) (rootDir : FilePath := ".")
-(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
-(leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: BuildM Unit := do
-  logStep s!"Building {name}"
+namespace Lake
+
+def compileLeanModule
+  (leanFile : FilePath)
+  (oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
+  (leanPath : SearchPath := []) (rootDir : FilePath := ".")
+  (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
+  (leanArgs : Array String := #[]) (lean : FilePath := "lean")
+: JobM Unit := do
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -37,7 +39,10 @@ def compileLeanModule (name : String) (leanFile : FilePath)
     args := args ++ #["-b", bcFile.toString]
   for dynlib in dynlibs do
     args := args.push s!"--load-dynlib={dynlib}"
-  proc {
+  args := args.push "--json"
+  show LogIO _ from do
+  let iniSz ← getLogSize
+  let out ← rawProc {
     args
     cmd := lean.toString
     env := #[
@@ -45,37 +50,59 @@ def compileLeanModule (name : String) (leanFile : FilePath)
       (sharedLibPathEnvVar, (← getSearchPath sharedLibPathEnvVar) ++ dynlibPath |>.toString)
     ]
   }
+  unless out.stdout.isEmpty do
+    let txt ← out.stdout.split (· == '\n') |>.foldlM (init := "") fun txt ln => do
+      if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
+        unless txt.isEmpty do
+          logInfo s!"stdout:\n{txt}"
+        logSerialMessage msg
+        return txt
+      else if txt.isEmpty && ln.isEmpty then
+        return txt
+      else
+        return txt ++ ln ++ "\n"
+    unless txt.isEmpty do
+      logInfo s!"stdout:\n{txt}"
+  unless out.stderr.isEmpty do
+    logInfo s!"stderr:\n{out.stderr}"
+  if out.exitCode ≠ 0 then
+    logError s!"Lean exited with code {out.exitCode}"
+    throw iniSz
 
-def compileO (name : String) (oFile srcFile : FilePath)
-(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Compiling {name}"
+def compileO
+  (oFile srcFile : FilePath)
+  (moreArgs : Array String := #[]) (compiler : FilePath := "cc")
+: JobM Unit := do
   createParentDirs oFile
   proc {
     cmd := compiler.toString
     args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
   }
 
-def compileStaticLib (name : String) (libFile : FilePath)
-(oFiles : Array FilePath) (ar : FilePath := "ar") : BuildM Unit := do
-  logStep s!"Creating {name}"
+def compileStaticLib
+  (libFile : FilePath) (oFiles : Array FilePath)
+  (ar : FilePath := "ar")
+: JobM Unit := do
   createParentDirs libFile
   proc {
     cmd := ar.toString
     args := #["rcs", libFile.toString] ++ oFiles.map toString
   }
 
-def compileSharedLib (name : String) (libFile : FilePath)
-(linkArgs : Array String) (linker : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Linking {name}"
+def compileSharedLib
+  (libFile : FilePath) (linkArgs : Array String)
+  (linker : FilePath := "cc")
+: JobM Unit := do
   createParentDirs libFile
   proc {
     cmd := linker.toString
     args := #["-shared", "-o", libFile.toString] ++ linkArgs
   }
 
-def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
-(linkArgs : Array String := #[]) (linker : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Linking {name}"
+def compileExe
+  (binFile : FilePath) (linkFiles : Array FilePath)
+  (linkArgs : Array String := #[]) (linker : FilePath := "cc")
+: JobM Unit := do
   createParentDirs binFile
   proc {
     cmd := linker.toString
@@ -83,46 +110,39 @@ def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/
-def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do
-  logVerbose s!"Downloading {name}"
+def download  (url : String) (file : FilePath) : LogIO PUnit := do
   if (← file.pathExists) then
     IO.FS.removeFile file
   else
     createParentDirs file
-  let args :=
-    if (← getIsVerbose) then #[] else #["-s"]
   proc (quiet := true) {
     cmd := "curl"
-    args := args ++ #["-f", "-o", file.toString, "-L", url]
+    args := #["-f", "-o", file.toString, "-L", url]
   }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
-def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
-  logVerbose s!"Unpacking {name}"
+def untar (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
   IO.FS.createDirAll dir
-  let mut opts := "-x"
-  if (← getIsVerbose) then
-    opts := opts.push 'v'
+  let mut opts := "-xvv"
   if gzip then
     opts := opts.push 'z'
-  proc {
+  proc (quiet := true) {
     cmd := "tar",
     args := #[opts, "-f", file.toString, "-C", dir.toString]
   }
 
 /-- Pack a directory `dir` using `tar` into the archive `file`. -/
-def tar (name : String) (dir : FilePath) (file : FilePath)
-(gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do
-  logVerbose s!"Packing {name}"
+def tar
+  (dir : FilePath) (file : FilePath)
+  (gzip := true) (excludePaths : Array FilePath := #[])
+: LogIO PUnit := do
   createParentDirs file
-  let mut args := #["-c"]
+  let mut args := #["-cvv"]
   if gzip then
     args := args.push "-z"
-  if (← getIsVerbose) then
-    args := args.push "-v"
   for path in excludePaths do
     args := args.push s!"--exclude={path}"
-  proc {
+  proc (quiet := true) {
     cmd := "tar"
     args := args ++ #["-f", file.toString, "-C", dir.toString, "."]
     -- don't pack `._` files on MacOS

src/lake/Lake/Build/Basic.lean

@@ -6,12 +6,9 @@ Authors: Mac Malone
 import Lake.Util.Log
 import Lake.Util.Exit
 import Lake.Util.Task
-import Lake.Util.Error
-import Lake.Util.OptionIO
+import Lake.Util.Lift
 import Lake.Config.Context
 import Lake.Build.Trace
-import Lake.Build.Store
-import Lake.Build.Topological
 
 open System
 namespace Lake
@@ -25,16 +22,35 @@ structure BuildConfig where
   trustHash : Bool := true
   /-- Early exit if a target has to be rebuilt. -/
   noBuild : Bool := false
+  verbosity : Verbosity := .normal
+  /--
+  Fail the top-level build if warnings have been logged.
+  Unlike some build systems, this does **NOT** convert warnings to errors,
+  and it does not abort jobs when warnings are logged (i.e., dependent jobs
+  will still continue unimpeded).
+  -/
+  failIfWarnings : Bool := false
+  /-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
+  useStdout : Bool := false
+
+abbrev JobResult α := EResult Nat Log α
+abbrev JobTask α := BaseIOTask (JobResult α)
+
+/-- A Lake job. -/
+structure Job (α : Type u)  where
+  task : JobTask α
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  startedBuilds : IO.Ref Nat
-  finishedBuilds : IO.Ref Nat
+  registeredJobs : IO.Ref (Array (String × Job Unit))
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
 
+instance [Pure m] : MonadLift LakeM (BuildT m) where
+  monadLift x := fun ctx => pure <| x.run ctx.toContext
+
 @[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
   (·.leanTrace) <$> readThe BuildContext
 
@@ -50,37 +66,23 @@ abbrev BuildT := ReaderT BuildContext
 @[inline] def getNoBuild [Monad m] : BuildT m Bool :=
   (·.noBuild) <$> getBuildConfig
 
-/-- The monad for the Lake build manager. -/
-abbrev SchedulerM := BuildT <| LogT BaseIO
+@[inline] def getVerbosity [Monad m] : BuildT m Verbosity :=
+  (·.verbosity) <$> getBuildConfig
 
-/-- The core monad for Lake builds. -/
-abbrev BuildM := BuildT LogIO
+@[inline] def getIsVerbose [Monad m] : BuildT m Bool :=
+  (· == .verbose) <$> getVerbosity
 
-/-- A transformer to equip a monad with a Lake build store. -/
-abbrev BuildStoreT := StateT BuildStore
+@[inline] def getIsQuiet [Monad m] : BuildT m Bool :=
+  (· == .quiet) <$> getVerbosity
 
-/-- A Lake build cycle. -/
-abbrev BuildCycle := Cycle BuildKey
+/-- The internal core monad of Lake builds.  Not intended for user use. -/
+abbrev CoreBuildM := BuildT LogIO
 
-/-- A transformer for monads that may encounter a build cycle. -/
-abbrev BuildCycleT := CycleT BuildKey
+/-- The monad of asynchronous Lake jobs. -/
+abbrev JobM := CoreBuildM
 
-/-- A recursive build of a Lake build store that may encounter a cycle. -/
-abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
+/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
+abbrev SpawnM := BuildT BaseIO
 
-instance [Pure m] : MonadLift LakeM (BuildT m) where
-  monadLift x := fun ctx => pure <| x.run ctx.toContext
-
-@[inline] def BuildM.run (ctx : BuildContext) (self : BuildM α) : LogIO α :=
-  self ctx
-
-def BuildM.catchFailure (f : Unit → BaseIO α) (self : BuildM α) : SchedulerM α :=
-  fun ctx logMethods => self ctx logMethods |>.catchFailure f
-
-def logStep (message : String) : BuildM Unit := do
-  let done ← (← read).finishedBuilds.get
-  let started ← (← read).startedBuilds.get
-  logInfo s!"[{done}/{started}] {message}"
-
-def createParentDirs (path : FilePath) : IO Unit := do
-  if let some dir := path.parent then IO.FS.createDirAll dir
+/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
+@[deprecated SpawnM] abbrev SchedulerM := SpawnM

src/lake/Lake/Build/Common.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Monad
+import Lake.Config.Monad
 import Lake.Build.Actions
 
 /-! # Common Build Tools
@@ -11,7 +11,8 @@ This file defines general utilities that abstract common
 build functionality and provides some common concrete build functions.
 -/
 
-open System
+open System Lean
+
 namespace Lake
 
 /-! ## General Utilities -/
@@ -24,8 +25,10 @@ and will be rebuilt on different host platforms.
 def platformTrace := pureHash System.Platform.target
 
 /-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
-@[specialize] def BuildTrace.checkUpToDate [CheckExists ι] [GetMTime ι]
-(info : ι) (depTrace : BuildTrace) (traceFile : FilePath) : JobM Bool := do
+@[specialize] def BuildTrace.checkUpToDate
+  [CheckExists ι] [GetMTime ι]
+  (info : ι) (depTrace : BuildTrace) (traceFile : FilePath)
+: JobM Bool := do
   if (← getIsOldMode) then
     depTrace.checkAgainstTime info
   else
@@ -36,13 +39,15 @@ Build `info` unless it already exists and `depTrace` matches that
 of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 Returns whether `info` was already up-to-date.
 -/
-@[inline] def buildUnlessUpToDate' [CheckExists ι] [GetMTime ι] (info : ι)
-(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM Bool := do
+@[inline] def buildUnlessUpToDate?
+  [CheckExists ι] [GetMTime ι] (info : ι)
+  (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+: JobM Bool := do
   if (← depTrace.checkUpToDate info traceFile) then
     return true
+  else if (← getNoBuild) then
+    IO.Process.exit noBuildCode.toUInt8
   else
-    if (← getNoBuild) then
-      IO.Process.exit noBuildCode.toUInt8
     build
     depTrace.writeToFile traceFile
     return false
@@ -51,12 +56,14 @@ Returns whether `info` was already up-to-date.
 Build `info` unless it already exists and `depTrace` matches that
 of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 -/
-@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
-(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
-  discard <| buildUnlessUpToDate' info depTrace traceFile build
+@[inline] def buildUnlessUpToDate
+  [CheckExists ι] [GetMTime ι] (info : ι)
+  (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+: JobM PUnit := do
+  discard <| buildUnlessUpToDate? info depTrace traceFile build
 
 /-- Fetch the trace of a file that may have its hash already cached in a `.hash` file. -/
-def fetchFileTrace (file : FilePath) : BuildM BuildTrace := do
+def fetchFileTrace (file : FilePath) : JobM BuildTrace := do
   if (← getTrustHash) then
     let hashFile := FilePath.mk <| file.toString ++ ".hash"
     if let some hash ← Hash.load? hashFile then
@@ -76,24 +83,48 @@ def cacheFileHash (file : FilePath) : IO Hash := do
   return hash
 
 /--
-Build `file` using `build` unless it already exists and `depTrace` matches
+Replays the JSON log in `logFile` (if it exists).
+If the log file is malformed, logs a warning.
+-/
+def replayBuildLog (logFile : FilePath) : LogIO PUnit := do
+  match (← IO.FS.readFile logFile |>.toBaseIO) with
+  | .ok contents =>
+    match Json.parse contents >>= fromJson? with
+    | .ok entries => Log.mk entries |>.replay
+    | .error e => logWarning s!"cached build log is corrupted: {e}"
+  | .error (.noFileOrDirectory ..) => pure ()
+  | .error e => logWarning s!"failed to read cached build log: {e}"
+
+/-- Saves the log produce by `build` as JSON to `logFile`. -/
+def cacheBuildLog (logFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
+  let iniSz ← getLogSize
+  build
+  let log ← getLog
+  let log := log.entries.extract iniSz log.entries.size
+  unless log.isEmpty do
+    IO.FS.writeFile logFile (toJson log).pretty
+
+/--
+Builds `file` using `build` unless it already exists and `depTrace` matches
 the trace stored in the `.trace` file. If built, save the new `depTrace` and
 cache `file`'s hash in a `.hash` file. Otherwise, try to fetch the hash from
-the `.hash` file using `fetchFileTrace`.
+the `.hash` file using `fetchFileTrace`. Build logs (if any) are saved to
+a `.log.json` file and replayed from there if the build is skipped.
 
-By example, for `file := "foo.c"`, compare `depTrace` with that in `foo.c.trace`
-and cache the hash using `foo.c.hash`.
+For example, given `file := "foo.c"`, compares `depTrace` with that in
+`foo.c.trace` with the hash cache in `foo.c.hash` and the log cache in
+`foo.c.log.json`.
 -/
-def buildFileUnlessUpToDate (file : FilePath)
-(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
+def buildFileUnlessUpToDate (
+  file : FilePath) (depTrace : BuildTrace) (build : JobM PUnit)
+: JobM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
-  if (← depTrace.checkUpToDate file traceFile) then
+  let logFile := FilePath.mk <| file.toString ++ ".log.json"
+  let build := cacheBuildLog logFile build
+  if (← buildUnlessUpToDate? file depTrace traceFile build) then
+    replayBuildLog logFile
     fetchFileTrace file
   else
-    if (← getNoBuild) then
-      IO.Process.exit noBuildCode.toUInt8
-    build
-    depTrace.writeToFile traceFile
     return .mk (← cacheFileHash file) (← getMTime file)
 
 /--
@@ -101,8 +132,9 @@ Build `file` using `build` after `dep` completes if the dependency's
 trace (and/or `extraDepTrace`) has changed.
 -/
 @[inline] def buildFileAfterDep
-(file : FilePath) (dep : BuildJob α) (build : α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
+  (file : FilePath) (dep : BuildJob α) (build : α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) :=
   dep.bindSync fun depInfo depTrace => do
     let depTrace := depTrace.mix (← extraDepTrace)
     let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo
@@ -110,20 +142,22 @@ trace (and/or `extraDepTrace`) has changed.
 
 /-- Build `file` using `build` after `deps` have built if any of their traces change. -/
 @[inline] def buildFileAfterDepList
-(file : FilePath) (deps : List (BuildJob α)) (build : List α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  (file : FilePath) (deps : List (BuildJob α)) (build : List α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) := do
   buildFileAfterDep file (← BuildJob.collectList deps) build extraDepTrace
 
 /-- Build `file` using `build` after `deps` have built if any of their traces change. -/
 @[inline] def buildFileAfterDepArray
-(file : FilePath) (deps : Array (BuildJob α)) (build : Array α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  (file : FilePath) (deps : Array (BuildJob α)) (build : Array α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) := do
   buildFileAfterDep file (← BuildJob.collectArray deps) build extraDepTrace
 
 /-! ## Common Builds -/
 
 /-- A build job for file that is expected to already exist (e.g., a source file). -/
-def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
+def inputFile (path : FilePath) : SpawnM (BuildJob FilePath) :=
   Job.async <| (path, ·) <$> computeTrace path
 
 /--
@@ -141,54 +175,58 @@ be `weakArgs` to avoid build artifact incompatibility between systems
 You can add more components to the trace via `extraDepTrace`,
 which will be computed in the resulting `BuildJob` before building.
 -/
-@[inline] def buildO (name : String)
-(oFile : FilePath) (srcJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) (compiler : FilePath := "cc")
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
+@[inline] def buildO
+  (oFile : FilePath) (srcJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[]) (compiler : FilePath := "cc")
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← extraDepTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-    compileO name oFile srcFile (weakArgs ++ traceArgs) compiler
+    compileO oFile srcFile (weakArgs ++ traceArgs) compiler
 
 /-- Build an object file from a source fie job (i.e, a `lean -c` output) using `leanc`. -/
-@[inline] def buildLeanO (name : String)
-(oFile : FilePath) (srcJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+@[inline] def buildLeanO
+  (oFile : FilePath) (srcJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-     compileO name oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
+     compileO oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build a static library from object file jobs using the `ar` packaged with Lean. -/
-def buildStaticLib (libFile : FilePath)
-(oFileJobs : Array (BuildJob FilePath)) : SchedulerM (BuildJob FilePath) :=
-  let name := libFile.fileName.getD libFile.toString
+def buildStaticLib
+  (libFile : FilePath) (oFileJobs : Array (BuildJob FilePath))
+: SpawnM (BuildJob FilePath) :=
   buildFileAfterDepArray libFile oFileJobs fun oFiles => do
-    compileStaticLib name libFile oFiles (← getLeanAr)
+    compileStaticLib libFile oFiles (← getLeanAr)
 
 /-- Build a shared library by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanSharedLib
-(libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
-  let name := libFile.fileName.getD libFile.toString
+  (libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray libFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileSharedLib name libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
+    compileSharedLib libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build an executable by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanExe
-(exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
-  let name := exeFile.fileName.getD exeFile.toString
+  (exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray exeFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileExe name exeFile links (weakArgs ++ traceArgs) (← getLeanc)
+    compileExe exeFile links (weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build a shared library from a static library using `leanc`. -/
-def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+def buildLeanSharedLibOfStatic
+  (staticLibJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   staticLibJob.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let baseArgs :=
@@ -200,13 +238,11 @@ def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
       (← getLeanTrace).mix <| (pureHash traceArgs).mix <| platformTrace
     let args := baseArgs ++ weakArgs ++ traceArgs
     let trace ← buildFileUnlessUpToDate dynlib depTrace do
-      let name := dynlib.fileName.getD dynlib.toString
-      compileSharedLib name dynlib args (← getLeanc)
+      compileSharedLib dynlib args (← getLeanc)
     return (dynlib, trace)
 
 /-- Construct a `Dynlib` object for a shared library target. -/
-def computeDynlibOfShared
-(sharedLibTarget : BuildJob FilePath) : SchedulerM (BuildJob Dynlib) :=
+def computeDynlibOfShared (sharedLibTarget : BuildJob FilePath) : SpawnM (BuildJob Dynlib) :=
   sharedLibTarget.bindSync fun sharedLib trace => do
     if let some stem := sharedLib.fileStem then
       if Platform.isWindows then

src/lake/Lake/Build/Data.lean

@@ -83,10 +83,11 @@ abbrev BuildData : BuildKey → Type
 | .targetFacet _ _ f => TargetData f
 | .customTarget p t => CustomData (p, t)
 
+instance (priority := low) : FamilyDef BuildData k (BuildData k) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
-instance (priority := low)  : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/

src/lake/Lake/Build/Executable.lean

@@ -11,8 +11,8 @@ namespace Lake
 The build function definition for a Lean executable.
 -/
 
-protected def LeanExe.recBuildExe
-(self : LeanExe) : IndexBuildM (BuildJob FilePath) := do
+def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Linking {self.fileName}" do
   let imports ← self.root.transImports.fetch
   let mut linkJobs := #[← self.root.o.fetch]
   for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do

src/lake/Lake/Build/Fetch.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Error
+import Lake.Util.Cycle
+import Lake.Util.EquipT
+import Lake.Build.Info
+import Lake.Build.Store
+
+/-! # Recursive Building
+
+This module defines Lake's top-level build monad, `FetchM`, used
+for performing recursive builds. A recursive build is a build function
+which can fetch the results of other (recursive) builds. This is done
+using the `fetch` function defined in this module.
+-/
+
+namespace Lake
+
+/-- A recursive build of a Lake build store that may encounter a cycle. -/
+abbrev RecBuildM := CallStackT BuildKey <| StateT BuildStore <| CoreBuildM
+
+/-- Run a recursive build. -/
+@[inline] def RecBuildM.run
+  (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
+: CoreBuildM (α × BuildStore) := do
+  build stack store
+
+/-- Run a recursive build in a fresh build store. -/
+@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
+  (·.1) <$> build.run {} {}
+
+/-- Log build cycle and error. -/
+@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
+  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
+
+instance : MonadCycleOf BuildKey RecBuildM where
+  throwCycle := buildCycleError
+
+/-- A build function for any element of the Lake build index. -/
+abbrev IndexBuildFn (m : Type → Type v) :=
+  -- `DFetchFn BuildInfo (BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (BuildData info.key)
+
+/-- A transformer to equip a monad with a build function for the Lake index. -/
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
+
+/-- The top-level monad for Lake build functions. -/
+abbrev FetchM := IndexT RecBuildM
+
+/-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
+@[deprecated FetchM] abbrev IndexBuildM := FetchM
+
+/-- The old build monad. **Uses should generally be replaced by `FetchM`.** -/
+@[deprecated FetchM] abbrev BuildM := CoreBuildM
+
+/-- Fetch the result associated with the info using the Lake build index. -/
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α :=
+  fun build => cast (by simp) <| build self
+
+export BuildInfo (fetch)

src/lake/Lake/Build/Imports.lean

@@ -18,7 +18,7 @@ the build jobs of their precompiled modules and the build jobs of said modules'
 external libraries.
 -/
 def recBuildImports (imports : Array Module)
-: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
+: FetchM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
   let mut modJobs := #[]
   let mut precompileImports := OrdModuleSet.empty
   for mod in imports do
@@ -37,18 +37,23 @@ Builds an `Array` of module imports. Used by `lake setup-file` to build modules
 for the Lean server and by `lake lean` to build the imports of a file.
 Returns the set of module dynlibs built (so they can be loaded by Lean).
 -/
-def buildImportsAndDeps (imports : Array Module) : BuildM (Array FilePath) := do
-  let ws ← getWorkspace
+def buildImportsAndDeps (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
-    ws.root.extraDep.build >>= (·.materialize)
-    return #[]
+    (← getRootPackage).extraDep.fetch <&> (·.map fun _ => #[])
   else
     -- build local imports from list
     let (modJobs, precompileJobs, externLibJobs) ←
-      recBuildImports imports |>.run.run
-    modJobs.forM (·.await)
-    let modLibs ← precompileJobs.mapM (·.await <&> (·.path))
-    let externLibs ← externLibJobs.mapM (·.await <&> (·.path))
-    -- NOTE: Lean wants the external library symbols before module symbols
-    return externLibs ++ modLibs
+      recBuildImports imports
+    let modJob ← BuildJob.mixArray modJobs
+    let precompileJob ← BuildJob.collectArray precompileJobs
+    let externLibJob ← BuildJob.collectArray externLibJobs
+    let job ←
+      modJob.bindAsync fun _ modTrace =>
+      precompileJob.bindAsync fun modLibs modLibTrace =>
+      externLibJob.bindSync fun externLibs externTrace => do
+        -- NOTE: Lean wants the external library symbols before module symbols
+        let libs := (externLibs ++ modLibs).map (·.path)
+        let trace := modTrace.mix modLibTrace |>.mix externTrace
+        return (libs, trace)
+    return job

src/lake/Lake/Build/Index.lean

@@ -3,7 +3,6 @@ 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.Targets
 import Lake.Build.Executable
 import Lake.Build.Topological
 
@@ -20,20 +19,25 @@ open Lean
 namespace Lake
 
 /--
-Converts a conveniently typed target facet build function into its
-dynamically typed equivalent.
+Converts a conveniently-typed target facet build function into its
+dynamically-typed equivalent.
 -/
-@[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
-[h : FamilyOut TargetData facet α] : IndexBuildM (TargetData facet) :=
+@[macro_inline] def mkTargetFacetBuild
+  (facet : Name) (build : FetchM (BuildJob α))
+  [h : FamilyOut TargetData facet (BuildJob α)]
+: FetchM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
-def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Building {lib.staticTargetName.toString}" do
   lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
 
-def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+def ExternLib.recBuildShared (lib : ExternLib) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Linking {lib.staticTargetName.toString}" do
   buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
 
-def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib) := do
+def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (BuildJob Dynlib) := do
+  withRegisterJob s!"Computing {lib.staticTargetName.toString} dynlib" do
   computeDynlibOfShared (← lib.shared.fetch)
 
 /-!
@@ -41,7 +45,7 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib)
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
+def recBuildWithIndex : (info : BuildInfo) → FetchM (BuildData info.key)
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
     config.build mod
@@ -72,41 +76,8 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
   mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
 
 /--
-Run the given recursive build using the Lake build index
+Run a recursive Lake build using the Lake build index
 and a topological / suspending scheduler.
 -/
-def IndexBuildM.run (build : IndexBuildM α) : RecBuildM α :=
-  build <| recFetchMemoize BuildInfo.key recBuildWithIndex
-
-/--
-Recursively build the given info using the Lake build index
-and a topological / suspending scheduler.
--/
-def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
-  recFetchMemoize BuildInfo.key recBuildWithIndex info
-
-/--
-Recursively build the given info using the Lake build index
-and a topological / suspending scheduler and return the dynamic result.
--/
-@[macro_inline] def buildIndexTop (info : BuildInfo)
-[FamilyOut BuildData info.key α] : RecBuildM α := do
-  cast (by simp) <| buildIndexTop' info
-
-/-- Build the given Lake target in a fresh build store. -/
-@[inline] def BuildInfo.build
-(self : BuildInfo) [FamilyOut BuildData self.key α] : BuildM α :=
-  buildIndexTop self |>.run
-
-export BuildInfo (build)
-
-/-! ### Lean Executable Builds -/
-
-@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
-  self.exe.build
-
-@[inline] protected def LeanExeConfig.build (self : LeanExeConfig) : BuildM (BuildJob FilePath) := do
-  (← self.get).build
-
-@[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
-  self.exe.fetch
+def FetchM.run (x : FetchM α) : RecBuildM α :=
+  x (inline <| recFetchMemoize BuildInfo.key recBuildWithIndex)

src/lake/Lake/Build/Info.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets
-import Lake.Util.EquipT
 
 /-!
 # Build Info
@@ -62,7 +61,7 @@ abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey :=
 /-! ### Build Info to Key -/
 
 /-- The key that identifies the build in the Lake build store. -/
-abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
+@[reducible] def BuildInfo.key : (self : BuildInfo) → BuildKey
 | moduleFacet m f => m.facetBuildKey f
 | packageFacet p f => p.facetBuildKey f
 | libraryFacet l f => l.facetBuildKey f
@@ -109,27 +108,6 @@ instance [FamilyOut TargetData ExternLib.dynlibFacet α]
 : FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
 
---------------------------------------------------------------------------------
-/-! ## Recursive Building                                                     -/
---------------------------------------------------------------------------------
-
-/-- A build function for any element of the Lake build index. -/
-abbrev IndexBuildFn (m : Type → Type v) :=
-  -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
-  (info : BuildInfo) → m (BuildData info.key)
-
-/-- A transformer to equip a monad with a build function for the Lake index. -/
-abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
-
-/-- The monad for build functions that are part of the index. -/
-abbrev IndexBuildM := IndexT RecBuildM
-
-/-- Fetch the result associated with the info using the Lake build index. -/
-@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : IndexBuildM α :=
-  fun build => cast (by simp) <| build self
-
-export BuildInfo (fetch)
-
 --------------------------------------------------------------------------------
 /-! ## Build Info & Facets                                                    -/
 --------------------------------------------------------------------------------

src/lake/Lake/Build/Job.lean

@@ -3,49 +3,139 @@ 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.Util.Async
 import Lake.Build.Trace
-import Lake.Build.Context
+import Lake.Build.Basic
 
 open System
+
 namespace Lake
 
-/-- A Lake job. -/
-abbrev Job α := OptionIOTask α
-
-/-- The monad of Lake jobs. -/
-abbrev JobM := BuildM
-
-/-- The monad of a finished Lake job. -/
-abbrev ResultM := OptionIO
-
 namespace Job
 
-@[inline] def attempt (self : Job α) : Job Bool := do
-  Option.isSome <$> self.run
+@[inline] protected def pure (a : α) : Job α :=
+  {task := Task.pure (.ok a {})}
 
-@[inline] def attempt? (self : Job α) : Job (Option α) := do
-  some <$> self.run
+instance : Pure Job := ⟨Job.pure⟩
+instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
 
-@[inline] def nil : Job Unit :=
- pure ()
+@[inline] protected def nop : Job Unit :=
+  pure ()
 
-@[inline] protected def async (act : JobM α) : SchedulerM (Job α) :=
-  async act
+@[inline] protected def error (l : Log) : Job α :=
+  {task := Task.pure (.error 0 l)}
 
-@[inline] protected def await (self : Job α) : ResultM α :=
-  await self
+@[inline] def mapResult
+  (f : JobResult α → JobResult β) (self : Job α)
+  (prio := Task.Priority.default) (sync := false)
+: Job β :=
+  {task := self.task.map f prio sync}
 
+@[inline] protected def map
+  (f : α → β) (self : Job α)
+  (prio := Task.Priority.default) (sync := false)
+: Job β :=
+  self.mapResult (·.map f) prio sync
+
+instance : Functor Job where map := Job.map
+
+@[inline] def clearLog (self : Job α) : Job α :=
+  self.mapResult (sync := true) fun
+  | .ok a _ => .ok a {}
+  | .error .. => .error 0 {}
+
+@[inline] def attempt (self : Job α) : Job Bool :=
+  self.mapResult (sync := true) fun
+  | .error n l => .ok false (l.shrink n)
+  | .ok _ l => .ok true l
+
+@[inline] def attempt? (self : Job α) : Job (Option α) :=
+  self.mapResult (sync := true) fun
+  | .error n l => .ok none (l.shrink n)
+  | .ok a l => .ok (some a) l
+
+/-- Spawn a job that asynchronously performs `act`. -/
+@[inline] protected def async
+  (act : JobM α) (prio := Task.Priority.default)
+: SpawnM (Job α) := fun ctx => Job.mk <$> do
+  BaseIO.asTask (act ctx {}) prio
+
+/-- Wait a the job to complete and return the result. -/
+@[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
+  IO.wait self.task
+
+/--
+Wait for a job to complete and return the produced value.
+If an error occurred, return `none` and discarded any logs produced.
+-/
+@[inline] protected def wait? (self : Job α) : BaseIO (Option α) := do
+  return (← self.wait).result?
+
+/--
+Wait for a job to complete and return the produced value.
+Logs the job's log and throws if there was an error.
+-/
+@[inline] protected def await (self : Job α) : LogIO α := do
+  match (← self.wait) with
+  | .error n l => l.replay; throw n
+  | .ok a l => l.replay; pure a
+
+/--
+`let c ← a.bindSync b` asynchronously performs the action `b`
+after the job `a` completes.
+-/
 @[inline] protected def bindSync
-(self : Job α) (f : α → JobM β) (prio := Task.Priority.default) : SchedulerM (Job β) :=
-  bindSync prio self f
+  (self : Job α) (f : α → JobM β)
+  (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) := fun ctx => Job.mk <$> do
+  BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun r=>
+    match r with
+    | EResult.ok a l => f a ctx l
+    | EResult.error n l => return .error n l
 
+/--
+`let c ← a.bindAsync b` asynchronously performs the action `b`
+after the job `a` completes and then merges into the job produced by `b`.
+-/
 @[inline] protected def bindAsync
-(self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β)  :=
-  bindAsync self f
+  (self : Job α) (f : α → SpawnM (Job β))
+  (prio := Task.Priority.default) (sync := false)
+: SpawnM (Job β) := fun ctx => Job.mk <$> do
+  BaseIO.bindTask self.task (prio := prio) (sync := sync) fun
+    | .ok a l => do
+      let job ← f a ctx
+      if l.isEmpty then return job.task else
+      return job.task.map (prio := prio) (sync := true) fun
+      | EResult.ok a l' => .ok a (l ++ l')
+      | EResult.error n l' => .error (l.size + n) (l ++ l')
+    | .error n l => return Task.pure (.error n l)
+
+/--
+`a.zipWith f b` produces a new job `c` that applies `f` to the
+results of `a` and `b`. The job `c` errors if either `a` or `b` error.
+-/
+@[inline] def zipWith
+  (f : α → β → γ) (x : Job α) (y : Job β)
+  (prio := Task.Priority.default) (sync := false)
+: BaseIO (Job γ) := Job.mk <$> do
+  BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx =>
+  BaseIO.bindTask y.task (prio := prio) (sync := sync) fun ry =>
+  match rx, ry with
+  | .ok a la, .ok b lb => return Task.pure (EResult.ok (f a b) (la ++ lb))
+  | rx, ry => return Task.pure (EResult.error 0 (rx.state ++ ry.state))
 
 end Job
 
+/-- Register the produced job for the CLI progress UI.  -/
+@[inline] def withRegisterJob
+  [Monad m] [MonadReaderOf BuildContext m] [MonadLiftT BaseIO m]
+  (caption : String) (x : m (Job α))
+: m (Job α) := do
+  let job ← x
+  let ctx ← read
+  liftM (m := BaseIO) do
+  ctx.registeredJobs.modify (·.push (caption, discard job))
+  return job.clearLog
+
 /-- A Lake build job. -/
 abbrev BuildJob α := Job (α × BuildTrace)
 
@@ -69,14 +159,14 @@ namespace BuildJob
 instance : Pure BuildJob := ⟨BuildJob.pure⟩
 
 @[inline] def attempt (self : BuildJob α) : BuildJob Bool :=
-  mk <| self.toJob.map fun
-    | none => some (false, nilTrace)
-    | some (_, t) => some (true, t)
+  {task := self.toJob.task.map fun
+    | .error _ l => .ok (false, nilTrace) l
+    | .ok (_, t) l => .ok (true, t) l}
 
 @[inline] def attempt? (self : BuildJob α) : BuildJob (Option α) :=
-  mk <| self.toJob.map fun
-    | none => some (none, nilTrace)
-    | some (a, t) => some (some a, t)
+  {task := self.toJob.task.map fun
+    | .error _ l => .ok (none, nilTrace) l
+    | .ok (a, t) l => .ok (some a, t) l}
 
 @[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
   mk <| (fun (a,t) => (f a,t)) <$> self.toJob
@@ -88,44 +178,39 @@ instance : Functor BuildJob where
   mk <| (fun (a,t) => f a t) <$> self.toJob
 
 @[inline] protected def bindSync
-(self : BuildJob α) (f : α → BuildTrace → JobM β)
-(prio : Task.Priority := .default) : SchedulerM (Job β) :=
-  self.toJob.bindSync (prio := prio) fun (a, t) => f a t
+  (self : BuildJob α) (f : α → BuildTrace → JobM β)
+  (prio : Task.Priority := .default) (sync := false)
+: SpawnM (Job β) :=
+  self.toJob.bindSync (prio := prio) (sync := sync) fun (a, t) => f a t
 
 @[inline] protected def bindAsync
-(self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β)  :=
-  self.toJob.bindAsync fun (a, t) => f a t
+  (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
+  (prio : Task.Priority := .default) (sync := false)
+ : SpawnM (Job β)  :=
+  self.toJob.bindAsync (prio := prio) (sync := sync) fun (a, t) => f a t
 
-@[inline] protected def await (self : BuildJob α) : ResultM α :=
-  (·.1) <$> await self.toJob
-
-instance : Await BuildJob ResultM := ⟨BuildJob.await⟩
-
-@[inline] def materialize (self : BuildJob α) : ResultM Unit :=
-  discard <| await self.toJob
+@[inline] protected def wait? (self : BuildJob α) : BaseIO (Option α) :=
+  (·.map (·.1)) <$> self.toJob.wait?
 
 def add (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob α) :=
-  mk <$> seqLeftAsync t1.toJob t2.toJob
+  mk <$> t1.toJob.zipWith (fun a _ => a) t2.toJob
 
 def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
-  mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob
+  mk <$> t1.toJob.zipWith (fun (_,t) (_,t') => ((), mixTrace t t')) t2.toJob
 
 def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
-  jobs.foldrM (init := pure nilTrace) fun j a =>
-    seqWithAsync (fun (_,t') t => mixTrace t t') j.toJob a
+  jobs.foldrM (·.toJob.zipWith (fun (_,t') t => mixTrace t t') ·) (pure nilTrace)
 
 def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
-  jobs.foldlM (init := pure nilTrace) fun a j =>
-    seqWithAsync (fun t (_,t') => mixTrace t t') a j.toJob
+  jobs.foldlM (·.zipWith (fun t (_,t') => mixTrace t t') ·.toJob) (pure nilTrace)
 
-protected def seqWithAsync
-(f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob γ) :=
-  mk <$> seqWithAsync (fun (a,t) (b,t') => (f a b, mixTrace t t')) t1.toJob t2.toJob
-
-instance : SeqWithAsync BaseIO BuildJob := ⟨BuildJob.seqWithAsync⟩
+protected def zipWith
+  (f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β)
+: BaseIO (BuildJob γ) :=
+  mk <$> t1.toJob.zipWith (fun (a,t) (b,t') => (f a b, mixTrace t t'))  t2.toJob
 
 def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) :=
-  jobs.foldrM (seqWithAsync List.cons) (pure [])
+  jobs.foldrM (BuildJob.zipWith List.cons) (pure [])
 
 def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) :=
-  jobs.foldlM (seqWithAsync Array.push) (pure #[])
+  jobs.foldlM (BuildJob.zipWith Array.push) (pure #[])

src/lake/Lake/Build/Library.lean

@@ -18,7 +18,7 @@ namespace Lake
 Collect the local modules of a library.
 That is, the modules from `getModuleArray` plus their local transitive imports.
 -/
-partial def LeanLib.recCollectLocalModules (self : LeanLib) : IndexBuildM (Array Module) := do
+partial def LeanLib.recCollectLocalModules (self : LeanLib) : FetchM (Array Module) := do
   let mut mods := #[]
   let mut modSet := ModuleSet.empty
   for mod in (← self.getModuleArray) do
@@ -42,17 +42,19 @@ def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=
   mkFacetConfig LeanLib.recCollectLocalModules
 
 protected def LeanLib.recBuildLean
-(self : LeanLib) : IndexBuildM (BuildJob Unit) := do
+(self : LeanLib) : FetchM (BuildJob Unit) := do
   let mods ← self.modules.fetch
   mods.foldlM (init := BuildJob.nil) fun job mod => do
     job.mix <| ← mod.leanArts.fetch
 
 /-- The `LibraryFacetConfig` for the builtin `leanArtsFacet`. -/
 def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
-  mkFacetJobConfigSmall LeanLib.recBuildLean
+  mkFacetJobConfig LeanLib.recBuildLean
 
 @[specialize] protected def LeanLib.recBuildStatic
-(self : LeanLib) (shouldExport : Bool) : IndexBuildM (BuildJob FilePath) := do
+(self : LeanLib) (shouldExport : Bool) : FetchM (BuildJob FilePath) := do
+  let exports := if shouldExport then "w/ exports" else "w/o exports"
+  withRegisterJob s!"Building {self.staticLibFileName} ({exports})" do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
@@ -71,7 +73,8 @@ def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet :=
 /-! ## Build Shared Lib -/
 
 protected def LeanLib.recBuildShared
-(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
+(self : LeanLib) : FetchM (BuildJob FilePath) := do
+  withRegisterJob s!"Linking {self.sharedLibFileName}" do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
     mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
@@ -86,13 +89,13 @@ def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
 /-! ## Build `extraDepTargets` -/
 
 /-- Build the `extraDepTargets` for the library and its package. -/
-def LeanLib.recBuildExtraDepTargets (self : LeanLib) : IndexBuildM (BuildJob Unit) := do
+def LeanLib.recBuildExtraDepTargets (self : LeanLib) : FetchM (BuildJob Unit) := do
   self.extraDepTargets.foldlM (init := ← self.pkg.extraDep.fetch) fun job target => do
     job.mix <| ← self.pkg.fetchTargetJob target
 
 /-- The `LibraryFacetConfig` for the builtin `extraDepFacet`. -/
 def LeanLib.extraDepFacetConfig : LibraryFacetConfig extraDepFacet :=
-  mkFacetJobConfigSmall LeanLib.recBuildExtraDepTargets
+  mkFacetJobConfig LeanLib.recBuildExtraDepTargets
 
 open LeanLib in
 /--

src/lake/Lake/Build/Module.lean

@@ -18,7 +18,7 @@ namespace Lake
 
 /-- Compute library directories and build external library Jobs of the given packages. -/
 def recBuildExternDynlibs (pkgs : Array Package)
-: IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do
+: FetchM (Array (BuildJob Dynlib) × Array FilePath) := do
   let mut libDirs := #[]
   let mut jobs : Array (BuildJob Dynlib) := #[]
   for pkg in pkgs do
@@ -31,7 +31,7 @@ Build the dynlibs of the transitive imports that want precompilation
 and the dynlibs of *their* imports.
 -/
 partial def recBuildPrecompileDynlibs (imports : Array Module)
-: IndexBuildM (Array (BuildJob Dynlib) × Array (BuildJob Dynlib) × Array FilePath) := do
+: FetchM (Array (BuildJob Dynlib) × Array (BuildJob Dynlib) × Array FilePath) := do
   let (pkgs, _, jobs) ←
     go imports OrdPackageSet.empty ModuleSet.empty #[] false
   return (jobs, ← recBuildExternDynlibs pkgs.toArray)
@@ -52,14 +52,12 @@ where
       (pkgs, modSet, jobs) ← go recImports pkgs modSet jobs shouldPrecompile
     return (pkgs, modSet, jobs)
 
-variable [MonadLiftT BuildM m]
-
 /--
 Recursively parse the Lean files of a module and its imports
 building an `Array` product of its direct local imports.
 -/
-def Module.recParseImports (mod : Module) : IndexBuildM (Array Module) := do
-  let callstack : CallStack BuildKey ← EquipT.lift <| CycleT.readCallStack
+def Module.recParseImports (mod : Module) : FetchM (Array Module) := do
+  let callstack ← getCallStack
   let contents ← liftM <| tryCatch (IO.FS.readFile mod.leanFile) fun err =>
     -- filter out only modules from build key, and remove adjacent duplicates (squeeze),
     -- since Lake visits multiple nested facets of the same module.
@@ -80,7 +78,7 @@ def Module.importsFacetConfig : ModuleFacetConfig importsFacet :=
   mkFacetConfig (·.recParseImports)
 
 /-- Recursively compute a module's transitive imports. -/
-def Module.recComputeTransImports (mod : Module) : IndexBuildM (Array Module) := do
+def Module.recComputeTransImports (mod : Module) : FetchM (Array Module) := do
   (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
     return set.appendArray (← imp.transImports.fetch) |>.insert imp
 
@@ -89,7 +87,7 @@ def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet :=
   mkFacetConfig (·.recComputeTransImports)
 
 /-- Recursively compute a module's precompiled imports. -/
-def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Module) := do
+def Module.recComputePrecompileImports (mod : Module) : FetchM (Array Module) := do
   (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
     if imp.shouldPrecompile then
       return set.appendArray (← imp.transImports.fetch) |>.insert imp
@@ -106,7 +104,7 @@ Recursively build a module's dependencies, including:
 * Shared libraries (e.g., `extern_lib` targets or precompiled modules)
 * `extraDepTargets` of its library
 -/
-def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Array FilePath)) := do
+def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := do
   let imports ← mod.imports.fetch
   let extraDepJob ← mod.lib.extraDep.fetch
   let precompileImports ← mod.precompileImports.fetch
@@ -142,28 +140,32 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
 
 /-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/
 def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
-  mkFacetJobConfigSmall (·.recBuildDeps)
+  mkFacetJobConfig (·.recBuildDeps)
 
 /--
 Recursively build a Lean module.
 Fetch its dependencies and then elaborate the Lean source file, producing
 all possible artifacts (i.e., `.olean`, `ilean`, `.c`, and `.bc`).
 -/
-def Module.recBuildLean (mod : Module) : IndexBuildM (BuildJob Unit) := do
+def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
+  withRegisterJob s!"Building {mod.name}" do
   (← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
     let argTrace : BuildTrace := pureHash mod.leanArgs
     let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
     let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-    buildUnlessUpToDate mod modTrace mod.traceFile do
+    let upToDate ← buildUnlessUpToDate? mod modTrace mod.traceFile do
       let hasLLVM := Lean.Internal.hasLLVMBackend ()
       let bcFile? := if hasLLVM then some mod.bcFile else none
-      compileLeanModule mod.name.toString mod.leanFile mod.oleanFile mod.ileanFile mod.cFile bcFile?
-        (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.weakLeanArgs ++ mod.leanArgs) (← getLean)
+      cacheBuildLog mod.logFile do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile bcFile?
+          (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.weakLeanArgs ++ mod.leanArgs) (← getLean)
       discard <| cacheFileHash mod.oleanFile
       discard <| cacheFileHash mod.ileanFile
       discard <| cacheFileHash mod.cFile
       if hasLLVM then
         discard <| cacheFileHash mod.bcFile
+    if upToDate then
+      replayBuildLog mod.logFile
     return ((), depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
@@ -172,26 +174,26 @@ def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
 
 /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
 def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
-  mkFacetJobConfigSmall fun mod => do
+  mkFacetJobConfig fun mod => do
     (← mod.leanArts.fetch).bindSync fun _ depTrace =>
       return (mod.oleanFile, mixTrace (← fetchFileTrace mod.oleanFile) depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
 def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
-  mkFacetJobConfigSmall fun mod => do
+  mkFacetJobConfig fun mod => do
     (← mod.leanArts.fetch).bindSync fun _ depTrace =>
       return (mod.ileanFile, mixTrace (← fetchFileTrace mod.ileanFile) depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 def Module.cFacetConfig : ModuleFacetConfig cFacet :=
-  mkFacetJobConfigSmall fun mod => do
+  mkFacetJobConfig fun mod => do
     (← mod.leanArts.fetch).bindSync fun _ _ =>
       -- do content-aware hashing so that we avoid recompiling unchanged C files
       return (mod.cFile, ← fetchFileTrace mod.cFile)
 
 /-- The `ModuleFacetConfig` for the builtin `bcFacet`. -/
 def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
-  mkFacetJobConfigSmall fun mod => do
+  mkFacetJobConfig fun mod => do
     (← mod.leanArts.fetch).bindSync fun _ _ =>
       -- do content-aware hashing so that we avoid recompiling unchanged bitcode files
       return (mod.bcFile, ← fetchFileTrace mod.bcFile)
@@ -200,10 +202,11 @@ def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
 Recursively build the module's object file from its C file produced by `lean`
 with `-DLEAN_EXPORTING` set, which exports Lean symbols defined within the C files.
 -/
-def Module.recBuildLeanCToOExport (self : Module) : IndexBuildM (BuildJob FilePath) := do
+def Module.recBuildLeanCToOExport (self : Module) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Compiling {self.name}" do
   -- TODO: add option to pass a target triplet for cross compilation
   let leancArgs := self.leancArgs ++ #["-DLEAN_EXPORTING"]
-  buildLeanO self.name.toString self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
+  buildLeanO self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
 
 /-- The `ModuleFacetConfig` for the builtin `coExportFacet`. -/
 def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
@@ -213,9 +216,10 @@ def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
 Recursively build the module's object file from its C file produced by `lean`.
 This version does not export any Lean symbols.
 -/
-def Module.recBuildLeanCToONoExport (self : Module) : IndexBuildM (BuildJob FilePath) := do
+def Module.recBuildLeanCToONoExport (self : Module) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Compiling {self.name}" do
   -- TODO: add option to pass a target triplet for cross compilation
-  buildLeanO self.name.toString self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
+  buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
 
 /-- The `ModuleFacetConfig` for the builtin `coNoExportFacet`. -/
 def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=
@@ -223,13 +227,14 @@ def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=
 
 /-- The `ModuleFacetConfig` for the builtin `coFacet`. -/
 def Module.coFacetConfig : ModuleFacetConfig coFacet :=
-  mkFacetJobConfigSmall fun mod =>
+  mkFacetJobConfig fun mod =>
     if Platform.isWindows then mod.coNoExport.fetch else mod.coExport.fetch
 
 /-- Recursively build the module's object file from its bitcode file produced by `lean`. -/
-def Module.recBuildLeanBcToO (self : Module) : IndexBuildM (BuildJob FilePath) := do
+def Module.recBuildLeanBcToO (self : Module) : FetchM (BuildJob FilePath) := do
+  withRegisterJob s!"Compiling {self.name}" do
   -- TODO: add option to pass a target triplet for cross compilation
-  buildLeanO self.name.toString self.bcoFile (← self.bc.fetch) self.weakLeancArgs self.leancArgs
+  buildLeanO self.bcoFile (← self.bc.fetch) self.weakLeancArgs self.leancArgs
 
 /-- The `ModuleFacetConfig` for the builtin `bcoFacet`. -/
 def Module.bcoFacetConfig : ModuleFacetConfig bcoFacet :=
@@ -237,28 +242,29 @@ def Module.bcoFacetConfig : ModuleFacetConfig bcoFacet :=
 
 /-- The `ModuleFacetConfig` for the builtin `oExportFacet`. -/
 def Module.oExportFacetConfig : ModuleFacetConfig oExportFacet :=
-  mkFacetJobConfigSmall fun mod =>
+  mkFacetJobConfig fun mod =>
     match mod.backend with
     | .default | .c => mod.coExport.fetch
     | .llvm => mod.bco.fetch
 
 /-- The `ModuleFacetConfig` for the builtin `oNoExportFacet`. -/
 def Module.oNoExportFacetConfig : ModuleFacetConfig oNoExportFacet :=
-  mkFacetJobConfigSmall fun mod =>
+  mkFacetJobConfig fun mod =>
     match mod.backend with
     | .default | .c => mod.coNoExport.fetch
     | .llvm => error "the LLVM backend only supports exporting Lean symbols"
 
 /-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
 def Module.oFacetConfig : ModuleFacetConfig oFacet :=
-  mkFacetJobConfigSmall fun mod =>
+  mkFacetJobConfig fun mod =>
     match mod.backend with
     | .default | .c => mod.co.fetch
     | .llvm => mod.bco.fetch
 
 -- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`
 /-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/
-def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
+def Module.recBuildDynlib (mod : Module) : FetchM (BuildJob Dynlib) :=
+  withRegisterJob s!"Linking {mod.name} dynlib" do
 
   -- Compute dependencies
   let transImports ← mod.transImports.fetch
@@ -274,23 +280,22 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
   let externDynlibsJob ← BuildJob.collectArray externJobs
 
   -- Build dynlib
-  show SchedulerM _ from do
-    linksJob.bindAsync fun links linksTrace => do
-    modDynlibsJob.bindAsync fun modDynlibs modLibsTrace => do
-    externDynlibsJob.bindSync fun externDynlibs externLibsTrace => do
-      let libNames := modDynlibs.map (·.name) ++ externDynlibs.map (·.name)
-      let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?)
-      let depTrace :=
-        linksTrace.mix <| modLibsTrace.mix <| externLibsTrace.mix
-        <| (← getLeanTrace).mix <| (pureHash mod.linkArgs).mix <|
-        platformTrace
-      let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
-        let args :=
-          links.map toString ++
-          libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}") ++
-          mod.weakLinkArgs ++ mod.linkArgs
-        compileSharedLib mod.name.toString mod.dynlibFile args (← getLeanc)
-      return (⟨mod.dynlibFile, mod.dynlibName⟩, trace)
+  linksJob.bindAsync fun links linksTrace => do
+  modDynlibsJob.bindAsync fun modDynlibs modLibsTrace => do
+  externDynlibsJob.bindSync fun externDynlibs externLibsTrace => do
+    let libNames := modDynlibs.map (·.name) ++ externDynlibs.map (·.name)
+    let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?)
+    let depTrace :=
+      linksTrace.mix <| modLibsTrace.mix <| externLibsTrace.mix
+      <| (← getLeanTrace).mix <| (pureHash mod.linkArgs).mix <|
+      platformTrace
+    let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
+      let args :=
+        links.map toString ++
+        libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}") ++
+        mod.weakLinkArgs ++ mod.linkArgs
+      compileSharedLib mod.dynlibFile args (← getLeanc)
+    return (⟨mod.dynlibFile, mod.dynlibName⟩, trace)
 
 /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
 def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=

src/lake/Lake/Build/Monad.lean

@@ -1,102 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
--/
-import Lake.Config.Monad
-import Lake.Build.Context
-import Lake.Util.EStateT
-
-open System
-
-namespace Lake
-
-def mkBuildContext (ws : Workspace) (config : BuildConfig) : IO BuildContext := do
-  return {
-    opaqueWs := ws,
-    toBuildConfig := config,
-    startedBuilds := ← IO.mkRef 0
-    finishedBuilds := ← IO.mkRef 0,
-    leanTrace := Hash.ofString ws.lakeEnv.leanGithash
-  }
-
-def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
-| Except.ok a => pure a
-| Except.error cycle => do
-  let cycle := cycle.map (s!"  {·}")
-  error s!"build cycle detected:\n{"\n".intercalate cycle}"
-
-/--
-Run the recursive build in the given build store.
-If a cycle is encountered, log it and then fail.
--/
-@[inline] def RecBuildM.runIn (store : BuildStore) (build : RecBuildM α) : BuildM (α × BuildStore) := do
-  let (res, store) ← EStateT.run store <| ReaderT.run build []
-  return (← failOnBuildCycle res, store)
-
-/--
-Run the recursive build in a fresh build store.
-If a cycle is encountered, log it and then fail.
--/
-@[inline] def RecBuildM.run (build : RecBuildM α) : BuildM α := do
-  (·.1) <$> build.runIn {}
-
-/--
-Busy waits to acquire the lock represented by the `lockFile`.
-Prints a warning if on the first time it has to wait.
--/
-@[inline] partial def busyAcquireLockFile (lockFile : FilePath) : IO PUnit := do
-  busyLoop true
-where
-  busyLoop firstTime :=
-    try
-      -- Remark: fail if already exists
-      -- (not part of POSIX, but supported on all our platforms)
-      createParentDirs lockFile
-      let h ← IO.FS.Handle.mk lockFile .writeNew
-      h.putStrLn <| toString <| ← IO.Process.getPID
-    catch
-      | .alreadyExists .. => do
-        if firstTime then
-          let stderr ← IO.getStderr
-          stderr.putStrLn s!"warning: waiting for prior `lake build` invocation to finish... (remove '{lockFile}' if stuck)"
-          stderr.flush
-        IO.sleep (ms := 300)
-        busyLoop false
-      | e => throw e
-
-/-- Busy wait to acquire the lock of `lockFile`, run `act`, and then release the lock. -/
-@[inline] def withLockFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (lockFile : FilePath) (act : m α) : m α := do
-  try
-    busyAcquireLockFile lockFile; act
-  finally show IO _ from do
-    try
-      IO.FS.removeFile lockFile
-    catch
-      | .noFileOrDirectory .. => IO.eprintln <|
-        s!"warning: `{lockFile}` was deleted before the lock was released"
-      | e => throw e
-
-/-- The name of the Lake build lock file name (i.e., `lake.lock`). -/
-def lockFileName : String :=
-  "lake.lock"
-
-/-- The workspace's build lock file. -/
-@[inline] def Workspace.lockFile (self : Workspace) : FilePath :=
-  self.root.buildDir / lockFileName
-
-/-- Run the given build function in the Workspace's context. -/
-@[inline] def Workspace.runBuild (ws : Workspace) (build : BuildM α) (config : BuildConfig := {}) : LogIO α := do
-  let ctx ← mkBuildContext ws config
-  /-
-  TODO:
-  The lock file has been temporarily disabled (by lean4#2445)
-  until we have an API for catching `Ctrl-C` during a build.
-  Absent this, the lock file was too disruptive for users.
-  -/
-  -- withLockFile ws.lockFile do
-  build.run ctx
-
-/-- Run the given build function in the Lake monad's workspace. -/
-@[inline] def runBuild (build : BuildM α) (config : BuildConfig := {}) : LakeT LogIO α := do
-  (← getWorkspace).runBuild build config

src/lake/Lake/Build/Package.lean

@@ -16,7 +16,7 @@ open System
 namespace Lake
 
 /-- Compute a topological ordering of the package's transitive dependencies. -/
-def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do
+def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
   (·.toArray) <$> self.deps.foldlM (init := OrdPackageSet.empty) fun deps dep => do
     return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep
 
@@ -28,7 +28,7 @@ def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
 Build the `extraDepTargets` for the package and its transitive dependencies.
 Also fetch pre-built releases for the package's' dependencies.
 -/
-def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do
+def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) := do
   let mut job := BuildJob.nil
   -- Build dependencies' extra dep targets
   for dep in self.deps do
@@ -46,10 +46,11 @@ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Uni
 
 /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
-  mkFacetJobConfigSmall Package.recBuildExtraDepTargets
+  mkFacetJobConfig Package.recBuildExtraDepTargets
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do
+def Package.fetchRelease (self : Package) : SpawnM (BuildJob Unit) :=
+  withRegisterJob "Fetching {self.name} cloud release" <| Job.async do
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
@@ -62,12 +63,12 @@ def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.as
   let logName := s!"{self.name}/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
   let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
-  let upToDate ← buildUnlessUpToDate' self.buildArchiveFile depTrace traceFile do
-    logStep s!"Downloading {self.name} cloud release"
-    download logName url self.buildArchiveFile
+  let upToDate ← buildUnlessUpToDate? self.buildArchiveFile depTrace traceFile do
+    logVerbose s!"downloading {logName}"
+    download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do
-    logStep s!"Unpacking {self.name} cloud release"
-    untar logName self.buildArchiveFile self.buildDir
+    logVerbose s!"unpacking {logName}"
+    untar self.buildArchiveFile self.buildDir
   return ((), .nil)
 
 /-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
@@ -75,14 +76,14 @@ def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
   mkFacetJobConfig (·.fetchRelease)
 
 /-- Perform a build job after first checking for a cloud release for the package. -/
-def Package.afterReleaseAsync (self : Package) (build : SchedulerM (Job α)) : IndexBuildM (Job α) := do
+def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
   if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
     (← self.release.fetch).bindAsync fun _ _ => build
   else
     build
 
 /-- Perform a build after first checking for a cloud release for the package. -/
-def Package.afterReleaseSync (self : Package) (build : BuildM α) : IndexBuildM (Job α) := do
+def Package.afterReleaseSync (self : Package) (build : JobM α) : FetchM (Job α) := do
   if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
     (← self.release.fetch).bindSync fun _ _ => build
   else

src/lake/Lake/Build/Run.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
+-/
+import Lake.Util.Lock
+import Lake.Build.Index
+
+/-! # Build Runner
+
+This module defines the top-level functions used to execute a
+Lake build, monitor its progress, and await the result.
+-/
+
+open System
+
+namespace Lake
+
+/-- Create a fresh build context from a workspace and a build configuration. -/
+def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext := do
+  return {
+    opaqueWs := ws,
+    toBuildConfig := config,
+    registeredJobs := ← IO.mkRef #[],
+    leanTrace := Hash.ofString ws.lakeEnv.leanGithash
+  }
+
+/--
+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
+failing build jobs (e.g., when using `-q` or non-verbose `--no-build`).
+-/
+def Workspace.runFetchM
+  (ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {})
+: IO α := do
+  let ctx ← mkBuildContext ws cfg
+  let out ← if cfg.useStdout then IO.getStdout else IO.getStderr
+  let useANSI ← out.isTty
+  let verbosity := cfg.verbosity
+  let showProgress :=
+    (cfg.noBuild && verbosity == .verbose) ||
+    verbosity != .quiet
+  let caption := "Computing build jobs"
+  let header := s!"[?/?] {caption}"
+  if showProgress then
+    out.putStr header; out.flush
+  let (io, a?, log) ← IO.FS.withIsolatedStreams (build.run.run'.run ctx).captureLog
+  let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error
+  let failed := log.any (·.level ≥ failLv)
+  if !failed && io.isEmpty && !log.hasVisibleEntries verbosity then
+    if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
+  else
+    unless showProgress do
+      out.putStr header
+    out.putStr "\n"
+    if failed || log.hasVisibleEntries verbosity then
+      let v := if failed then .verbose else verbosity
+      log.replay (logger := MonadLog.stream out v)
+    unless io.isEmpty do
+      out.putStr "stdout/stderr:\n"
+      out.putStr io
+    out.flush
+  let failures := if failed then #[caption] else #[]
+  let jobs ← ctx.registeredJobs.get
+  let numJobs := jobs.size
+  let failures ← numJobs.foldM (init := failures) fun i s => Prod.snd <$> StateT.run (s := s) do
+    let (caption, job) := jobs[i]!
+    let header := s!"[{i+1}/{numJobs}] {caption}"
+    if showProgress then
+      out.putStr header; out.flush
+    let log := (← job.wait).state
+    let failed := log.any (·.level ≥ failLv)
+    if failed then modify (·.push caption)
+    if !(failed || log.hasVisibleEntries verbosity) then
+      if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
+    else
+      unless showProgress do
+        out.putStr header
+      out.putStr "\n"
+      let v := if failed then .verbose else verbosity
+      log.replay (logger := MonadLog.stream out v)
+      out.flush
+  if failures.isEmpty then
+    let some a := a?
+      | error "build failed"
+    return a
+  else
+    out.putStr "Some build steps logged failures:\n"
+    failures.forM (out.putStr s!"- {·}\n")
+    error "build failed"
+
+/-- Run a build function in the Workspace's context and await the result. -/
+@[inline] def Workspace.runBuild
+  (ws : Workspace) (build : FetchM (BuildJob α)) (cfg : BuildConfig := {})
+: IO α := do
+  let job ← ws.runFetchM build cfg
+  let some a ← job.wait? | error "build failed"
+  return a
+
+/-- Produce a build job in the Lake monad's workspace and await the result. -/
+@[inline] def runBuild
+  (build : FetchM (BuildJob α)) (cfg : BuildConfig := {})
+: LakeT IO α := do
+  (← getWorkspace).runBuild build cfg

src/lake/Lake/Build/Targets.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Monad
+import Lake.Config.Monad
 
 /-! # Build Target Fetching
 Utilities for fetching package, library, module, and executable targets and facets.
@@ -15,39 +15,39 @@ namespace Lake
 
 /-- Fetch the build job of the specified package target. -/
 def Package.fetchTargetJob (self : Package)
-(target : Name) : IndexBuildM (BuildJob Unit) :=  do
+(target : Name) : FetchM (BuildJob Unit) :=  do
   let some config := self.findTargetConfig? target
     | error s!"package '{self.name}' has no target '{target}'"
   return config.getJob (← fetch <| self.target target)
 
 /-- Fetch the build result of a target. -/
 protected def TargetDecl.fetch (self : TargetDecl)
-[FamilyOut CustomData (self.pkg, self.name) α] : IndexBuildM α := do
+[FamilyOut CustomData (self.pkg, self.name) α] : FetchM α := do
   let some pkg ← findPackage? self.pkg
     | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
   fetch <| pkg.target self.name
 
 /-- Fetch the build job of the target. -/
-def TargetDecl.fetchJob (self : TargetDecl) : IndexBuildM (BuildJob Unit) :=  do
+def TargetDecl.fetchJob (self : TargetDecl) : FetchM (BuildJob Unit) :=  do
   let some pkg ← findPackage? self.pkg
     | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
   return self.config.getJob (← fetch <| pkg.target self.name)
 
 /-- Fetch the build result of a package facet. -/
 @[inline] protected def PackageFacetDecl.fetch (pkg : Package)
-(self : PackageFacetDecl) [FamilyOut PackageData self.name α] : IndexBuildM α := do
+(self : PackageFacetDecl) [FamilyOut PackageData self.name α] : FetchM α := do
   fetch <| pkg.facet self.name
 
 /-- Fetch the build job of a package facet. -/
 def PackageFacetConfig.fetchJob (pkg : Package)
-(self : PackageFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+(self : PackageFacetConfig name) : FetchM (BuildJob Unit) :=  do
   let some getJob := self.getJob?
     | error s!"package facet '{name}' has no associated build job"
   return getJob <| ← fetch <| pkg.facet self.name
 
 /-- Fetch the build job of a library facet. -/
 def Package.fetchFacetJob (name : Name)
-(self : Package) : IndexBuildM (BuildJob Unit) :=  do
+(self : Package) : FetchM (BuildJob Unit) :=  do
   let some config := (← getWorkspace).packageFacetConfigs.find? name
     | error s!"package facet '{name}' does not exist in workspace"
   inline <| config.fetchJob self
@@ -56,21 +56,21 @@ def Package.fetchFacetJob (name : Name)
 
 /-- Fetch the build result of a module facet. -/
 @[inline] protected def ModuleFacetDecl.fetch (mod : Module)
-(self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : IndexBuildM α := do
+(self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : FetchM α := do
   fetch <| mod.facet self.name
 
 /-- Fetch the build job of a module facet. -/
 def ModuleFacetConfig.fetchJob (mod : Module)
-(self : ModuleFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+(self : ModuleFacetConfig name) : FetchM (BuildJob Unit) :=  do
   let some getJob := self.getJob?
-    | error "module facet '{self.name}' has no associated build job"
+    | error s!"module facet '{self.name}' has no associated build job"
   return getJob <| ← fetch <| mod.facet self.name
 
 /-- Fetch the build job of a module facet. -/
 def Module.fetchFacetJob
-(name : Name) (self : Module) : IndexBuildM (BuildJob Unit) :=  do
+(name : Name) (self : Module) : FetchM (BuildJob Unit) :=  do
   let some config := (← getWorkspace).moduleFacetConfigs.find? name
-    | error "library facet '{name}' does not exist in workspace"
+    | error s!"library facet '{name}' does not exist in workspace"
   inline <| config.fetchJob self
 
 /-! ## Lean Library Facets -/
@@ -79,26 +79,26 @@ def Module.fetchFacetJob
 @[inline] def LeanLibConfig.get
 (self : LeanLibConfig) [Monad m] [MonadError m] [MonadLake m] : m LeanLib := do
   let some lib ← findLeanLib? self.name
-    | error "Lean library '{self.name}' does not exist in the workspace"
+    | error s!"Lean library '{self.name}' does not exist in the workspace"
   return lib
 
 /-- Fetch the build result of a library facet. -/
 @[inline] protected def LibraryFacetDecl.fetch (lib : LeanLib)
-(self : LibraryFacetDecl) [FamilyOut LibraryData self.name α] : IndexBuildM α := do
+(self : LibraryFacetDecl) [FamilyOut LibraryData self.name α] : FetchM α := do
   fetch <| lib.facet self.name
 
 /-- Fetch the build job of a library facet. -/
 def LibraryFacetConfig.fetchJob (lib : LeanLib)
-(self : LibraryFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+(self : LibraryFacetConfig name) : FetchM (BuildJob Unit) :=  do
   let some getJob := self.getJob?
-    | error "library facet '{self.name}' has no associated build job"
+    | error s!"library facet '{self.name}' has no associated build job"
   return getJob <| ← fetch <| lib.facet self.name
 
 /-- Fetch the build job of a library facet. -/
 def LeanLib.fetchFacetJob (name : Name)
-(self : LeanLib) : IndexBuildM (BuildJob Unit) :=  do
+(self : LeanLib) : FetchM (BuildJob Unit) :=  do
   let some config := (← getWorkspace).libraryFacetConfigs.find? name
-    | error "library facet '{name}' does not exist in workspace"
+    | error s!"library facet '{name}' does not exist in workspace"
   inline <| config.fetchJob self
 
 /-! ## Lean Executable Target -/
@@ -107,10 +107,14 @@ def LeanLib.fetchFacetJob (name : Name)
 @[inline] def LeanExeConfig.get (self : LeanExeConfig)
 [Monad m] [MonadError m] [MonadLake m] : m LeanExe := do
   let some exe ← findLeanExe? self.name
-    | error "Lean executable '{self.name}' does not exist in the workspace"
+    | error s!"Lean executable '{self.name}' does not exist in the workspace"
   return exe
 
 /-- Fetch the build of the Lean executable. -/
 @[inline] def LeanExeConfig.fetch
-(self : LeanExeConfig) : IndexBuildM (BuildJob FilePath) := do
+(self : LeanExeConfig) : FetchM (BuildJob FilePath) := do
   (← self.get).exe.fetch
+
+/-- Fetch the build of the Lean executable. -/
+@[inline] def LeanExe.fetch (self : LeanExe) : FetchM (BuildJob FilePath) :=
+  self.exe.fetch

src/lake/Lake/Build/Topological.lean

@@ -77,22 +77,25 @@ define the `acyclicRecFetch` below to guard against such cases.
 -/
 
 /--
-A `recFetch` augmented by a `CycleT` to guard against recursive cycles.
+A `recFetch` augmented by a `MonadCycle` to guard against recursive cycles.
 If the set of visited keys is finite, this function should provably terminate.
 
 We use `keyOf` to the derive the unique key of a fetch from its descriptor
 `a : α`. We do this because descriptors may not be comparable and/or contain
 more information than necessary to determine uniqueness.
 -/
-@[inline] def recFetchAcyclic [BEq κ] [Monad m]
-(keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) :=
-  recFetch fun a recurse =>
+@[specialize] def recFetchAcyclic
+  [BEq κ] [Monad m] [MonadCycle κ m]
+  (keyOf : α → κ) (fetch : DRecFetchFn α β m)
+: DFetchFn α β m :=
+  recFetch fun a recurse => guardCycle (keyOf a) do
     /-
     NOTE: We provide the stack directly to `recurse` rather than
-    get it through `ReaderT` to prevent it being overridden by the `fetch`
-    function (and thereby potentially produce a cycle).
+    using the version in the monad to prevent it being overridden by
+    the `fetch` function (and thereby potentially produce a cycle).
     -/
-    guardCycle (keyOf a) fun stack => fetch a (recurse · stack) stack
+    let stack ← getCallStack
+    fetch a fun a => withCallStack stack (recurse a)
 
 /-!
 When building, we usually do not want to build the same thing twice during
@@ -105,8 +108,9 @@ future fetches. This is what `recFetchMemoize` below does.
 `recFetchAcyclic` augmented with a `MonadDStore` to
 memoize fetch results and thus avoid computing the same result twice.
 -/
-@[inline] def recFetchMemoize [BEq κ] [Monad m] [MonadDStore κ β m]
-(keyOf : α → κ) (fetch : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
-: DFetchFn α (fun a => β (keyOf a)) (CycleT κ m) :=
-  recFetchAcyclic keyOf fun a recurse =>
+@[specialize] def recFetchMemoize
+  [BEq κ] [Monad m] [MonadCycle κ m] [MonadDStore κ β m]
+  (keyOf : α → κ) (fetch : DRecFetchFn α (fun a => β (keyOf a)) m)
+: DFetchFn α (fun a => β (keyOf a)) m :=
+  inline <| recFetchAcyclic keyOf fun a recurse =>
     fetchOrCreate (keyOf a) do fetch a recurse

src/lake/Lake/Build/Trace.lean

@@ -12,6 +12,10 @@ namespace Lake
 /-! # Utilities -/
 --------------------------------------------------------------------------------
 
+/-- Creates any missing parent directories of `path`. -/
+@[inline] def createParentDirs (path : FilePath) : IO Unit := do
+  if let some dir := path.parent then IO.FS.createDirAll dir
+
 class CheckExists.{u} (i : Type u) where
   /-- Check whether there already exists an artifact for the given target info. -/
   checkExists : i → BaseIO Bool
@@ -38,7 +42,7 @@ class NilTrace.{u} (t : Type u) where
 
 export NilTrace (nilTrace)
 
-instance [NilTrace t] : Inhabited t := ⟨nilTrace⟩
+instance inhabitedOfNilTrace [NilTrace t] : Inhabited t := ⟨nilTrace⟩
 
 class MixTrace.{u} (t : Type u) where
   /-- Combine two traces. The result should be dirty if either of the inputs is dirty. -/
@@ -255,7 +259,8 @@ If not, check if the info is newer than this trace's modification time.
   else
     self.checkAgainstTime info
 
-@[inline] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
+@[inline] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit := do
+  createParentDirs traceFile
   IO.FS.writeFile traceFile self.hash.toString
 
 end BuildTrace

src/lake/Lake/CLI/Actions.lean

@@ -3,38 +3,39 @@ 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.Index
+import Lake.Build.Run
+import Lake.Build.Targets
 
 namespace Lake
 
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
   IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)
 
-def exe (name : Name) (args  : Array String := #[]) (buildConfig : BuildConfig := {}) : LakeT LogIO UInt32 := do
+def exe (name : Name) (args  : Array String := #[]) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
   let ws ← getWorkspace
-  if let some exe := ws.findLeanExe? name then
-    let exeFile ← ws.runBuild (exe.build >>= (·.await)) buildConfig
-    env exeFile.toString args
-  else
-    error s!"unknown executable `{name}`"
+  let some exe := ws.findLeanExe? name
+    | error s!"unknown executable `{name}`"
+  let exeFile ← ws.runBuild exe.fetch buildConfig
+  env exeFile.toString args
 
 def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
   let mut args :=
     #["release", "upload", tag, pkg.buildArchiveFile.toString, "--clobber"]
   if let some repo := pkg.releaseRepo? then
     args := args.append #["-R", repo]
-  tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile
-  logInfo s!"Uploading {tag}/{pkg.buildArchive}"
+  logInfo s!"packing {pkg.buildArchive}"
+  tar pkg.buildDir pkg.buildArchiveFile
+  logInfo s!"uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
 
-def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT LogIO UInt32 := do
+def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
   let pkgName := pkg.name.toString (escape := false)
   if pkg.testRunner.isAnonymous then
     error s!"{pkgName}: no test runner script or executable"
   else if let some script := pkg.scripts.find? pkg.testRunner then
     script.run args
   else if let some exe := pkg.findLeanExe? pkg.testRunner then
-    let exeFile ← runBuild (exe.build >>= (·.await)) buildConfig
+    let exeFile ← runBuild exe.fetch buildConfig
     env exeFile.toString args.toArray
   else
     error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`"

src/lake/Lake/CLI/Build.lean

@@ -14,9 +14,6 @@ structure BuildSpec where
   info : BuildInfo
   getBuildJob : BuildData info.key → BuildJob Unit
 
-@[inline] def BuildSpec.getJob (self : BuildSpec) (data : BuildData self.info.key) : Job Unit :=
-  discard <| self.getBuildJob data
-
 @[inline] def BuildData.toBuildJob
 [FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit :=
   discard <| ofFamily data
@@ -32,12 +29,11 @@ structure BuildSpec where
     | throw <| CliError.nonCliFacet facetType facet
   return {info, getBuildJob := h ▸ getJob}
 
-def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) :=
-  self.getJob <$> buildIndexTop' self.info
+@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) :=
+  self.getBuildJob <$> self.info.fetch
 
-def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do
-  let jobs ← RecBuildM.run do specs.mapM (·.build)
-  jobs.forM (discard <| ·.await)
+def buildSpecs (specs : Array BuildSpec) : FetchM (BuildJob Unit) := do
+  BuildJob.mixArray (← specs.mapM (·.fetch))
 
 /-! ## Parsing CLI Build Target Specifiers -/
 

src/lake/Lake/CLI/Help.lean

@@ -43,6 +43,7 @@ OPTIONS:
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update, -U          update manifest before building
   --reconfigure, -R     elaborate configuration files instead of using OLeans
+  --wfail               report a build failure if warnings are logged
 
 See `lake help <command>` for more information on a specific command."
 

src/lake/Lake/CLI/Init.lean

@@ -248,7 +248,8 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (lang : Config
           "no known toolchain name for the current Elan/Lean/Lake"
   else
     if tmp = .math then
-      download "lean-toolchain" mathToolchainUrl toolchainFile
+      logInfo "downloading mathlib `lean-toolchain` file"
+      download mathToolchainUrl toolchainFile
     else
       IO.FS.writeFile toolchainFile <| env.toolchain ++ "\n"
 

src/lake/Lake/CLI/Main.lean

@@ -40,6 +40,7 @@ structure LakeOptions where
   oldMode : Bool := false
   trustHash : Bool := true
   noBuild : Bool := false
+  failIfWarnings : Bool := false
 
 /-- Get the Lean installation. Error if missing. -/
 def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
@@ -74,10 +75,13 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
   }
 
 /-- Make a `BuildConfig` from a `LakeOptions`. -/
-def LakeOptions.mkBuildConfig (opts : LakeOptions) : BuildConfig where
+def LakeOptions.mkBuildConfig (opts : LakeOptions) (useStdout := false) : BuildConfig where
   oldMode := opts.oldMode
   trustHash := opts.trustHash
   noBuild := opts.noBuild
+  verbosity := opts.verbosity
+  failIfWarnings := opts.failIfWarnings
+  useStdout := useStdout
 
 export LakeOptions (mkLoadConfig mkBuildConfig)
 
@@ -96,9 +100,6 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
 instance : MonadLift LogIO CliStateM :=
   ⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
 
-instance : MonadLift OptionIO MainM where
-  monadLift x := x.adaptExcept (fun _ => 1)
-
 /-! ## Argument Parsing -/
 
 def takeArg (arg : String) : CliM String := do
@@ -159,6 +160,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
 | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
+| "--wfail"       => modifyThe LakeOptions ({· with failIfWarnings := true})
 | "--dir"         => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
 | "--file"        => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
 | "--lean"        => do setLean <| ← takeOptArg "--lean" "path or command"
@@ -284,14 +286,14 @@ protected def new : CliM PUnit := do
   let opts ← getThe LakeOptions
   let name ← takeArg "package name"
   let (tmp, lang) ← parseTemplateLangSpec <| (← takeArg?).getD ""
-  noArgsRem do MainM.runLogIO (new name tmp lang (← opts.computeEnv) opts.rootDir) opts.verbosity
+  noArgsRem do new name tmp lang (← opts.computeEnv) opts.rootDir
 
 protected def init : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let name := (← takeArg?).getD "."
   let (tmp, lang) ← parseTemplateLangSpec <| (← takeArg?).getD ""
-  noArgsRem do MainM.runLogIO (init name tmp lang (← opts.computeEnv) opts.rootDir) opts.verbosity
+  noArgsRem do init name tmp lang (← opts.computeEnv) opts.rootDir
 
 protected def build : CliM PUnit := do
   processOptions lakeOption
@@ -300,22 +302,21 @@ protected def build : CliM PUnit := do
   let ws ← loadWorkspace config opts.updateDeps
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
-  let buildConfig := mkBuildConfig opts
-  ws.runBuild (buildSpecs specs) buildConfig |>.run (MonadLog.io opts.verbosity)
+  let buildConfig := mkBuildConfig opts (useStdout := true)
+  ws.runBuild (buildSpecs specs) buildConfig
 
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
-  noArgsRem do
-    liftM <| discard <| (loadWorkspace config opts.updateDeps).run (MonadLog.io opts.verbosity)
+  discard <| loadWorkspace config opts.updateDeps
 
 protected def update : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let toUpdate := (← getArgs).foldl (·.insert <| stringToLegalOrSimpleName ·) {}
-  liftM <| (updateManifest config toUpdate).run (MonadLog.io opts.verbosity)
+  updateManifest config toUpdate
 
 protected def upload : CliM PUnit := do
   processOptions lakeOption
@@ -323,8 +324,7 @@ protected def upload : CliM PUnit := do
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
-  noArgsRem do
-    liftM <| uploadRelease ws.root tag |>.run (MonadLog.io opts.verbosity)
+  uploadRelease ws.root tag
 
 protected def setupFile : CliM PUnit := do
   processOptions lakeOption
@@ -342,7 +342,7 @@ protected def test : CliM PUnit := do
   let ws ← loadWorkspace config
   noArgsRem do
   let x := ws.root.test opts.subArgs (mkBuildConfig opts)
-  exit <| ← x.run (mkLakeContext ws) |>.run (MonadLog.io opts.verbosity)
+  exit <| ← x.run (mkLakeContext ws)
 
 protected def checkTest : CliM PUnit := do
   processOptions lakeOption
@@ -402,7 +402,7 @@ protected def exe : CliM PUnit := do
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
   let exe ← parseExeTargetSpec ws exeSpec
-  let exeFile ← ws.runBuild (exe.build >>= (·.await)) <| mkBuildConfig opts
+  let exeFile ← ws.runBuild exe.fetch (mkBuildConfig opts)
   exit <| ← (env exeFile.toString args.toArray).run <| mkLakeContext ws
 
 protected def lean : CliM PUnit := do
@@ -421,7 +421,7 @@ protected def lean : CliM PUnit := do
     cmd := ws.lakeEnv.lean.lean.toString
     env := ws.augmentedEnvVars
   }
-  logProcCmd spawnArgs logVerbose
+  logVerbose (mkCmdLog spawnArgs)
   let rc ← IO.Process.spawn spawnArgs >>= (·.wait)
   exit rc
 

src/lake/Lake/CLI/Serve.lean

@@ -21,13 +21,16 @@ and falls back to plain `lean --server`.
 def invalidConfigEnvVar := "LAKE_INVALID_CONFIG"
 
 /--
-Build a list of imports of a file and print the `.olean` and source directories of every used package, as well as the server options for the file.
+Build a list of imports of a file and print the `.olean` and source directories
+of every used package, as well as the server options for the file.
 If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).
 
-The `setup-file` command is used internally by Lean 4 server.
+The `setup-file` command is used internally by the Lean 4 server.
 -/
-def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
-(buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal) : MainM PUnit := do
+def setupFile
+  (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
+  (buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal)
+: MainM PUnit := do
   if (← configFileExists loadConfig.configFile) then
     if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
       IO.eprint errLog
@@ -35,9 +38,8 @@ def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String
       exit 1
     let ws ← MainM.runLogIO (loadWorkspace loadConfig) verbosity
     let imports := imports.foldl (init := #[]) fun imps imp =>
-    if let some mod := ws.findModule? imp.toName then imps.push mod else imps
-    let dynlibs ← ws.runBuild (buildImportsAndDeps imports) buildConfig
-      |>.run (MonadLog.eio verbosity)
+      if let some mod := ws.findModule? imp.toName then imps.push mod else imps
+    let dynlibs ← MainM.runLogIO (ws.runBuild (buildImportsAndDeps imports) buildConfig) verbosity
     let paths : LeanPaths := {
       oleanPath := ws.leanPath
       srcPath := ws.leanSrcPath
@@ -65,14 +67,14 @@ with the given additional `args`.
 -/
 def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
   let (extraEnv, moreServerArgs) ← do
-    let (log, ws?) ← loadWorkspace config |>.captureLog
-    IO.eprint log
+    let (ws?, log) ← (loadWorkspace config).captureLog
+    log.replay (logger := MonadLog.stderr)
     if let some ws := ws? then
       let ctx := mkLakeContext ws
       pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreGlobalServerArgs)
     else
       IO.eprintln "warning: package configuration has errors, falling back to plain `lean --server`"
-      pure (config.lakeEnv.baseVars.push (invalidConfigEnvVar, log), #[])
+      pure (config.lakeEnv.baseVars.push (invalidConfigEnvVar, log.toString), #[])
   (← IO.Process.spawn {
     cmd := config.lakeEnv.lean.lean.toString
     args := #["--server"] ++ moreServerArgs ++ args

src/lake/Lake/Config/ExternLibConfig.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Job
+import Lake.Build.Data
 
 namespace Lake
 open Lean System

src/lake/Lake/Config/FacetConfig.lean

@@ -3,15 +3,14 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Mario Carneiro
 -/
-import Lake.Build.Info
-import Lake.Build.Store
+import Lake.Build.Fetch
 
 namespace Lake
 
 /-- A facet's declarative configuration. -/
 structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where
   /-- The facet's build (function). -/
-  build : ι → IndexBuildM (DataFam name)
+  build : ι → FetchM (DataFam name)
   /-- Does this facet produce an associated asynchronous job? -/
   getJob? : Option (DataFam name → BuildJob Unit)
   deriving Inhabited
@@ -19,31 +18,17 @@ structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type
 protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
 
 /-- A smart constructor for facet configurations that are not known to generate targets. -/
-@[inline] def mkFacetConfig (build : ι → IndexBuildM α)
+@[inline] def mkFacetConfig (build : ι → FetchM α)
 [h : FamilyOut Fam facet α] : FacetConfig Fam ι facet where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := none
 
-/--
-A smart constructor for facet configurations that generate jobs for the CLI.
-This is for small jobs that do not the increase the progress counter.
--/
-@[inline] def mkFacetJobConfigSmall (build : ι → IndexBuildM (BuildJob α))
+/-- A smart constructor for facet configurations that generate jobs for the CLI. -/
+@[inline] def mkFacetJobConfig (build : ι → FetchM (BuildJob α))
 [h : FamilyOut Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := some fun data => discard <| ofFamily data
 
-/-- A smart constructor for facet configurations that generate jobs for the CLI.  -/
-@[inline] def mkFacetJobConfig (build : ι → IndexBuildM (BuildJob α))
-[FamilyOut Fam facet (BuildJob α)] : FacetConfig Fam ι facet :=
-  mkFacetJobConfigSmall fun i => do
-    let ctx ← readThe BuildContext
-    ctx.startedBuilds.modify (·+1)
-    let job ← build i
-    job.bindSync (prio := .default + 1) fun a trace => do
-      ctx.finishedBuilds.modify (·+1)
-      return (a, trace)
-
 /-- A dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where
   name : Name

src/lake/Lake/Config/Module.lean

@@ -80,6 +80,9 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def ileanFile (self : Module) : FilePath :=
   self.leanLibPath "ilean"
 
+@[inline] def logFile (self : Module) : FilePath :=
+  self.leanLibPath "log.json"
+
 @[inline] def traceFile (self : Module) : FilePath :=
   self.leanLibPath "trace"
 

src/lake/Lake/Config/TargetConfig.lean

@@ -3,22 +3,21 @@ 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.Info
-import Lake.Build.Store
+import Lake.Build.Fetch
 
 namespace Lake
 
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  build : (pkg : NPackage pkgName) → IndexBuildM (CustomData (pkgName, name))
+  build : (pkg : NPackage pkgName) → FetchM (CustomData (pkgName, name))
   /-- The target's resulting build job. -/
   getJob : CustomData (pkgName, name) → BuildJob Unit
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-(build : (pkg : NPackage pkgName) → IndexBuildM (BuildJob α))
+(build : (pkg : NPackage pkgName) → FetchM (BuildJob α))
 [h : FamilyOut CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob := fun data => discard <| ofFamily data

src/lake/Lake/Config/Workspace.lean

@@ -115,7 +115,7 @@ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Wor
   {self with moduleFacetConfigs := self.moduleFacetConfigs.insert name cfg}
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
-@[inline] def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
+def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
   self.moduleFacetConfigs.find? name
 
 /-- Add a package facet to the workspace. -/
@@ -123,7 +123,7 @@ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : W
   {self with packageFacetConfigs := self.packageFacetConfigs.insert name cfg}
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
-@[inline] def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
+def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
   self.packageFacetConfigs.find? name
 
 /-- Add a library facet to the workspace. -/
@@ -131,7 +131,7 @@ def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : W
   {self with libraryFacetConfigs := self.libraryFacetConfigs.insert cfg.name cfg}
 
 /-- Try to find a library facet configuration in the workspace with the given name. -/
-@[inline] def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
+def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
   self.libraryFacetConfigs.find? name
 
 /-- The workspace's binary directories (which are added to `Path`). -/

src/lake/Lake/DSL/Package.lean

@@ -59,7 +59,7 @@ post_update pkg do
   let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
   let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
   IO.FS.writeFile wsToolchainFile mathlibToolchain
-  let exeFile ← runBuild cache.build >>= (·.await)
+  let exeFile ← runBuild cache.fetch
   let exitCode ← env exeFile.toString #["get"]
   if exitCode ≠ 0 then
     error s!"{pkg.name}: failed to fetch cache"

src/lake/Lake/DSL/Targets.lean

@@ -25,7 +25,7 @@ Define a new module facet. Has one form:
 
 ```lean
 module_facet «facet-name» (mod : Module) : α :=
-  /- build term of type `IndexBuildM (BuildJob α)` -/
+  /- build term of type `FetchM (BuildJob α)` -/
 ```
 
 The `mod` parameter (and its type specifier) is optional.
@@ -39,12 +39,13 @@ kw:"module_facet " sig:buildDeclSig : command => do
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
+    let cap := quote s!"Building {id.getId}"
     let mod ← expandOptSimpleBinder mod?
     `(module_data $id : BuildJob $ty
       $[$doc?:docComment]? @[$attrs,*] abbrev $facetId : ModuleFacetDecl := {
         name := $name
-        config := Lake.mkFacetJobConfig
-          fun $mod => ($defn : IndexBuildM (BuildJob $ty))
+        config := Lake.mkFacetJobConfig fun $mod =>
+          Lake.withRegisterJob $cap ($defn : FetchM (BuildJob $ty))
       } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
 
@@ -53,7 +54,7 @@ Define a new package facet. Has one form:
 
 ```lean
 package_facet «facet-name» (pkg : Package) : α :=
-  /- build term of type `IndexBuildM (BuildJob α)` -/
+  /- build term of type `FetchM (BuildJob α)` -/
 ```
 
 The `pkg` parameter (and its type specifier) is optional.
@@ -67,12 +68,13 @@ kw:"package_facet " sig:buildDeclSig : command => do
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
+    let cap := quote s!"Building {id.getId}"
     let pkg ← expandOptSimpleBinder pkg?
     `(package_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := {
         name := $name
-        config := Lake.mkFacetJobConfig
-          fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
+        config := Lake.mkFacetJobConfig fun $pkg =>
+          Lake.withRegisterJob $cap ($defn : FetchM (BuildJob $ty))
       } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
@@ -81,7 +83,7 @@ Define a new library facet. Has one form:
 
 ```lean
 library_facet «facet-name» (lib : LeanLib) : α :=
-  /- build term of type `IndexBuildM (BuildJob α)` -/
+  /- build term of type `FetchM (BuildJob α)` -/
 ```
 
 The `lib` parameter (and its type specifier) is optional.
@@ -95,12 +97,13 @@ kw:"library_facet " sig:buildDeclSig : command => do
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
+    let cap := quote s!"Building {id.getId}"
     let lib ← expandOptSimpleBinder lib?
     `(library_data $id : BuildJob $ty
       $[$doc?]? @[$attrs,*] abbrev $facetId : LibraryFacetDecl := {
         name := $name
-        config := Lake.mkFacetJobConfig
-          fun $lib => ($defn : IndexBuildM (BuildJob $ty))
+        config := Lake.mkFacetJobConfig fun $lib =>
+          Lake.withRegisterJob $cap ($defn : FetchM (BuildJob $ty))
       } $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
 
@@ -113,7 +116,7 @@ Define a new custom target for the package. Has one form:
 
 ```lean
 target «target-name» (pkg : NPackage _package.name) : α :=
-  /- build term of type `IndexBuildM (BuildJob α)` -/
+  /- build term of type `FetchM (BuildJob α)` -/
 ```
 
 The `pkg` parameter (and its type specifier) is optional.
@@ -129,13 +132,14 @@ kw:"target " sig:buildDeclSig : command => do
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let pkgName := mkIdentFrom id `_package.name
+    let cap := quote s!"Building {id.getId}"
     let pkg ← expandOptSimpleBinder pkg?
     `(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
       $[$doc?]? @[$attrs,*] abbrev $id : TargetDecl := {
         pkg := $pkgName
         name := $name
-        config := Lake.mkTargetJobConfig
-          fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
+        config := Lake.mkTargetJobConfig fun $pkg =>
+          Lake.withRegisterJob $cap ($defn : FetchM (BuildJob $ty))
       }  $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
 
@@ -204,7 +208,7 @@ Define a new external library target for the package. Has one form:
 
 ```lean
 extern_lib «target-name» (pkg : NPackage _package.name) :=
-  /- build term of type `IndexBuildM (BuildJob FilePath)` -/
+  /- build term of type `FetchM (BuildJob FilePath)` -/
 ```
 
 The `pkg` parameter (and its type specifier) is optional.

src/lake/Lake/Load/Elab.lean

@@ -229,11 +229,10 @@ def importConfigFile (cfg : LoadConfig) : LogIO Environment := do
       Lean.writeModule env olean
       h.unlock
       return env
-    | .error e =>
+    | .error e => errorWithLog do
       logError <| toString e
       h.unlock
       IO.FS.removeFile traceFile
-      failure
   let validateTrace h : LogIO Environment := id do
     if cfg.reconfigure then
       elabConfig (← acquireTrace h) cfg.lakeOpts

src/lake/Lake/Load/Toml.lean

@@ -269,10 +269,8 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
     if errs.isEmpty then
       return pkg
     else
-      errs.forM fun {ref, msg} =>
+      errorWithLog <| errs.forM fun {ref, msg} =>
         let pos := ictx.fileMap.toPosition <| ref.getPos?.getD 0
         logError <| mkErrorStringWithPos ictx.fileName pos msg
-      failure
   | .error log =>
-    log.forM fun msg => do logError (← msg.toString)
-    failure
+    errorWithLog <| log.forM fun msg => do logError (← msg.toString)

src/lake/Lake/Util/Async.lean

@@ -1,267 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-import Lake.Util.Task
-import Lake.Util.OptionIO
-import Lake.Util.Lift
-
-/-!
-This module Defines the asynchronous monadic interface for Lake.
-The interface is composed of three major abstract monadic types:
-
-* `m`: The monad of the synchronous action (e.g., `IO`).
-* `n`: The monad of the (a)synchronous task manager (e.g., `BaseIO`).
-* `k`: The monad of the (a)synchronous task (e.g., `IOTask`).
-
-The definitions within this module provide the basic utilities for converting
-between these monads and combining them in different ways.
--/
-
-namespace Lake
-
---------------------------------------------------------------------------------
-/-! # Async / Await Abstraction -/
---------------------------------------------------------------------------------
-
-class Sync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
-  /-- Run the monadic action as a synchronous task. -/
-  sync : m α → n (k α)
-
-export Sync (sync)
-
-class Async (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
-  /-- Run the monadic action as an asynchronous task. -/
-  async : m α → n (k α)
-
-export Async (async)
-
-class Await (k : Type u → Type v) (m : outParam $ Type u → Type w)  where
-  /-- Wait for an (a)synchronous task to finish. -/
-  await : k α → m α
-
-export Await (await)
-
-/-! ## Standard Instances -/
-
-instance : Sync Id Id Task := ⟨Task.pure⟩
-instance : Sync BaseIO BaseIO BaseIOTask := ⟨Functor.map Task.pure⟩
-
-instance [Sync m n k] : Sync (ReaderT ρ m) (ReaderT ρ n) k where
-  sync x := fun r => sync (x r)
-
-instance [Sync m n k] : Sync (ExceptT ε m) n (ExceptT ε k) where
-  sync x := cast (by delta ExceptT; rfl) <| sync (n := n) x.run
-
-instance [Sync m n k] : Sync (OptionT m) n (OptionT k) where
-  sync x := cast (by delta OptionT; rfl) <| sync (n := n) x.run
-
-instance : Sync (EIO ε) BaseIO (EIOTask ε) where
-  sync x := sync <| ExceptT.mk x.toBaseIO
-
-instance : Sync OptionIO BaseIO OptionIOTask where
-  sync x := sync <| OptionT.mk x.toBaseIO
-
-instance : Async Id Id Task := ⟨Task.pure⟩
-instance : Async BaseIO BaseIO BaseIOTask := ⟨BaseIO.asTask⟩
-
-instance [Async m n k] : Async (ReaderT ρ m) (ReaderT ρ n) k where
-  async x := fun r => async (x r)
-
-instance [Async m n k] : Async (ExceptT ε m) n (ExceptT ε k) where
-  async x := cast (by delta ExceptT; rfl) <| async (n := n) x.run
-
-instance [Async m n k] : Async (OptionT m) n (OptionT k) where
-  async x := cast (by delta OptionT; rfl) <| async (n := n) x.run
-
-instance : Async (EIO ε) BaseIO (EIOTask ε) where
-  async x := async <| ExceptT.mk x.toBaseIO
-
-instance : Async OptionIO BaseIO OptionIOTask where
-  async x := async <| OptionT.mk x.toBaseIO
-
-instance : Await Task Id := ⟨Task.get⟩
-
-instance : Await (EIOTask ε) (EIO ε) where
-  await x := IO.wait x >>= liftM
-
-instance : Await OptionIOTask OptionIO where
-  await x := IO.wait x >>= liftM
-
-instance [Await k m] : Await (ExceptT ε k) (ExceptT ε m) where
-  await x := ExceptT.mk <| await x.run
-
-instance [Await k m] : Await (OptionT k) (OptionT m) where
-  await x := OptionT.mk <| await x.run
-
---------------------------------------------------------------------------------
-/-! # Combinators -/
---------------------------------------------------------------------------------
-
-class BindSync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
-  /-- Perform a synchronous action after another (a)synchronous task completes successfully. -/
-  bindSync {α β : Type u} : Task.Priority → k α → (α → m β) → n (k β)
-
-export BindSync (bindSync)
-
-class BindAsync (n : Type u → Type v) (k : Type u → Type u) where
-  /-- Perform a asynchronous task after another (a)synchronous task completes successfully. -/
-  bindAsync {α β : Type u} : k α → (α → n (k β)) → n (k β)
-
-export BindAsync (bindAsync)
-
-class SeqAsync (n : outParam $ Type u → Type v) (k : Type u → Type u) where
-  /-- Combine two (a)synchronous tasks, applying the result of the second one to the first one. -/
-  seqAsync {α β : Type u} : k (α → β) → k α → n (k β)
-
-export SeqAsync (seqAsync)
-
-class SeqLeftAsync (n : outParam $ Type u → Type v) (k : Type u → Type u) where
-  /-- Combine two (a)synchronous tasks, returning the result of the first one. -/
-  seqLeftAsync {α β : Type u} : k α → k β → n (k α)
-
-export SeqLeftAsync (seqLeftAsync)
-
-class SeqRightAsync (n : outParam $ Type u → Type v) (k : Type u → Type u) where
-  /-- Combine two (a)synchronous tasks, returning the result of the second one. -/
-  seqRightAsync {α β : Type u} : k α → k β → n (k β)
-
-export SeqRightAsync (seqRightAsync)
-
-class SeqWithAsync (n : outParam $ Type u → Type v) (k : Type u → Type u) where
-  /-- Combine two (a)synchronous tasks using `f`. -/
-  seqWithAsync {α β : Type u} : (f : α → β → γ) → k α → k β → n (k γ)
-
-export SeqWithAsync (seqWithAsync)
-
-class ApplicativeAsync (n : outParam $ Type u → Type v) (k : Type u → Type u)
-extends SeqAsync n k, SeqLeftAsync n k, SeqRightAsync n k, SeqWithAsync n k where
-  seqAsync      := seqWithAsync fun f a => f a
-  seqLeftAsync  := seqWithAsync fun a _ => a
-  seqRightAsync := seqWithAsync fun _ b => b
-
-/-! ## Standard Instances -/
-
-instance : BindSync Id Id Task := ⟨fun _ => flip Task.map⟩
-instance : BindSync BaseIO BaseIO BaseIOTask := ⟨fun _ => flip BaseIO.mapTask⟩
-
-instance : BindSync (EIO ε) BaseIO (ETask ε) where
-  bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun
-    | Except.ok a => f a |>.toBaseIO
-    | Except.error e => pure <| Except.error e
-
-instance : BindSync OptionIO BaseIO OptionIOTask where
-  bindSync prio ka f := ka.run |> BaseIO.mapTask (prio := prio) fun
-    | some a => f a |>.toBaseIO
-    | none => pure none
-
-instance [BindSync m n k] : BindSync (ReaderT ρ m) (ReaderT ρ n) k where
-  bindSync prio ka f := fun r => bindSync prio ka fun a => f a r
-
-instance [BindSync m n k] [Pure m] : BindSync (ExceptT ε m) n (ExceptT ε k) where
-  bindSync prio ka f := cast (by delta ExceptT; rfl) <| bindSync prio (n := n) ka.run fun
-    | Except.ok a => f a |>.run
-    | Except.error e => pure <| Except.error e
-
-instance [BindSync m n k] [Pure m] : BindSync (OptionT m) n (OptionT k) where
-  bindSync prio ka f := cast (by delta OptionT; rfl) <| bindSync prio ka.run fun
-    | some a => f a |>.run
-    | none => pure none
-
-instance : BindAsync Id Task := ⟨Task.bind⟩
-instance : BindAsync BaseIO BaseIOTask := ⟨BaseIO.bindTask⟩
-
-instance : BindAsync BaseIO (EIOTask ε) where
-  bindAsync ka f := BaseIO.bindTask ka.run fun
-    | Except.ok a => f a
-    | Except.error e => pure <| pure (Except.error e)
-
-instance : BindAsync BaseIO OptionIOTask where
-  bindAsync ka f := BaseIO.bindTask ka.run fun
-    | some a => f a
-    | none => pure (pure none)
-
-instance [BindAsync n k] : BindAsync (ReaderT ρ n) k where
-  bindAsync ka f := fun r => bindAsync ka fun a => f a r
-
-instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (ExceptT ε k) where
-  bindAsync ka f := cast (by delta ExceptT; rfl) <| bindAsync ka.run fun
-    | Except.ok a => f a
-    | Except.error e => pure <| pure <| Except.error e
-
-instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (OptionT k) where
-  bindAsync ka f := cast (by delta OptionT; rfl) <| bindAsync ka.run fun
-    | some a => f a
-    | none => pure (pure none)
-
-instance : ApplicativeAsync Id Task where
-  seqWithAsync f ka kb := ka.bind fun a => kb.bind fun b => pure <| f a b
-
-instance : ApplicativeAsync BaseIO BaseIOTask where
-  seqWithAsync f ka kb := BaseIO.bindTask ka fun a => BaseIO.bindTask kb fun b => pure <| pure <| f a b
-
-instance [ApplicativeAsync n k] : ApplicativeAsync n (ExceptT ε k) where
-  seqWithAsync f ka kb :=
-    let h xa xb : Except ε _ := return f (← xa) (← xb)
-    cast (by delta ExceptT; rfl) <| seqWithAsync (n := n) h ka kb
-
-instance [ApplicativeAsync n k] : ApplicativeAsync n (OptionT k) where
-  seqWithAsync f ka kb :=
-    let h xa xb : Option _ := return f (← xa) (← xb)
-    cast (by delta OptionT; rfl) <| seqWithAsync (n := n) h ka kb
-
---------------------------------------------------------------------------------
-/-! #  List/Array Utilities -/
---------------------------------------------------------------------------------
-
-/-! ## Sequencing (A)synchronous Tasks -/
-
-/-- Combine all (a)synchronous tasks in a `List` from right to left into a single task ending `last`. -/
-def seqLeftList1Async [SeqLeftAsync n k] [Monad n] (last : (k α)) : (tasks : List (k α)) → n (k α)
-| [] => return last
-| t::ts => seqLeftList1Async t ts >>= (seqLeftAsync last ·)
-
-/-- Combine all (a)synchronous tasks in a `List` from right to left into a single task. -/
-def seqLeftListAsync [SeqLeftAsync n k] [Monad n] [Pure k] : (tasks : List (k PUnit)) → n (k PUnit)
-| [] => return (pure ())
-| t::ts => seqLeftList1Async t ts
-
-/-- Combine all (a)synchronous tasks in a `List` from left to right into a single task. -/
-def seqRightListAsync [SeqRightAsync n k] [Monad n] [Pure k] : (tasks : List (k PUnit)) → n (k PUnit)
-| [] => return (pure ())
-| t::ts => ts.foldlM seqRightAsync t
-
-/-- Combine all (a)synchronous tasks in a `Array` from right to left into a single task. -/
-def seqLeftArrayAsync [SeqLeftAsync n k] [Monad n] [Pure k] (tasks : Array (k PUnit)) : n (k PUnit) :=
-  if h : 0 < tasks.size then
-    tasks.pop.foldrM seqLeftAsync (tasks.get ⟨tasks.size - 1, Nat.sub_lt h (by decide)⟩)
-  else
-    return (pure ())
-
-/-- Combine all (a)synchronous tasks in a `Array` from left to right into a single task. -/
-def seqRightArrayAsync [SeqRightAsync n k] [Monad n] [Pure k] (tasks : Array (k PUnit)) : n (k PUnit) :=
-  if h : 0 < tasks.size then
-    tasks.foldlM seqRightAsync (tasks.get ⟨0, h⟩)
-  else
-    return (pure ())
-
-/-! ## Folding (A)synchronous Tasks -/
-
-variable [SeqWithAsync n k] [Monad n] [Pure k]
-
-/-- Fold a `List` of (a)synchronous tasks from right to left (i.e., a right fold) into a single task. -/
-def foldLeftListAsync (f : α → β → β) (init : β) (tasks : List (k α)) : n (k β) :=
-  tasks.foldrM (seqWithAsync f) (pure init)
-
-/-- Fold an `Array` of (a)synchronous tasks from right to left (i.e., a right fold) into a single task. -/
-def foldLeftArrayAsync (f : α → β → β) (init : β) (tasks : Array (k α)) : n (k β) :=
-  tasks.foldrM (seqWithAsync f) (pure init)
-
-/-- Fold a `List` of (a)synchronous tasks from left to right (i.e., a left fold) into a single task. -/
-def foldRightListAsync (f : β → α → β) (init : β) (tasks : List (k α)) : n (k β) :=
-  tasks.foldlM (seqWithAsync f) (pure init)
-
-/-- Fold an `Array` of (a)synchronous tasks from left to right (i.e., a left fold) into a single task. -/
-def foldRightArrayAsync (f : β → α → β) (init : β) (tasks : Array (k α)) : n (k β) :=
-  tasks.foldlM (seqWithAsync f) (pure init)

src/lake/Lake/Util/Cycle.lean

@@ -12,22 +12,68 @@ abbrev CallStack κ := List κ
 /-- A `CallStack` ending in a cycle. -/
 abbrev Cycle κ := CallStack κ
 
-/-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
-abbrev CycleT κ m := ReaderT (CallStack κ) <| ExceptT (Cycle κ) m
+/-- A monad equipped with a call stack. -/
+class MonadCallStackOf (κ :  semiOutParam (Type u)) (m : Type u → Type v) where
+  getCallStack : m (CallStack κ)
+  withCallStack (stack : CallStack κ) (x : m α) : m α
 
-/-- Read the call stack from a CycleT.
-  this specialized version exists to be used in e.g. `BuildM`. -/
-def CycleT.readCallStack [Pure m] : CycleT κ m (CallStack κ) :=
-  fun callStack => ExceptT.mk <| pure (Except.ok callStack)
+/-- Similar to `MonadCallStackOf`, but `κ` is an `outParam` for convenience. -/
+class MonadCallStack (κ :  outParam (Type u)) (m : Type u → Type v) where
+  getCallStack : m (CallStack κ)
+  withCallStack (stack : CallStack κ) (x : m α) : m α
+
+export MonadCallStack (getCallStack withCallStack)
+
+instance [MonadCallStackOf κ m] : MonadCallStack κ m where
+  getCallStack := MonadCallStackOf.getCallStack
+  withCallStack := MonadCallStackOf.withCallStack
+
+instance [MonadLift m n] [MonadFunctor m n] [MonadCallStackOf κ m] : MonadCallStackOf κ n where
+  getCallStack := liftM (m := m) getCallStack
+  withCallStack s := monadMap (m := m) (withCallStack s ·)
+
+/-- A monad equipped with a call stack and the ability to error on a cycle. -/
+class MonadCycleOf (κ :  semiOutParam (Type u)) (m : Type u → Type v) extends MonadCallStackOf κ m where
+  throwCycle (cycle : Cycle κ) : m α
+
+/-- Similar to `MonadCycle`, but `κ` is an `outParam` for convenience. -/
+class MonadCycle (κ :  outParam (Type u)) (m : Type u → Type v) extends MonadCallStack κ m where
+  throwCycle (cycle : Cycle κ) : m α
+
+export MonadCycle (throwCycle)
+
+instance [MonadCycleOf κ m] : MonadCycle κ m where
+  throwCycle := MonadCycleOf.throwCycle
+
+export MonadCycle (throwCycle)
+
+instance [MonadLift m n] [MonadFunctor m n] [MonadCycleOf κ m] : MonadCycleOf κ n where
+  throwCycle cycle := liftM (m := m) (throwCycle cycle)
+
+instance inhabitedOfMonadCycle [MonadCycle κ m] : Inhabited (m α) := ⟨throwCycle []⟩
+
+/-- A transformer that equips a monad with a `CallStack`. -/
+abbrev CallStackT κ m := ReaderT (CallStack κ) m
+
+instance [Monad m] : MonadCallStackOf κ (CallStackT κ m) where
+  getCallStack := read
+  withCallStack s x := x s
+
+/-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
+abbrev CycleT κ m := CallStackT κ <| ExceptT (Cycle κ) m
+
+instance [Monad m] : MonadCycleOf κ (CycleT κ m) where
+  throwCycle := throw
 
 /--
 Add `key` to the monad's `CallStack` before invoking `act`.
 If adding `key` produces a cycle, the cyclic call stack is thrown.
 -/
-@[inline] def guardCycle [BEq κ] [Monad m]
-(key : κ) (act : CycleT κ m α) : CycleT κ m α := do
-  let parents ← read
+@[inline] def guardCycle
+  [BEq κ] [Monad m] [MonadCycle κ m] (key : κ) (act : m α)
+: m α := do
+  let parents ← getCallStack
   if parents.contains key then
-    throw <| key :: (parents.partition (· != key)).1 ++ [key]
+    throwCycle <| key :: (parents.partition (· != key)).1 ++ [key]
   else
-    act (key :: parents)
+    withCallStack (key :: parents) act

src/lake/Lake/Util/EStateT.lean

@@ -1,22 +1,186 @@
 /-
-Copyright (c) 2022 Mac Malone. All rights reserved.
+Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
+Authors: Mac Malone, Leonardo de Moura, Mario Carneiro
 -/
 
 namespace Lake
 
-/-- An exception plus state monad transformer (ι.e., `ExceptT` + `StateT`). -/
-abbrev EStateT.{u,v} (ε : Type u) (σ : Type u) (m : Type u → Type v) :=
-  ExceptT ε <| StateT σ m
+/--
+`EResult ε σ α` is equivalent to `Except ε α × σ`, but using a single
+combined inductive yields a more efficient data representation.
+-/
+inductive EResult (ε : Type u) (σ : Type v) (α : Type w) : Type max u v w
+/-- A success value of type `α`, and a new state `σ`. -/
+| ok    : α → σ → EResult ε σ α
+/-- A failure value of type `ε`, and a new state `σ`. -/
+| error : ε → σ → EResult ε σ α
+
+instance [Inhabited α] [Inhabited σ] : Inhabited (EResult ε σ α) where
+  default := EResult.ok default default
+
+instance [Inhabited ε] [Inhabited σ] : Inhabited (EResult ε σ α) where
+  default := EResult.error default default
+
+/-- Extract the state `σ` from a `EResult ε σ α`. -/
+@[inline] def EResult.state : EResult ε σ α → σ
+| .ok _ s => s
+| .error _ s => s
+
+@[inline] def EResult.setState (s : σ') : EResult ε σ α → EResult ε σ' α
+| .ok a _ => .ok a s
+| .error e _ => .error e s
+
+/-- Extract the result `α` from a `EResult ε σ α`. -/
+@[inline] def EResult.result? : EResult ε σ α → Option α
+| .ok a _ => some a
+| _ => none
+
+/-- Extract the error `ε` from a `EResult ε σ α`. -/
+@[inline] def EResult.error? : EResult ε σ α → Option ε
+| .error e _ => some e
+| _ => none
+
+/-- Convert an `EResult ε σ α` into `Except ε α`, discarding its state. -/
+@[inline] def EResult.toExcept : EResult ε σ α → Except ε α
+| .ok a _ => .ok a
+| .error e _ => .error e
+
+@[always_inline, inline]
+protected def EResult.map (f : α → β) : EResult ε σ α → EResult ε σ β
+| .ok a s => .ok (f a) s
+| .error e s => .error e s
+
+instance : Functor (EResult ε σ) where
+  map := EResult.map
+
+/--
+`EStateT ε σ m` is a combined error and state monad transformer,
+equivalent to `ExceptT ε (StateT σ m)` but more efficient.
+-/
+def EStateT (ε : Type u) (σ : Type v) (m : Type max u v w → Type x) (α : Type w) :=
+  σ → m (EResult ε σ α)
 
 namespace EStateT
-variable {ε : Type u} {σ : Type u} {m : Type u → Type v}
 
-@[inline] def run (init : σ) (self : EStateT ε σ m α) : m (Except ε α × σ) :=
-  ExceptT.run self |>.run init
+instance [Inhabited ε] [Pure m] : Inhabited (EStateT ε σ m α) where
+  default := fun s => pure (EResult.error default s)
 
-@[inline] def run' [Functor m] (init : σ) (self : EStateT ε σ m α) : m (Except ε α) :=
-  ExceptT.run self |>.run' init
+/-- Lift the `m` monad into the `EStateT ε σ m` monad transformer. -/
+@[always_inline, inline]
+protected def lift {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α := fun s => do
+  let a ← x; pure (.ok a s)
 
-end EStateT
+instance [Monad m] : MonadLift m (EStateT ε σ m) := ⟨EStateT.lift⟩
+
+variable {ε ε' : Type u} {σ : Type v} {α β : Type w}
+
+/-- Execute an `EStateT` on initial state `s` to get an `EResult` result. -/
+@[always_inline, inline]
+def run (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α) :=
+  self init
+
+/-- Execute an `EStateT` on initial state `s` to get an `Except` result. -/
+@[always_inline, inline]
+def run' {σ : Type max u w} [Functor m] (init : σ) (self : EStateT ε σ m α) : m (Except ε α) :=
+  EResult.toExcept <$> self init
+
+/-- The `pure` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def pure [Pure m] (a : α) : EStateT ε σ m α := fun s =>
+  pure <| .ok a s
+
+instance [Pure m] : Pure (EStateT ε σ m) where
+  pure := EStateT.pure
+
+/-- The `map` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def map [Functor m] (f : α → β) (x : EStateT ε σ m α) : EStateT ε σ m β := fun s =>
+  x s |> Functor.map fun
+  | .ok a s    => .ok (f a) s
+  | .error e s => .error e s
+
+instance [Functor m] : Functor (EStateT ε σ m) where
+  map := EStateT.map
+
+/-- The `bind` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def bind [Monad m] (x : EStateT ε σ m α) (f : α → EStateT ε σ m β) : EStateT ε σ m β := fun s => do
+  match (← x s) with
+  | .ok a s    => f a s
+  | .error e s => pure <| .error e s
+
+/-- The `seqRight` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def seqRight [Monad m] (x : EStateT ε σ m α) (y : Unit → EStateT ε σ m β) : EStateT ε σ m β := fun s => do
+  match (← x s) with
+  | .ok _ s    => y () s
+  | .error e s => pure <| .error e s
+
+@[always_inline]
+instance [Monad m] : Monad (EStateT ε σ m) where
+  bind     := EStateT.bind
+  seqRight := EStateT.seqRight
+
+/-- The `set` operation of the `EStateT` monad. -/
+@[always_inline, inline]
+protected def set [Pure m] (s : σ) : EStateT ε σ m PUnit.{w+1} := fun _ =>
+  pure <| .ok ⟨⟩ s
+
+/-- The `get` operation of the `EStateT` monad. -/
+@[always_inline, inline]
+protected def get [Pure m]  : EStateT ε σ m σ := fun s =>
+  pure <| .ok s s
+
+/-- The `modifyGet` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def modifyGet [Pure m] (f : σ → Prod α σ) : EStateT ε σ m α := fun s =>
+  match f s with | (a, s) => pure <| .ok a s
+
+instance [Pure m] : MonadStateOf σ (EStateT ε σ m) where
+  set       := EStateT.set
+  get       := EStateT.get
+  modifyGet := EStateT.modifyGet
+
+/-- The `throw` operation of the `EStateT` monad transformer. -/
+@[always_inline, inline]
+protected def throw [Pure m] (e : ε) : EStateT ε σ m α := fun s =>
+  pure <| .error e s
+
+@[always_inline, inline]
+protected def tryCatch [Monad m] (x : EStateT ε σ m α) (handle : ε → EStateT ε σ m α) : EStateT ε σ m α := fun s => do
+  match (← x s) with
+  | .error e s => handle e s
+  | ok         => pure ok
+
+instance [Monad m] : MonadExceptOf ε (EStateT ε σ m) where
+  throw    := EStateT.throw
+  tryCatch := EStateT.tryCatch
+
+@[always_inline, inline]
+protected def orElse [Monad m] (x₁ : EStateT ε σ m α) (x₂ : Unit → EStateT ε σ m α) : EStateT ε σ m α := fun s => do
+  match (← x₁ s) with
+  | .error _ s => x₂ () s
+  | ok         => pure ok
+
+instance [Monad m] : OrElse (EStateT ε σ m α) where
+  orElse := EStateT.orElse
+
+/-- Map the exception type of a `EStateT ε σ m α` by a function `f : ε → ε'`. -/
+@[always_inline, inline]
+def adaptExcept [Functor m] (f : ε → ε') (x : EStateT ε σ m α) : EStateT ε' σ m α := fun s =>
+  x s |> Functor.map fun
+  | .error e s => .error (f e) s
+  | .ok a s    => .ok a s
+
+@[always_inline]
+instance [Monad m] : MonadFinally (EStateT ε σ m) where
+  tryFinally' x h s := do
+    let r ← x s
+    match r with
+    | .ok a s => match (← h (some a) s) with
+      | .ok b s => return .ok (a, b) s
+      | .error e s => return .error e s
+    | .error e₁ s => match (← h none s) with
+      | .ok _ s => return .error e₁ s
+      | .error e₂ s => return .error e₂ s

src/lake/Lake/Util/EquipT.lean

@@ -67,6 +67,9 @@ def lift {α : Type v} (t : m α) : EquipT ρ m α :=
 instance : MonadLift m (EquipT ρ m) where
   monadLift := EquipT.lift
 
+instance : MonadFunctor m (EquipT ρ m) where
+  monadMap f x := fun ctx => f (x ctx)
+
 @[inline] protected
 def failure [Alternative m] {α : Type v} : EquipT ρ m α :=
   fun _ => failure

src/lake/Lake/Util/Lift.lean

@@ -3,8 +3,6 @@ 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.Util.OptionIO
-
 namespace Lake
 
 instance [Pure m] : MonadLiftT Id m where
@@ -34,6 +32,3 @@ instance [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT
 
 instance [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where
   monadLift act := act.toBaseIO >>= liftM
-
-instance [Monad m] [Alternative m] [MonadLiftT BaseIO m] : MonadLiftT OptionIO m where
-  monadLift act := act.toBaseIO >>= liftM

src/lake/Lake/Util/Lock.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
+-/
+
+/-! # Lock File Utilities
+
+This module defines utilities to use a file to ensure mutual exclusions
+between processes manipulating some shared resource. Such a file is termed
+a "lock file".
+
+Lake does not currently use a lock file. Previously, Lake used one for builds,
+but this was removed in [lean4#2445][1]. Without an API for catching `Ctrl-C`
+during a build, the lock file was deemed too disruptive for users.
+
+[1]: https://github.com/leanprover/lean4/pull/2445
+-/
+
+open System
+namespace Lake
+
+@[inline] partial def busyAcquireLockFile (lockFile : FilePath) : IO PUnit := do
+  busyLoop true
+where
+  busyLoop firstTime :=
+    try
+      if let some dir := lockFile.parent then
+        IO.FS.createDirAll dir
+      -- Remark: fail if already exists
+      -- (not part of POSIX, but supported on all our platforms)
+      let h ← IO.FS.Handle.mk lockFile .writeNew
+      h.putStrLn <| toString <| ← IO.Process.getPID
+    catch
+      | .alreadyExists .. => do
+        if firstTime then
+          let stderr ← IO.getStderr
+          stderr.putStrLn s!"warning: waiting for prior `lake build` invocation to finish... (remove '{lockFile}' if stuck)"
+          stderr.flush
+        IO.sleep (ms := 300)
+        busyLoop false
+      | e => throw e
+
+/-- Busy wait to acquire the lock of `lockFile`, run `act`, and then release the lock. -/
+@[inline] def withLockFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (lockFile : FilePath) (act : m α) : m α := do
+  try
+    busyAcquireLockFile lockFile; act
+  finally show IO _ from do
+    try
+      IO.FS.removeFile lockFile
+    catch
+      | .noFileOrDirectory .. => IO.eprintln <|
+        s!"warning: `{lockFile}` was deleted before the lock was released"
+      | e => throw e

src/lake/Lake/Util/Log.lean

@@ -4,93 +4,146 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.Error
-import Lake.Util.OptionIO
+import Lake.Util.EStateT
+import Lean.Data.Json
+import Lean.Message
+
+open Lean
 
 namespace Lake
 
-inductive LogLevel
-| info
-| warning
-| error
-
-inductive Verbosity : Type u
+inductive Verbosity
 | quiet
 | normal
 | verbose
-deriving BEq
+deriving Repr, DecidableEq, Ord
+
+instance : LT Verbosity := ltOfOrd
+instance : LE Verbosity := leOfOrd
+instance : Min Verbosity := minOfLe
+instance : Max Verbosity := maxOfLe
 
 instance : Inhabited Verbosity := ⟨.normal⟩
 
-/-! # Class -/
+inductive LogLevel
+| trace
+| info
+| warning
+| error
+deriving Inhabited, Repr, DecidableEq, Ord, ToJson, FromJson
+
+instance : LT LogLevel := ltOfOrd
+instance : LE LogLevel := leOfOrd
+instance : Min LogLevel := minOfLe
+instance : Max LogLevel := maxOfLe
+
+protected def LogLevel.toString : LogLevel → String
+| .trace => "trace"
+| .info => "info"
+| .warning => "warning"
+| .error => "error"
+
+protected def LogLevel.ofMessageSeverity : MessageSeverity → LogLevel
+| .information => .info
+| .warning => .warning
+| .error => .error
+
+instance : ToString LogLevel := ⟨LogLevel.toString⟩
+
+def LogLevel.visibleAtVerbosity (self : LogLevel) (verbosity : Verbosity) : Bool :=
+  match self with
+  | .trace => verbosity == .verbose
+  | .info => verbosity != .quiet
+  | _ => true
+
+structure LogEntry where
+  level : LogLevel
+  message : String
+  deriving Inhabited, ToJson, FromJson
+
+protected def LogEntry.toString (self : LogEntry) : String :=
+  s!"{self.level}: {self.message.trim}"
+
+instance : ToString LogEntry := ⟨LogEntry.toString⟩
 
 class MonadLog (m : Type u → Type v) where
-  getVerbosity : m Verbosity
-  log (message : String) (level : LogLevel) : m PUnit
+  logEntry (e : LogEntry) : m PUnit
 
-export MonadLog (log getVerbosity)
-
-@[inline] def getIsVerbose [Functor m] [MonadLog m] : m Bool :=
-  getVerbosity <&> (· == .verbose)
-
-@[inline] def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
-  getVerbosity <&> (· == .quiet)
+export MonadLog (logEntry)
 
 @[inline] def logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do
-  if (← getIsVerbose) then log message .info
+  logEntry {level := .trace, message}
 
 @[inline] def logInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do
-  if !(← getIsQuiet) then log message .info
+  logEntry {level := .info, message}
 
 @[inline] def logWarning [MonadLog m] (message : String) : m PUnit :=
-  log message .warning
+  logEntry {level := .warning, message}
 
 @[inline] def logError  [MonadLog m] (message : String) : m PUnit :=
-  log message .error
+  logEntry {level := .error, message}
+
+def logToIO (e : LogEntry) (verbosity : Verbosity) : BaseIO PUnit := do
+  match e.level with
+  | .trace => if verbosity == .verbose then
+    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
+  | .info => if verbosity != .quiet then
+    IO.println e.message.trim |>.catchExceptions fun _ => pure ()
+  | .warning => IO.eprintln s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+  | .error => IO.eprintln s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+
+def logToStream (e : LogEntry) (h : IO.FS.Stream) (verbosity : Verbosity) : BaseIO PUnit := do
+  match e.level with
+  | .trace => if verbosity == .verbose then
+    h.putStrLn s!"trace: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+  | .info => if verbosity != .quiet then
+    h.putStrLn s!"info: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+  | .warning => h.putStrLn s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+  | .error => h.putStrLn s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
+
+@[specialize] def logSerialMessage (msg : SerialMessage) [MonadLog m] : m PUnit :=
+  let str := msg.data
+  let str := if msg.caption.trim.isEmpty then
+    str.trim else s!"{msg.caption.trim}:\n{str.trim}"
+  logEntry {
+    level := .ofMessageSeverity msg.severity
+    message := mkErrorStringWithPos msg.fileName msg.pos str msg.endPos
+  }
 
 namespace MonadLog
 
 @[specialize] def nop [Pure m] : MonadLog m :=
-  ⟨pure .normal, fun _ _ => pure ()⟩
+  ⟨fun _ => pure ()⟩
 
 instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
 
 @[specialize] def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
-  getVerbosity := (pure verbosity : BaseIO _)
-  log msg
-    | .info => IO.println msg.trim |>.catchExceptions fun _ => pure ()
-    | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
-    | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
+  logEntry e := logToIO e verbosity
 
-@[specialize] def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
-  getVerbosity := (pure verbosity : BaseIO _)
-  log msg
-    | .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
-    | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
-    | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
+@[inline] def stream [MonadLiftT BaseIO m] (h : IO.FS.Stream) (verbosity := Verbosity.normal) : MonadLog m where
+  logEntry e := logToStream e h verbosity
 
-@[specialize] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
-  getVerbosity := liftM <| self.getVerbosity
-  log msg lv := liftM <| self.log msg lv
+@[inline] def stdout [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+  logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStdout) verbosity
+
+@[inline] def stderr [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+  logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStderr) verbosity
+
+@[inline] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
+  logEntry e := liftM <| self.logEntry e
 
 instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
 
-/-- Log the given error message and then fail. -/
-@[inline] protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
-  logError msg *> failure
-
 end MonadLog
 
-/-! # Transformers -/
-
 abbrev MonadLogT (m : Type u → Type v) (n : Type v → Type w) :=
-   ReaderT (MonadLog m) n
+  ReaderT (MonadLog m) n
 
 instance [Pure n] [Inhabited α] : Inhabited (MonadLogT m n α) :=
   ⟨fun _ => pure Inhabited.default⟩
 
 instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
-  getVerbosity := do (← read).getVerbosity
-  log msg lv := do (← read).log msg lv
+  logEntry e := do (← read).logEntry e
 
 @[inline] def MonadLogT.adaptMethods [Monad n]
 (f : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α :=
@@ -99,14 +152,125 @@ instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
 @[inline] def  MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
   self MonadLog.nop
 
-abbrev LogIO :=
-  MonadLogT BaseIO OptionIO
+structure Log where
+  entries : Array LogEntry
 
-instance : MonadError LogIO := ⟨MonadLog.error⟩
-instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
+namespace Log
 
-def LogIO.captureLog (self : LogIO α) (verbosity := Verbosity.normal) : BaseIO (String × Option α) :=
-  IO.FS.withIsolatedStreams <| self (MonadLog.eio verbosity) |>.toBaseIO
+@[inline] def empty : Log :=
+  .mk #[]
+
+instance : EmptyCollection Log := ⟨Log.empty⟩
+
+@[inline] def isEmpty (log : Log) : Bool :=
+  log.entries.isEmpty
+
+@[inline] def size (log : Log) : Nat :=
+  log.entries.size
+
+@[inline] def push (log : Log) (e : LogEntry) : Log :=
+  .mk <| log.entries.push e
+
+@[inline] def append (log : Log) (o : Log) : Log :=
+  .mk <| log.entries.append o.entries
+
+instance : Append Log := ⟨Log.append⟩
+
+@[inline] def shrink (log : Log) (n : Nat) : Log :=
+  (.mk <| log.entries.shrink n)
+
+@[inline] def split (log : Log) (n : Nat) : Log × Log :=
+  (.mk <| log.entries.extract 0 n, log.shrink n)
+
+def toString (log : Log) : String :=
+  log.entries.foldl (· ++ ·.toString ++ "\n") ""
+
+instance : ToString Log := ⟨Log.toString⟩
+
+@[inline] def replay [Monad m] [logger : MonadLog m] (log : Log) : m PUnit :=
+  log.entries.forM fun e => logger.logEntry e
+
+@[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)
+
+@[inline] def any (f : LogEntry → Bool) (log : Log) : Bool :=
+  log.entries.any f
+
+def hasVisibleEntries (log : Log) (verbosity := Verbosity.normal) : Bool :=
+  log.any (·.level.visibleAtVerbosity verbosity)
+
+end Log
+
+class MonadGetLog (m : Type → Type v) where
+  getLog : m Log
+
+@[inline] def MonadGetLog.getLogSize [Functor m] [MonadGetLog m] : m Nat :=
+  (·.size) <$> getLog
+
+export MonadGetLog (getLog getLogSize)
+
+instance [MonadLift m n] [MonadGetLog m] : MonadGetLog n where
+  getLog := liftM (m := m) getLog
 
 abbrev LogT (m : Type → Type) :=
-  MonadLogT m m
+  StateT Log m
+
+namespace LogT
+
+instance [Monad m] : MonadGetLog (LogT m) := ⟨get⟩
+
+@[inline] protected def log [Monad m] (e : LogEntry) : LogT m PUnit :=
+  modify (·.push e)
+
+instance [Monad m] : MonadLog (LogT m) := ⟨LogT.log⟩
+
+end LogT
+
+abbrev ELogT (m : Type → Type) :=
+  EStateT Nat Log m
+
+namespace ELogT
+
+instance [Pure m] : MonadGetLog (ELogT m) := ⟨get⟩
+
+@[inline] protected def log [Monad m] (e : LogEntry) : ELogT m PUnit :=
+  modify (·.push e)
+
+instance [Monad m] : MonadLog (ELogT m) := ⟨ELogT.log⟩
+
+/-- Performs `x` and groups all logs generated into an error block. -/
+@[inline] def errorWithLog [Monad m] (x : ELogT m α) : ELogT m β := fun s => do
+  let iniSz := s.size
+  match (← x.run s) with
+  | .ok _ log | .error _ log => pure (.error iniSz log)
+
+@[inline] protected def error [Monad m] (msg : String) : ELogT m α :=
+  errorWithLog (logError msg)
+
+instance [Monad m] : MonadError (ELogT m) := ⟨ELogT.error⟩
+
+@[inline] def replayLog [Alternative n] [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : ELogT m α) : n α := do
+  match (← self {}) with
+  | .ok a log => log.replay (logger := logger) *> pure a
+  | .error _ log => log.replay (logger := logger) *> failure
+
+@[inline] def catchFailure [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := fun log => do
+  match (← self log) with
+  | .error n log => let (h,t) := log.split n; f h t
+  | .ok a log => return (a, log)
+
+@[inline] def captureLog [Monad m] (self : ELogT m α) : m (Option α × Log) := do
+ match (← self {}) with
+ | .ok a log => return (some a, log)
+ | .error _ log => return (none, log)
+
+end ELogT
+
+export ELogT (errorWithLog)
+
+abbrev LogIO := ELogT BaseIO
+
+instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩

src/lake/Lake/Util/MainM.lean

@@ -66,7 +66,7 @@ instance : Alternative MainM where
 
 /-! # Logging and IO -/
 
-instance : MonadLog MainM := MonadLog.eio
+instance : MonadLog MainM := MonadLog.stderr
 
 /-- Print out a error line with the given message and then exit with an error code. -/
 @[inline] protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
@@ -74,9 +74,9 @@ instance : MonadLog MainM := MonadLog.eio
   exit rc
 
 instance : MonadError MainM := ⟨MainM.error⟩
-instance : MonadLift IO MainM := ⟨MonadError.runEIO⟩
+instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
 
 @[inline] def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
-  liftM <| x.run <| MonadLog.eio verbosity
+  x.replayLog (logger := MonadLog.stderr verbosity)
 
 instance : MonadLift LogIO MainM := ⟨runLogIO⟩

src/lake/Lake/Util/OptionIO.lean

@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-namespace Lake
-
-/-- Conceptually identical to `OptionT BaseIO`, but practically more efficient. -/
-def OptionIO := EIO PUnit
-
-instance : Monad OptionIO := inferInstanceAs (Monad (EIO PUnit))
-instance : MonadLift BaseIO OptionIO := inferInstanceAs (MonadLift BaseIO (EIO PUnit))
-
-namespace OptionIO
-
-@[inline] def mk (x : EIO PUnit α) : OptionIO α :=
-  x
-
-@[inline] def toBaseIO (self : OptionIO α) : BaseIO (Option α) :=
-  fun s => match self s with
-  | EStateM.Result.ok a s => EStateM.Result.ok (some a) s
-  | EStateM.Result.error _ s => EStateM.Result.ok none s
-
-@[inline] def toEIO (self : OptionIO α) : EIO PUnit α :=
-  self
-
-@[inline] def toIO (f : Unit → IO.Error) (self : OptionIO α) : IO α :=
-  self.toEIO.toIO f
-
-@[inline] def catchFailure (f : Unit → BaseIO α) (self : OptionIO α) : BaseIO α :=
-  self.toEIO.catchExceptions f
-
-@[inline] protected def failure : OptionIO α :=
-  mk <| throw ()
-
-@[inline] protected def orElse (self : OptionIO α) (f : Unit → OptionIO α) : OptionIO α :=
-  mk <| tryCatch self.toEIO f
-
-instance : Alternative OptionIO where
-  failure := OptionIO.failure
-  orElse := OptionIO.orElse
-
-@[always_inline] instance OptionIO.finally : MonadFinally OptionIO where
-  tryFinally' := fun x h => do
-    match (← x.toBaseIO) with
-    | some a => h (some a) <&> ((a, ·))
-    | none => h none *> failure
-
-@[inline] def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
-  self.toBaseIO.asTask prio

src/lake/Lake/Util/Proc.lean

@@ -7,50 +7,46 @@ import Lake.Util.Log
 
 namespace Lake
 
-@[specialize] def logProcCmd [Monad m]
-(args : IO.Process.SpawnArgs) (log : String → m PUnit) : m Unit := do
+def mkCmdLog (args : IO.Process.SpawnArgs) : String :=
   let envStr := String.join <| args.env.toList.map fun (k, v) =>
     if k == "PATH" then "PATH " else s!"{k}={v.getD ""} " -- PATH too big
   let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
-  log <| "> " ++ envStr ++
-    match args.cwd with
-    | some cwd => s!"{cmdStr}    # in directory {cwd}"
-    | none     => cmdStr
+  let cwd := args.cwd.getD "."
+  s!"{cwd}> {envStr}{cmdStr}"
 
-@[specialize] def logProcOutput [Monad m]
-(out : IO.Process.Output) (log : String → m PUnit) : m Unit := do
+@[inline] def logOutput
+  [Monad m] (out : IO.Process.Output) (log : String → m PUnit)
+: m Unit := do
   unless out.stdout.isEmpty do
     log s!"stdout:\n{out.stdout}"
   unless out.stderr.isEmpty do
     log s!"stderr:\n{out.stderr}"
 
-@[specialize] def logProcWith [Monad m]
-(args : IO.Process.SpawnArgs) (out : IO.Process.Output)
-(log : String → m PUnit) (logOutput := log) : m Unit := do
-  logProcCmd args log
-  logProcOutput out logOutput
+@[inline] def rawProc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO IO.Process.Output := do
+  let iniSz ← getLogSize
+  unless quiet do logVerbose (mkCmdLog args)
+  match (← IO.Process.output args |>.toBaseIO) with
+  | .ok out => return out
+  | .error err =>
+    logError s!"failed to execute '{args.cmd}': {err}"
+    throw iniSz
 
 def proc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO Unit := do
-  match (← IO.Process.output args |>.toBaseIO) with
-  | .ok out =>
-    if out.exitCode = 0 then
-      logProcWith args out logVerbose (logOutput := if quiet then logVerbose else logInfo)
-    else
-      logProcWith args out logError
-      error s!"external command `{args.cmd}` exited with code {out.exitCode}"
-  | .error err =>
-    error s!"failed to execute `{args.cmd}`: {err}"
+  let iniSz ← getLogSize
+  let out ← rawProc args
+  logOutput out (if quiet then logVerbose else logInfo)
+  if out.exitCode ≠ 0 then
+    logError s!"external command '{args.cmd}' exited with code {out.exitCode}"
+    throw iniSz
 
 def captureProc (args : IO.Process.SpawnArgs) : LogIO String := do
-  match (← IO.Process.output args |>.toBaseIO) with
-  | .ok out =>
-    if out.exitCode = 0 then
-      return out.stdout.trim -- remove, e.g., newline at end
-    else
-      logProcWith args out logError
-      error s!"external command `{args.cmd}` exited with code {out.exitCode}"
-  | .error err =>
-    error s!"failed to execute `{args.cmd}`: {err}"
+  let out ← rawProc args (quiet := true)
+  if out.exitCode = 0 then
+    return out.stdout.trim -- remove, e.g., newline at end
+  else errorWithLog do
+    logVerbose (mkCmdLog args)
+    logOutput out logInfo
+    logError s!"external command '{args.cmd}' exited with code {out.exitCode}"
 
 def captureProc? (args : IO.Process.SpawnArgs) : BaseIO (Option String) := do
   EIO.catchExceptions (h := fun _ => pure none) do

src/lake/README.md

@@ -267,7 +267,7 @@ extern_lib «target-name» (pkg : NPackage _package.name) :=
   -- a build function that produces its static library
 ```
 
-The declaration is essentially a wrapper around a `System.FilePath` [target](#custom-targets). Like such a target, the `pkg` parameter and its type specifier are optional and body should be a term of type `IndexBuildM (BuildJob System.FilePath)` function that builds the static library. The `pkg` parameter is of type `NPackage _package.name` to provably demonstrate that it is the package in which the external library is defined.
+The declaration is essentially a wrapper around a `System.FilePath` [target](#custom-targets). Like such a target, the `pkg` parameter and its type specifier are optional and body should be a term of type `FetchM (BuildJob System.FilePath)` function that builds the static library. The `pkg` parameter is of type `NPackage _package.name` to provably demonstrate that it is the package in which the external library is defined.
 
 ### Custom Targets
 
@@ -280,7 +280,7 @@ target «target-name» (pkg : NPackage _package.name) : α :=
   -- a build function that produces a `BuildJob α`
 ```
 
-The `pkg` parameter and its type specifier are optional and the body should be a term of type `IndexBuildM (BuildJob α)`. The `pkg` parameter is of type `NPackage _package.name` to provably demonstrate that it is the package in which the target is defined.
+The `pkg` parameter and its type specifier are optional and the body should be a term of type `FetchM (BuildJob α)`. The `pkg` parameter is of type `NPackage _package.name` to provably demonstrate that it is the package in which the target is defined.
 
 ## Defining New Facets
 
@@ -299,7 +299,7 @@ library_facet «facet-name» (lib : LeanLib) : α :=
   -- a build function that produces a `BuildJob α`
 ```
 
-In all of these, the object parameter and its type specifier are optional and the body should be a term of type `IndexBuildM (BuildJob α)`.
+In all of these, the object parameter and its type specifier are optional and the body should be a term of type `FetchM (BuildJob α)`.
 
 ## Adding Dependencies
 

src/lake/examples/ffi/lib/lakefile.lean

@@ -8,17 +8,16 @@ package ffi {
 
 lean_lib FFI
 
-@[default_target] lean_exe test {
+@[default_target] lean_exe test where
   root := `Main
-}
 
 target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
   let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString]
-  buildO "ffi.cpp" oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
+  buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
 
 extern_lib libleanffi pkg := do
+  let ffiO ← ffi.o.fetch
   let name := nameToStaticLib "leanffi"
-  let ffiO ← fetch <| pkg.target ``ffi.o
   buildStaticLib (pkg.nativeLibDir / name) #[ffiO]

src/lake/examples/targets/lakefile.lean

@@ -30,9 +30,9 @@ target caw pkg : Unit := do
   IO.FS.writeFile (pkg.buildDir / "caw.txt") "Caw!"
   return .nil
 
-target bark : Unit := do
+target bark : Unit := Job.async do
   logInfo "Bark!"
-  return .nil
+  return ((), .nil)
 
 target bark_bark : Unit := do
   bark.fetch

src/lake/examples/targets/test.sh

@@ -23,9 +23,9 @@ fi
 $LAKE build targets:noexistent && false || true
 
 # Test custom targets and package, library, and module facets
-$LAKE build bark | grep Bark!
-$LAKE build targets/bark_bark | grep Bark!
-$LAKE build targets:print_name | grep targets
+$LAKE build bark | tee /dev/stderr | awk '/bark/,/Bark!/' | wc -l | grep -q 2
+$LAKE build targets/bark_bark | tee /dev/stderr | awk '/bark/,/bark_bark/' | wc -l | grep -q 3
+$LAKE build targets:print_name | tee /dev/stderr | awk '/targets/,/print_name/' | wc -l | grep -q 2
 $LAKE build Foo.Bar:print_src | grep Bar.lean
 $LAKE build Foo:print_name | grep Foo
 

src/lake/tests/buildArgs/expected.out

@@ -1,11 +0,0 @@
-# lean args
-[0/1] Building Hello
-# weak lean args
-# compile args
-[1/2] Compiling Hello
-# weak compile args
-# link args
-[2/3] Linking Hello
-[2/3] Linking Hello
-[4/4] Linking hello
-# weak link args

src/lake/tests/buildArgs/test.sh

@@ -17,38 +17,25 @@ fi
 
 ${LAKE} build +Hello -R
 # see https://github.com/leanprover/lake/issues/50
-echo "# lean args" > produced.out
-${LAKE} build +Hello -R -KleanArgs=-DwarningAsError=true | tee -a produced.out
+${LAKE} build +Hello -R -KleanArgs=-DwarningAsError=true -v | grep --color warningAsError
 
 ${LAKE} build +Hello -R
 # see https://github.com/leanprover/lake/issues/172
-echo "# weak lean args" >> produced.out
-${LAKE} build +Hello -R -KweakLeanArgs=-DwarningAsError=true | tee -a produced.out
+${LAKE} build +Hello -R -KweakLeanArgs=-DwarningAsError=true --no-build
 
 ${LAKE} build +Hello:o -R
-echo "# compile args" >> produced.out
-# Use `head -n1` to avoid extraneous warnings on Windows with current Lean (8/1/23)
-${LAKE} build +Hello:o -R -KleancArgs=-DBAR | head -n1 | tee -a produced.out
+${LAKE} build +Hello:o -R -KleancArgs=-DBAR -v | grep --color leanc
 
 ${LAKE} build +Hello:o -R
-echo "# weak compile args" >> produced.out
-${LAKE} build +Hello:o -R -KweakLeancArgs=-DBAR | tee -a produced.out
+${LAKE} build +Hello:o -R -KweakLeancArgs=-DBAR --no-build
 
 ${LAKE} build +Hello:dynlib Hello:shared hello -R
-echo "# link args" >> produced.out
-# Use `head -n1` to avoid extraneous warnings on MacOS with current Lean (6/8/23)
-${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out
-${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out
-${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out
+${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
+${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
+${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
 
 ${LAKE} build +Hello:dynlib Hello:shared hello  -R
-echo "# weak link args" >> produced.out
-${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out
-${LAKE} build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out
-${LAKE} build hello -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out
-
-# check output against the expected output
-sed_i 's/lib//g' produced.out # remove lib prefixes
-sed_i 's/\..*//g' produced.out # remove extensions
-diff --strip-trailing-cr expected.out produced.out
+${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib  --no-build
+${LAKE} build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib  --no-build
+${LAKE} build hello -R -KweakLinkArgs=-L.lake/build/lib  --no-build
 

src/lake/tests/clone/test.sh

@@ -17,6 +17,7 @@ fi
 mkdir hello
 pushd hello
 $LAKE init hello
+$LAKE update
 git checkout -b master
 git config user.name test
 git config user.email test@example.com
@@ -29,10 +30,10 @@ HELLO_MAP="{\"hello\" : \"file://$(pwd)/hello\"}"
 cd test
 
 # test that `LAKE_PKG_URL_MAP` properly overwrites the config-specified Git URL
-LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | grep "file://"
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep "file://"
 # test that a second `lake update` is a no-op (with URLs)
 # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
-LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | diff - /dev/null
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | diff - /dev/null
 rm -rf .lake/packages
 
 # Test that Lake produces no warnings on a `lake build` after a `lake update`
@@ -40,7 +41,7 @@ rm -rf .lake/packages
 
 $LAKE update
 # test that a second `lake update` is a no-op (with file paths)
-$LAKE update | diff - /dev/null
+$LAKE update 2>&1 | diff - /dev/null
 test -d .lake/packages/hello
 # test that Lake produces no warnings
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
@@ -50,7 +51,7 @@ $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
 # See https://github.com/leanprover/lake/issues/167
 
 sed_i "s/world/changes/" .lake/packages/hello/Hello/Basic.lean
-! git -C .lake/packages/hello diff --exit-code
+git -C .lake/packages/hello diff --exit-code && false || true
 $LAKE build 3>&1 1>&2 2>&3 | grep "has local changes"
 ./.lake/build/bin/test | grep "Hello, changes"
 git -C .lake/packages/hello reset --hard

src/lake/tests/lock/Wait.lean

@@ -1,4 +1,4 @@
-import Lake.Build.Monad
+import Lake.Build.Run
 
 partial def busyWaitFile (file : System.FilePath) : BaseIO PUnit := do
   if (← file.pathExists) then

src/lake/tests/postUpdate/dep/lakefile.lean

@@ -9,7 +9,7 @@ post_update pkg do
   let wsToolchainFile := (← getRootPackage).dir / "toolchain"
   let depToolchain ← IO.FS.readFile <| pkg.dir / "toolchain"
   IO.FS.writeFile wsToolchainFile depToolchain
-  let exeFile ← runBuild hello.build >>= (·.await)
+  let exeFile ← runBuild hello.fetch
   let exitCode ← env exeFile.toString #["get"]
   if exitCode ≠ 0 then
     error s!"{pkg.name}: failed to fetch hello"

src/lake/tests/wfail/Warn.lean

@@ -0,0 +1,3 @@
+import Lean.Elab.Command
+
+run_cmd Lean.logWarning "bar"

src/lake/tests/wfail/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/wfail/lakefile.lean

@@ -0,0 +1,17 @@
+import Lake
+open Lake DSL
+
+package test
+
+lean_lib Warn
+
+target warn : PUnit := Job.async do
+  logWarning "foo"
+  return ((), .nil)
+
+target warnArt pkg : PUnit := Job.async do
+  let warnArtFile := pkg.buildDir / "warn_art"
+  (((), ·)) <$> buildFileUnlessUpToDate warnArtFile .nil do
+    logWarning "foo-file"
+    createParentDirs warnArtFile
+    IO.FS.writeFile warnArtFile ""

src/lake/tests/wfail/test.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# Test Lake warnings produce build failures with `--wfail`
+
+$LAKE build warn | grep --color foo
+$LAKE build warn | grep --color foo # test idempotent
+$LAKE build warn --wfail && exit 1 || true
+
+$LAKE build warnArt | grep --color foo-file
+$LAKE build warnArt | grep --color foo-file # test `buildFileUpToDate` cache
+$LAKE build warnArt --wfail && exit 1 || true
+
+# Test Lean warnings produce build failures with `--wfail`
+
+$LAKE build Warn | grep --color bar
+$LAKE build Warn | grep --color bar # test Lean module build log cache
+$LAKE build Warn --wfail && exit 1 || true

tests/pkg/prv/test.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 
 rm -rf .lake/build
-lake build 2>&1 | grep 'error: field.*private'
+lake build 2>&1 | grep 'error: .*: field.*private'

tests/pkg/test_extern/expected.txt

@@ -1,5 +1,4 @@
-error: stdout:
-././././TestExtern.lean:5:0: error: native implementation did not agree with reference implementation!
+error: ././././TestExtern.lean:5:0-5:27: native implementation did not agree with reference implementation!
 Compare the outputs of:
 #eval Nat.not_add 4 5
  and

tests/pkg/test_extern/test.sh

@@ -14,8 +14,8 @@ rm -rf .lake/build
 verify_output() {
     # Normalize path separators from backslashes to forward slashes
     sed 's#\\#/#g' |
-    awk '/error: stdout:/, /error: external command/' |
-    sed '/error: external command/d'
+    awk '/error: .*lean:/, /error: Lean exited/' |
+    sed '/error: Lean exited/d'
 }
 
 lake build 2>&1 | verify_output > produced.txt