refactor: cleanup logging API (unify BuildIO with LogIO)

Author: tydeu

Diff for: Lake/Build/Actions.lean

@@ -5,41 +5,21 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Build.Job
 import Lake.Config.Env
+import Lake.Util.Proc
 
 namespace Lake
 open System
 
 def createParentDirs (path : FilePath) : IO Unit := do
   if let some dir := path.parent then IO.FS.createDirAll dir
 
-def proc (args : IO.Process.SpawnArgs) : BuildIO Unit := do
-  let envStr := String.join <| args.env.toList.filterMap fun (k, v) =>
-    if k == "PATH" then none else some s!"{k}={v.getD ""} " -- PATH too big
-  let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
-  logVerbose <| "> " ++ envStr ++
-    match args.cwd with
-    | some cwd => s!"{cmdStr}    # in directory {cwd}"
-    | none     => cmdStr
-  let out ← IO.Process.output args
-  let logOutputWith (log : String → BuildIO PUnit) := do
-    unless out.stdout.isEmpty do
-      log s!"stdout:\n{out.stdout}"
-    unless out.stderr.isEmpty do
-      log s!"stderr:\n{out.stderr}"
-  if out.exitCode = 0 then
-    logOutputWith logInfo
-  else
-    logOutputWith logError
-    logError s!"external command {args.cmd} exited with status {out.exitCode}"
-    failure
-
 def compileLeanModule (name : String) (leanFile : FilePath)
 (oleanFile? ileanFile? cFile? : Option FilePath)
 (leanPath : SearchPath := []) (rootDir : FilePath := ".")
 (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
 (leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: BuildIO PUnit := do
-  logAuxInfo s!"Building {name}"
+: LogIO PUnit := do
+  logInfo s!"Building {name}"
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -63,44 +43,44 @@ def compileLeanModule (name : String) (leanFile : FilePath)
   }
 
 def compileO (name : String) (oFile srcFile : FilePath)
-(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildIO Unit := do
-  logAuxInfo s!"Compiling {name}"
+(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : LogIO Unit := do
+  logInfo s!"Compiling {name}"
   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") : BuildIO Unit := do
-  logAuxInfo s!"Linking {name}"
+(oFiles : Array FilePath) (ar : FilePath := "ar") : LogIO Unit := do
+  logInfo s!"Linking {name}"
   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") : BuildIO Unit := do
-  logAuxInfo s!"Linking {name}"
+(linkArgs : Array String) (linker : FilePath := "cc") : LogIO Unit := do
+  logInfo s!"Linking {name}"
   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") : BuildIO Unit := do
-  logAuxInfo s!"Linking {name}"
+(linkArgs : Array String := #[]) (linker : FilePath := "cc") : LogIO Unit := do
+  logInfo s!"Linking {name}"
   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) : BuildIO PUnit := do
-  logAuxInfo s!"Downloading {name}"
+def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do
+  logInfo s!"Downloading {name}"
   if (← file.pathExists) then
     IO.FS.removeFile file
   else
@@ -113,8 +93,8 @@ def download (name : String) (url : String) (file : FilePath) : BuildIO PUnit :=
   }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
-def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : BuildIO PUnit := do
-  logAuxInfo s!"Unpacking {name}"
+def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
+  logInfo s!"Unpacking {name}"
   let mut opts := "-x"
   if (← getIsVerbose) then
     opts := opts.push 'v'
@@ -127,8 +107,8 @@ def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : Bu
 
 /-- Pack a directory `dir` using `tar` into the archive `file`. -/
 def tar (name : String) (dir : FilePath) (file : FilePath)
-(gzip := true) (excludePaths : Array FilePath := #[]) : BuildIO PUnit := do
-  logAuxInfo s!"Packing {name}"
+(gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do
+  logInfo s!"Packing {name}"
   createParentDirs file
   let mut args := #["-c"]
   if gzip then

Diff for: Lake/Build/Context.lean

@@ -25,11 +25,8 @@ abbrev BuildT := ReaderT BuildContext
 /-- The monad for the Lake build manager. -/
 abbrev SchedulerM := BuildT <| LogT BaseIO
 
-/-- The base IO monad for Lake builds. -/
-abbrev BuildIO := MonadLogT BaseIO OptionIO
-
 /-- The core monad for Lake builds. -/
-abbrev BuildM := BuildT BuildIO
+abbrev BuildM := BuildT LogIO
 
 /-- A transformer to equip a monad with a Lake build store. -/
 abbrev BuildStoreT := StateT BuildStore
@@ -43,15 +40,9 @@ abbrev BuildCycleT := CycleT BuildKey
 /-- A recursive build of a Lake build store that may encounter a cycle. -/
 abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
 
-instance : MonadError BuildIO := ⟨MonadLog.error⟩
-instance : MonadLift IO BuildIO := ⟨MonadError.runIO⟩
-
 instance [Pure m] : MonadLift LakeM (BuildT m) where
   monadLift x := fun ctx => pure <| x.run ctx.toContext
 
-instance : MonadLift LogIO BuildIO where
-  monadLift x := fun meths => liftM (n := BuildIO) (x.run meths.lift) meths
-
 def BuildM.run (logMethods : MonadLog BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α :=
   self ctx logMethods |>.toIO fun _ => IO.userError "build failed"
 

Diff for: Lake/Build/Trace.lean

@@ -171,8 +171,8 @@ def getFileMTime (file : FilePath) : IO MTime :=
 instance : GetMTime FilePath := ⟨getFileMTime⟩
 
 /-- Check if the info's `MTIme` is at least `depMTime`. -/
-def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : IO Bool := do
-  try pure ((← getMTime info) >= depMTime) catch _ => pure false
+def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
+  (do pure ((← getMTime info) >= depMTime : Bool)).catchExceptions fun _ => pure false
 
 --------------------------------------------------------------------------------
 /-! # Lake Build Trace (Hash + MTIme) -/

Diff for: Lake/CLI/Init.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Git
+import Lake.Util.Sugar
 import Lake.Config.Package
 import Lake.Config.Workspace
 import Lake.Load.Config
@@ -176,7 +177,7 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit
       repo.quietInit
       unless upstreamBranch = "master" do
         repo.checkoutBranch upstreamBranch
-    catch _ =>
+    else
       logWarning "failed to initialize git repository"
 
 def init (pkgName : String) (tmp : InitTemplate) : LogIO PUnit :=

Diff for: Lake/CLI/Main.lean

@@ -203,7 +203,7 @@ def serve (config : LoadConfig) (args : Array String) : LogIO UInt32 := do
       let ws ← loadWorkspace config
       let ctx := mkLakeContext ws
       pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
-    catch _ =>
+    else
       logWarning "package configuration has errors, falling back to plain `lean --server`"
       pure (config.env.installVars.push (invalidConfigEnvVar, "1"), #[])
   (← IO.Process.spawn {
@@ -221,14 +221,14 @@ def exe (name : Name) (args  : Array String := #[]) (verbosity : Verbosity) : La
   else
     error s!"unknown executable `{name}`"
 
-def uploadRelease (pkg : Package) (tag : String) : BuildIO Unit := do
+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
     (excludePaths := #["*.tar.gz", "*.tar.gz.trace"])
-  logAuxInfo s!"Uploading {tag}/{pkg.buildArchive}"
+  logInfo s!"Uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
 
 def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError (Package × String) :=

Diff for: Lake/Load/Main.lean

@@ -111,7 +111,7 @@ def resolveDeps (ws : Workspace) (pkg : Package) (shouldUpdate := true) : LogIO
           log := log ++ s!"`{name}` locked `{inputRev}` at `{contrib.rev}`\n"
         let inputRev := entry.inputRev?.getD Git.upstreamBranch
         log := log ++  s!"Using `{inputRev}` at `{entry.rev}`"
-        logVerbose log
+        logInfo log
     manifest.saveToFile ws.manifestFile
   return pkg
 

Diff for: Lake/Util/Error.lean

@@ -36,5 +36,6 @@ protected def MonadError.runEIO [Monad m]
 Perform an IO action.
 If it throws an error, invoke `error` with its string representation.
 -/
-protected def MonadError.runIO [Monad m] [MonadError m] [MonadLiftT BaseIO m] (x : IO α) : m α :=
+@[inline] protected def MonadError.runIO
+[Monad m] [MonadError m] [MonadLiftT BaseIO m] (x : IO α) : m α :=
   MonadError.runEIO x

Diff for: Lake/Util/Git.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lake.Util.Log
+import Lake.Util.Proc
 import Lake.Util.Lift
 
 open System
@@ -33,37 +33,6 @@ def filterUrl? (url : String) : Option String :=
 def isFullObjectName (rev : String) : Bool :=
   rev.length == 40 && rev.all fun c => c.isDigit || ('a' <= c && c <= 'f')
 
-def capture (args : Array String) (wd : Option FilePath := none) : LogIO String := do
-  let out ← IO.Process.output {cmd := "git", args, cwd := wd}
-  if out.exitCode != 0 then
-    let mut log := s!"\n> git {" ".intercalate args.toList}\n"
-    unless out.stdout.isEmpty do
-      log := log ++ s!"stdout:\n{out.stdout.trim}\n"
-    unless out.stderr.isEmpty do
-      log := log ++ s!"stderr:\n{out.stderr.trim}\n"
-    logError log.trim
-    error <| "git exited with code " ++ toString out.exitCode
-  return out.stdout.trim -- remove, e.g., newline at end
-
-def capture? (args : Array String) (wd : Option FilePath := none) : BaseIO (Option String) := do
-  EIO.catchExceptions (h := fun _ => pure none) do
-    let out ← IO.Process.output {cmd := "git", args, cwd := wd}
-    if out.exitCode = 0 then
-      return some out.stdout.trim -- remove, e.g., newline at end
-    else
-      return none
-
-def exec (args : Array String) (wd : Option FilePath := none) : LogIO PUnit := do
-  discard <| capture args wd
-
-def test (args : Array String) (wd : Option FilePath := none) : BaseIO Bool :=
-  EIO.catchExceptions (h := fun _ => pure false) do
-    let child ← IO.Process.spawn {
-      cmd := "git", args, cwd := wd,
-      stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null
-    }
-    return (← child.wait) == 0
-
 end Git
 
 structure GitRepo where
@@ -75,43 +44,43 @@ namespace GitRepo
 
 def cwd : GitRepo := ⟨"."⟩
 
-def dirExists (repo : GitRepo) : BaseIO Bool :=
+@[inline] def dirExists (repo : GitRepo) : BaseIO Bool :=
   repo.dir.isDir
 
-def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
-  Git.capture args repo.dir
+@[inline] def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
+  captureProc {cmd := "git", args, cwd := repo.dir}
 
-def captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String) :=
-  Git.capture? args repo.dir
+@[inline] def captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String) :=
+  captureProc? {cmd := "git", args, cwd := repo.dir}
 
-def execGit (args : Array String) (repo : GitRepo) : LogIO PUnit :=
-  Git.exec args repo.dir
+@[inline] def execGit (args : Array String) (repo : GitRepo) : LogIO PUnit :=
+  proc {cmd := "git", args, cwd := repo.dir}
 
-def testGit (args : Array String) (repo : GitRepo) : BaseIO Bool :=
-  Git.test args repo.dir
+@[inline] def testGit (args : Array String) (repo : GitRepo) : BaseIO Bool :=
+  testProc {cmd := "git", args, cwd := repo.dir}
 
-def clone (url : String) (repo : GitRepo) : LogIO PUnit  :=
-  Git.exec #["clone", url, repo.dir.toString]
+@[inline] def clone (url : String) (repo : GitRepo) : LogIO PUnit  :=
+  proc {cmd := "git", args := #["clone", url, repo.dir.toString]}
 
-def quietInit (repo : GitRepo) : LogIO PUnit  :=
+@[inline] def quietInit (repo : GitRepo) : LogIO PUnit  :=
   repo.execGit #["init", "-q"]
 
-def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit  :=
+@[inline] def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit  :=
   repo.execGit #["fetch", remote]
 
-def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
+@[inline] def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
   repo.execGit #["checkout", "-B", branch]
 
-def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit  :=
+@[inline] def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit  :=
   repo.execGit #["checkout", "--detach", hash]
 
-def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
+@[inline] def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
   repo.captureGit? #["rev-parse", "--verify", rev]
 
-def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
+@[inline] def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
   repo.captureGit #["rev-parse", "--verify", rev]
 
-def headRevision (repo : GitRepo) : LogIO String :=
+@[inline] def headRevision (repo : GitRepo) : LogIO String :=
   repo.resolveRevision "HEAD"
 
 def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
@@ -123,16 +92,16 @@ def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : G
 def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote := Git.defaultRemote) : LogIO String := do
   repo.fetch remote; repo.resolveRemoteRevision (rev?.getD Git.upstreamBranch) remote
 
-def branchExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
+@[inline] def branchExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
   repo.testGit #["show-ref", "--verify", s!"refs/heads/{rev}"]
 
-def revisionExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
+@[inline] def revisionExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
   repo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"]
 
-def findTag? (rev : String := "HEAD") (repo : GitRepo) : BaseIO (Option String) := do
+@[inline] def findTag? (rev : String := "HEAD") (repo : GitRepo) : BaseIO (Option String) := do
   repo.captureGit? #["describe", "--tags", "--exact-match", rev]
 
-def getRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String) := do
+@[inline] def getRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String) := do
   repo.captureGit? #["remote", "get-url", remote]
 
 def getFilteredRemoteUrl? (remote := Git.defaultRemote) (repo : GitRepo) : BaseIO (Option String) := OptionT.run do

Diff for: Lake/Util/Lift.lean

@@ -3,6 +3,7 @@ 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
 
@@ -33,3 +34,6 @@ 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