max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: show stdout by default

Browse source
This commit is contained in:
Gabriel Ebner 2023-03-11 00:56:15 +00:00 • committed by Mac
parent 421e73f6c5
commit 276bf837e2
3 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Build/Actions.lean
View file

@ -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]
}

4
Lake/Util/Git.lean
View file

@ -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"]

17
Lake/Util/Proc.lean
View file

@ -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}"