refactor: replace RealM with BaseIO

Lake/BuildMonad.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Task
 import Lake.Trace
-import Lake.RealM
 import Lake.LogMonad
 import Lake.InstallPath
 
@@ -22,7 +21,7 @@ structure BuildContext where
   lakeInstall : LakeInstall
   deriving Inhabited
 
-abbrev BuildCoreM := LogMethodsT RealM <| EIO PUnit
+abbrev BuildCoreM := LogMethodsT BaseIO <| EIO PUnit
 abbrev BuildM := ReaderT BuildContext BuildCoreM
 
 --------------------------------------------------------------------------------
@@ -49,10 +48,10 @@ def getLakeInstall : BuildM LakeInstall :=
 
 namespace BuildCoreM
 
-def run (logMethods : LogMethods RealM) (self : BuildCoreM α) : IO α :=
+def run (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : IO α :=
   ReaderT.run self logMethods |>.toIO fun _ => IO.userError "build failed"
 
-def runWith (logMethods : LogMethods RealM) (self : BuildCoreM α) : EIO PUnit α :=
+def runWith (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : EIO PUnit α :=
   ReaderT.run self logMethods
 
 protected def failure : BuildCoreM α :=
@@ -66,7 +65,7 @@ instance : Alternative BuildCoreM where
   orElse := BuildCoreM.orElse
 
 def runIO (x : IO α) : BuildCoreM α := do
-  match (← RealM.runIO' x) with
+  match (← x.toBaseIO) with
   | Except.ok a => pure a
   | Except.error e => do
     logError (toString e)
@@ -79,7 +78,7 @@ instance : MonadLift (LogT IO) BuildCoreM where
 
 end BuildCoreM
 
-def BuildM.run (logMethods : LogMethods RealM) (ctx : BuildContext) (self : BuildM α) : IO α :=
+def BuildM.run (logMethods : LogMethods BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α :=
   self ctx |>.run logMethods
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α

Lake/Cli.lean

@@ -57,7 +57,7 @@ open CliT
 
 /-- Print out a line wih the given message and then exit with an error code. -/
 def error (msg : String) (rc : UInt32 := 1) : CliM α := do
-  RealM.runIO_ <| IO.eprintln s!"error: {msg}"
+  IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
   exit rc
 
 /--
@@ -65,7 +65,7 @@ def error (msg : String) (rc : UInt32 := 1) : CliM α := do
   If it throws an error, invoke `error` with the its message.
 -/
 def runIO (x : IO α) : CliM α := do
-  match (← RealM.runIO' x) with
+  match (← x.toBaseIO) with
   | Except.ok a => pure a
   | Except.error e => error (toString e)
 

Lake/LogMonad.lean

@@ -3,8 +3,6 @@ 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
@@ -35,15 +33,15 @@ def nop [Pure m] : LogMethods m :=
 
 instance [Pure m] : Inhabited (LogMethods m) := ⟨LogMethods.nop⟩
 
-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 io [MonadLiftT BaseIO m] : LogMethods m where
+  logInfo msg := IO.println msg |>.catchExceptions fun _ => ()
+  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => ()
+  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
 
-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}"
+def eio [MonadLiftT BaseIO m] : LogMethods m where
+  logInfo msg := IO.eprintln s!"info: {msg}" |>.catchExceptions fun _ => ()
+  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => ()
+  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
 
 def lift [MonadLiftT m n] (self : LogMethods m) : LogMethods n where
   logInfo msg := liftM <| self.logInfo msg

Lake/MainM.lean

@@ -3,8 +3,6 @@ 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
 
 /-- A process exit / return code. -/
@@ -28,11 +26,11 @@ namespace MainM
 @[inline] protected def toEIO (self : MainM α) : EIO ExitCode α :=
   self
 
-@[inline] protected def toRealM (self : MainM α) : RealM (Except ExitCode α) :=
-  RealM.runEIO' self.toEIO
+@[inline] protected def toBaseIO (self : MainM α) : BaseIO (Except ExitCode α) :=
+  self.toEIO.toBaseIO
 
-protected def run (self : MainM PUnit) : RealM ExitCode :=
-  self.toRealM.map fun | Except.ok _ => 0 | Except.error rc => rc
+protected def run (self : MainM PUnit) : BaseIO ExitCode :=
+  self.toBaseIO.map fun | Except.ok _ => 0 | Except.error rc => rc
 
 /-- Exit with given return code. -/
 protected def exit (rc : ExitCode) : MainM α :=

Lake/RealM.lean

@@ -1,48 +0,0 @@
-/-
-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