From b2acab81d4e0391eeb1915ccbd890a4b4762acad Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 4 Oct 2021 12:25:50 -0400 Subject: [PATCH] refactor: output `print-paths` build info to stderr --- Lake/BuildBin.lean | 4 ++-- Lake/BuildMonad.lean | 26 +++++++++++++++++++------- Lake/BuildPackage.lean | 4 ++-- 3 files changed, 23 insertions(+), 11 deletions(-) diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 1033d22646..6cbcc6d5b1 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -32,7 +32,7 @@ def Package.staticLibTarget (self : Package) : FileTarget := (← self.buildTarget).staticLibTarget.materializeAsync def buildLib (pkg : Package) : IO PUnit := - pkg.staticLibTarget.build.run + pkg.staticLibTarget.build.run' -- # Build Package Bin @@ -52,4 +52,4 @@ def Package.binTarget (self : Package) : FileTarget := pkgTarget.binTarget depTargets >>= (·.materializeAsync) def buildBin (pkg : Package) : IO PUnit := - pkg.binTarget.build.run + pkg.binTarget.build.run' diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index 064d2ef0fd..efb0c1bbf4 100644 --- a/Lake/BuildMonad.lean +++ b/Lake/BuildMonad.lean @@ -62,6 +62,12 @@ def io : BuildContext where logError := fun msg => IO.eprintln msg } +def ioErr : BuildContext where + methodsRef := BuildMethodsRef.mk { + logInfo := fun msg => IO.eprintln msg + logError := fun msg => IO.eprintln msg + } + def methods (self : BuildContext) : BuildMethods := self.methodsRef.get @@ -78,11 +84,8 @@ def logInfo (msg : String) : BuildM PUnit := do def logError (msg : String) : BuildM PUnit := do (← getMethods).logError msg -def runIn (ctx : BuildContext) (self : BuildM α) : IO α := - self ctx - -def run' (self : BuildM α) : IO α := - runIn BuildContext.io do try self catch e => +def convErrors (self : BuildM α) : BuildM α := do + try self catch e => /- Remark: Actual error should have already been logged earlier. However, if the error was thrown by something that did not know it was @@ -93,8 +96,17 @@ def run' (self : BuildM α) : IO α := BuildM.logError s!"build error: {toString e}" throw <| IO.userError "build failed" -def run (self : BuildM α) : IO PUnit := - discard self.run' +def runIn (ctx : BuildContext) (self : BuildM α) : IO α := + self ctx + +def run (self : BuildM α) : IO α := + (convErrors self).runIn BuildContext.io + +def runErr (self : BuildM α) : IO α := + (convErrors self).runIn BuildContext.ioErr + +def run' (self : BuildM α) : IO PUnit := + discard self.run end BuildM diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index fe30fa7d3b..4bed0bbac1 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -146,7 +146,7 @@ def Package.buildDeps (self : Package) : BuildM (Array Package) := do targets.mapM fun target => Functor.mapConst target.info.1 target.materialize def configure (pkg : Package) : IO Unit := - pkg.buildDeps.run + pkg.buildDeps.run' def Package.build (self : Package) : BuildM PUnit := do let depTargets ← self.buildDepTargets @@ -170,7 +170,7 @@ def Package.filterLocalImports (imports : List String) (self : Package) : Array return localImports def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do - let deps ← BuildM.run' do + let deps ← BuildM.runErr do -- resolve and build deps let depTargets ← pkg.buildDepTargets let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) []