refactor: properly manage errors in the build monad

Lake/BuildMonad.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Task
 import Lake.Trace
+import Lake.RealM
 import Lake.LogMonad
 import Lake.InstallPath
 
@@ -21,7 +22,8 @@ structure BuildContext where
   lakeInstall : LakeInstall
   deriving Inhabited
 
-abbrev BuildM := ReaderT BuildContext <| LogT <| IO
+abbrev BuildCoreM := LogT <| EIO PUnit
+abbrev BuildM := ReaderT BuildContext BuildCoreM
 
 --------------------------------------------------------------------------------
 -- # Build Monad Utilities
@@ -45,31 +47,80 @@ def getLeanc : BuildM FilePath :=
 def getLakeInstall : BuildM LakeInstall :=
   (·.lakeInstall) <$> read
 
-namespace BuildM
+namespace BuildCoreM
 
-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
-      in `BuildM` (e.g., a general `Target`), it may have not been.
+def run (logMethods : LogMethods (EIO PUnit)) (self : BuildCoreM α) : IO α :=
+  ReaderT.run self logMethods |>.toIO fun _ => IO.userError "build failed"
 
-      TODO: Use an `OptionT` in `BuildM` to properly record build failures.
-    -/
-    logError s!"build error: {toString e}"
-    throw <| IO.userError "build failed"
+def runWith (logMethods : LogMethods (EIO PUnit)) (self : BuildCoreM α) : EIO PUnit α :=
+  ReaderT.run self logMethods
 
-def run (logMethods : LogMethods IO) (ctx : BuildContext) (self : BuildM α) : IO α :=
-  (convErrors self) ctx logMethods
+protected def failure : BuildCoreM α :=
+  throw ()
 
-end BuildM
+protected def orElse (self : BuildCoreM α) (f : Unit → BuildCoreM α) : BuildCoreM α :=
+  tryCatch self f
+
+instance : Alternative BuildCoreM where
+  failure := BuildCoreM.failure
+  orElse := BuildCoreM.orElse
+
+def runIO (x : IO α) : BuildCoreM α := do
+  match (← RealM.runIO' x) with
+  | Except.ok a => pure a
+  | Except.error e => do
+    logError (toString e)
+    failure
+
+instance : MonadLift IO BuildCoreM := ⟨runIO⟩
+
+end BuildCoreM
+
+def BuildM.run (logMethods : LogMethods (EIO PUnit)) (ctx : BuildContext) (self : BuildM α) : IO α :=
+  self ctx |>.run logMethods
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
 | Except.ok a => a
 | Except.error cycle => do
   let cycle := cycle.map (s!"  {·}")
-  let msg := s!"build cycle detected:\n{"\n".intercalate cycle}"
-  logError msg
-  throw <| IO.userError msg
+  logError s!"build cycle detected:\n{"\n".intercalate cycle}"
+  failure
 
+/-- TODO: Replace with an `EIOTask PUnit` once Lean supports such a thing. -/
 abbrev BuildTask := IOTask
+
+namespace BuildTask
+
+def spawn (act : BuildCoreM α) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask α) :=
+  fun meths => BuildCoreM.runWith meths do IO.asTask (act.run meths) prio
+
+instance : Async BuildCoreM BuildTask := ⟨spawn⟩
+
+protected def await (self : BuildTask α) : BuildCoreM α := do
+  match (← IO.wait self) with
+  | Except.ok a    => pure a
+  | Except.error e => logError (toString e); failure
+
+instance : Await BuildTask BuildCoreM := ⟨BuildTask.await⟩
+
+protected def mapAsync (f : α → BuildCoreM β) (self : BuildTask α) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) :=
+  fun meths => BuildCoreM.runWith meths do self.mapAsync (fun a => f a |>.run meths) prio
+
+instance : MapAsync BuildCoreM BuildTask := ⟨BuildTask.mapAsync⟩
+
+protected def bindAsync (self : BuildTask α) (f : α → BuildCoreM (BuildTask β)) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) :=
+  fun meths => BuildCoreM.runWith meths do self.bindAsync (fun a => f a |>.run meths) prio
+
+instance : BindAsync BuildCoreM BuildTask := ⟨BuildTask.bindAsync⟩
+
+protected def seqLeftAsync (self : BuildTask α) (act : BuildCoreM β) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask α) :=
+  fun meths => BuildCoreM.runWith meths do self.seqLeftAsync (act.run meths) prio
+
+instance : SeqLeftAsync BuildCoreM BuildTask := ⟨BuildTask.seqLeftAsync⟩
+
+protected def seqRightAsync (self : BuildTask α) (act : BuildCoreM β) (prio := Task.Priority.dedicated) : BuildCoreM (BuildTask β) :=
+  fun meths => BuildCoreM.runWith meths do self.seqRightAsync (act.run meths) prio
+
+instance : SeqRightAsync BuildCoreM BuildTask := ⟨BuildTask.seqRightAsync⟩
+
+end BuildTask

Lake/BuildTarget.lean

@@ -28,20 +28,6 @@ abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace
 /-- A `BuildTarget` that produces a file. -/
 abbrev FileTarget := BuildTarget FilePath
 
-namespace FileTarget
-
-variable [ComputeTrace FilePath m BuildTrace] [MonadLiftT m BuildM]
-
-def computeSync (path : FilePath) : FileTarget :=
-  Target.mk path do pure <$> try computeTrace path catch e =>
-    logError (toString e); throw e
-
-def computeAsync (path : FilePath) : FileTarget :=
-  Target.mk path do async <| try computeTrace path catch e =>
-    logError (toString e); throw e
-
-end FileTarget
-
 -- ## Active
 
 /-- An `ActiveBuildTarget` that produces a file. -/

