From 276bf837e284a4cf26522e6b232e59235d120f1b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 11 Mar 2023 00:56:15 +0000
Subject: [PATCH] feat: show stdout by default

---
 Lake/Build/Actions.lean |  2 +-
 Lake/Util/Git.lean      |  4 ++--
 Lake/Util/Proc.lean     | 17 +++++++++++++----
 3 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean
index c45a7cb940..28d60f7dab 100644
--- a/Lake/Build/Actions.lean
+++ b/Lake/Build/Actions.lean
@@ -86,7 +86,7 @@ def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := d
     createParentDirs file
   let args :=
     if (← getIsVerbose) then #[] else #["-s"]
-  proc {
+  proc (quiet := true) {
     cmd := "curl"
     args := args ++ #["-f", "-o", file.toString, "-L", url]
   }
diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean
index 0a6e3f46c1..5868a27d24 100644
--- a/Lake/Util/Git.lean
+++ b/Lake/Util/Git.lean
@@ -54,13 +54,13 @@ def cwd : GitRepo := ⟨"."⟩
   captureProc? {cmd := "git", args, cwd := repo.dir}
 
 @[inline] def execGit (args : Array String) (repo : GitRepo) : LogIO PUnit :=
-  proc {cmd := "git", args, cwd := repo.dir}
+  proc {cmd := "git", args, cwd := repo.dir} (quiet := true)
 
 @[inline] def testGit (args : Array String) (repo : GitRepo) : BaseIO Bool :=
   testProc {cmd := "git", args, cwd := repo.dir}
 
 @[inline] def clone (url : String) (repo : GitRepo) : LogIO PUnit  :=
-  proc {cmd := "git", args := #["clone", url, repo.dir.toString]}
+  proc {cmd := "git", args := #["clone", url, repo.dir.toString]} (quiet := true)
 
 @[inline] def quietInit (repo : GitRepo) : LogIO PUnit  :=
   repo.execGit #["init", "-q"]
diff --git a/Lake/Util/Proc.lean b/Lake/Util/Proc.lean
index 69898917ee..01239c7c53 100644
--- a/Lake/Util/Proc.lean
+++ b/Lake/Util/Proc.lean
@@ -7,8 +7,8 @@ import Lake.Util.Log
 
 namespace Lake
 
-@[specialize] def logProcWith [Monad m]
-(args : IO.Process.SpawnArgs) (out : IO.Process.Output)  (log : String → m PUnit) : m Unit := do
+@[specialize] def logProcCmd [Monad m]
+(args : IO.Process.SpawnArgs) (log : String → m PUnit) : m Unit := do
   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)
@@ -16,16 +16,25 @@ namespace Lake
     match args.cwd with
     | some cwd => s!"{cmdStr}    # in directory {cwd}"
     | none     => cmdStr
+
+@[specialize] def logProcOutput [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}"
 
-def proc (args : IO.Process.SpawnArgs) : LogIO Unit := do
+@[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
+
+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
+      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}"