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

refactor: pipe proc output to logger

Browse source
This commit is contained in:
tydeu 2021-11-02 07:03:48 -04:00
parent 182409e0f4
commit 763ac9a2e8
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
Lake/Compile.lean
View file

@ -8,7 +8,7 @@ import Lake.BuildMonad
namespace Lake
open System
def createParentDirs (path : FilePath) : BuildM PUnit := do
def createParentDirs (path : FilePath) : IO PUnit := do
if let some dir := path.parent then IO.FS.createDirAll dir
def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
@ -18,10 +18,13 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
match args.cwd with
| some cwd => s!"{cmdStr} # in directory {cwd}"
| none => cmdStr
let child ← IO.Process.spawn args
let exitCode ← child.wait
if exitCode != 0 then -- log errors early
logError s!"external command {args.cmd} exited with status {exitCode}"
let out ← IO.Process.output args
unless out.stdout.isEmpty do
logInfo out.stdout
unless out.stderr.isEmpty do
logError out.stderr
if out.exitCode != 0 then
logError s!"external command {args.cmd} exited with status {out.exitCode}"
failure
def compileOlean (leanFile oleanFile : FilePath)