Lake/BuildTargets.lean

@@ -11,7 +11,9 @@ namespace Lake
 
 -- # General Utilities
 
-def inputFileTarget := FileTarget.computeAsync
+def inputFileTarget (path : FilePath) : FileTarget :=
+  Target.computeAsync path
+
 instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩
 
 def buildFileUnlessUpToDate (file : FilePath)

Lake/Compile.lean

@@ -9,8 +9,7 @@ namespace Lake
 open System
 
 def createParentDirs (path : FilePath) : BuildM PUnit := do
-  if let some dir := path.parent then
-    try IO.FS.createDirAll dir catch e => logError (toString e)
+  if let some dir := path.parent then IO.FS.createDirAll dir
 
 def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
   let envStr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
@@ -21,10 +20,9 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
     | none     => cmdStr
   let child ← IO.Process.spawn args
   let exitCode ← child.wait
-  if exitCode != 0 then
-    let msg := s!"external command {args.cmd} exited with status {exitCode}"
-    logError msg -- log errors early
-    throw <| IO.userError msg
+  if exitCode != 0 then -- log errors early
+    logError s!"external command {args.cmd} exited with status {exitCode}"
+    failure
 
 def compileOlean (leanFile oleanFile : FilePath)
 (oleanDirs : List FilePath := [])  (rootDir : FilePath := ".")

Lake/LogMonad.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.RealM
+
 namespace Lake
 
 -- # Typeclass
@@ -33,15 +35,15 @@ def nop [Pure m] : LogMethods m :=
 
 instance [Pure m] : Inhabited (LogMethods m) := ⟨LogMethods.nop⟩
 
-def io : LogMethods IO where
-  logInfo msg := IO.println msg
-  logWarning msg := IO.eprintln s!"warning: {msg}"
-  logError msg := IO.eprintln s!"error: {msg}"
+def io [MonadLiftT RealM m] : LogMethods m where
+  logInfo msg := RealM.runIO_ <| IO.println msg
+  logWarning msg := RealM.runIO_ <| IO.eprintln s!"warning: {msg}"
+  logError msg := RealM.runIO_ <| IO.eprintln s!"error: {msg}"
 
-def eio : LogMethods IO where
-  logInfo msg := IO.eprintln s!"info: {msg}"
-  logWarning msg := IO.eprintln s!"warning: {msg}"
-  logError msg := IO.eprintln s!"error: {msg}"
+def eio [MonadLiftT RealM m] : LogMethods m where
+  logInfo msg := RealM.runIO_ <| IO.eprintln s!"info: {msg}"
+  logWarning msg := RealM.runIO_ <| IO.eprintln s!"warning: {msg}"
+  logError msg := RealM.runIO_ <| IO.eprintln s!"error: {msg}"
 
 end LogMethods
 
@@ -58,5 +60,15 @@ instance [Monad m] : MonadLog (LogT m) where
   logWarning msg := do (← read).logWarning msg
   logError msg := do (← read).logError msg
 
-def LogT.adaptMethods [Monad m] (f : LogMethods m → LogMethods m) (self : LogT m α) : LogT m α :=
+namespace LogT
+
+abbrev run (methods :  LogMethods m) (self : LogT m α) : m α :=
+  ReaderT.run self methods
+
+abbrev runWith (methods :  LogMethods m) (self : LogT m α) : m α :=
+  ReaderT.run self methods
+
+abbrev adaptMethods [Monad m] (f : LogMethods m → LogMethods m) (self : LogT m α) : LogT m α :=
   ReaderT.adapt f self
+
+end LogT

Lake/RealM.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+namespace Lake
+
+/-- An `IO`/`EIO` monad that can't error. -/
+def RealM := EIO Empty
+
+instance : Monad RealM := inferInstanceAs (Monad (EIO Empty))
+instance  [Inhabited α] : Inhabited (RealM α) := inferInstanceAs (Inhabited (EIO Empty α))
+
+namespace RealM
+
+abbrev run (self : RealM α) : EIO Empty α :=
+  self
+
+def toEIO (self : RealM α) : EIO ε α :=
+  fun s => match self s with
+  | EStateM.Result.ok a s => EStateM.Result.ok a s
+
+instance : MonadLift RealM (EIO ε) := ⟨toEIO⟩
+
+abbrev toIO (self : RealM α) : IO α :=
+  self.toEIO
+
+def runEIO (f : ε → RealM α) (x : EIO ε α) : RealM α :=
+  x.catchExceptions f
+
+abbrev runIO (f : IO.Error → RealM α) (x : IO α) : RealM α :=
+  runEIO f x
+
+def runEIO' (x : EIO ε α) : RealM (Except ε α) :=
+  fun s => match x s with
+  | EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s
+  | EStateM.Result.error e s => EStateM.Result.ok (Except.error e) s
+
+abbrev runIO' (x : IO α) : RealM (Except IO.Error α) :=
+  runEIO' x
+
+def runEIO_ (x : EIO ε α) : RealM PUnit :=
+  fun s => match x s with
+  | EStateM.Result.ok a s => EStateM.Result.ok () s
+  | EStateM.Result.error e s => EStateM.Result.ok () s
+
+abbrev runIO_ (x : IO α) : RealM PUnit :=
+  runEIO_ x