refactor: lake: track logs instead of eagerly printing them

src/lake/Lake/Build.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.Build.Run
 import Lake.Build.Actions
 import Lake.Build.Index
 import Lake.Build.Module

src/lake/Lake/Build/Actions.lean

@@ -8,19 +8,20 @@ import Lake.Util.NativeLib
 import Lake.Build.Context
 
 /-! # 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
 
-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}"
+def compileLeanModule
+  (name : Name) (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
+  logVerbose s!"building Lean module {name}"
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -46,83 +47,80 @@ def compileLeanModule (name : String) (leanFile : FilePath)
     ]
   }
 
-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
     args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
   }
 
 /-- 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 := "-xv"
   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 := #["-v", "-c"]
   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/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
@@ -24,8 +24,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,8 +38,10 @@ 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
@@ -51,12 +55,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
+@[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
@@ -84,8 +90,9 @@ the `.hash` file using `fetchFileTrace`.
 By example, for `file := "foo.c"`, compare `depTrace` with that in `foo.c.trace`
 and cache the hash using `foo.c.hash`.
 -/
-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
     fetchFileTrace file
@@ -101,23 +108,26 @@ 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)
+: SchedulerM (BuildJob FilePath) :=
   dep.bindSync fun depInfo depTrace => do
     let depTrace := depTrace.mix (← extraDepTrace)
     let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo
     return (file, trace)
 
 /-- 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)
+: SchedulerM (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)
+: SchedulerM (BuildJob FilePath) := do
   buildFileAfterDep file (← BuildJob.collectArray deps) build extraDepTrace
 
 /-! ## Common Builds -/
@@ -141,54 +151,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)
+: SchedulerM (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 := #[])
+: SchedulerM (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))
+: SchedulerM (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 := #[])
+: SchedulerM (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 := #[])
+: SchedulerM (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 := #[])
+: SchedulerM (BuildJob FilePath) :=
   staticLibJob.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let baseArgs :=
@@ -200,13 +214,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) : SchedulerM (BuildJob Dynlib) :=
   sharedLibTarget.bindSync fun sharedLib trace => do
     if let some stem := sharedLib.fileStem then
       if Platform.isWindows then

src/lake/Lake/Build/Context.lean

@@ -25,12 +25,21 @@ structure BuildConfig where
   trustHash : Bool := true
   /-- Early exit if a target has to be rebuilt. -/
   noBuild : Bool := false
+  verbosity : Verbosity := .normal
+
+abbrev LogIOTask α :=
+  BaseIOTask (EResult Nat Log α)
+
+abbrev JobTask α := LogIOTask α
+
+/-- 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
+  buildJobs : IO.Ref (Array (String × Job Unit))
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
@@ -56,6 +65,9 @@ abbrev SchedulerM := BuildT <| LogT BaseIO
 /-- The core monad for Lake builds. -/
 abbrev BuildM := BuildT LogIO
 
+/-- The monad of Lake jobs. -/
+abbrev JobM := BuildM
+
 /-- A transformer to equip a monad with a Lake build store. -/
 abbrev BuildStoreT := StateT BuildStore
 
@@ -74,13 +86,5 @@ instance [Pure m] : MonadLift LakeM (BuildT m) where
 @[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