Documentation

Lake.Util.MainM

source
def Lake.MainM (α : Type) :
Type

The monad in Lake for main-like functions. Supports IO, logging, and exit.

Instances For
    source
    @[implicit_reducible]
    instance Lake.instMonadMainM :
    Monad MainM
    source
    @[implicit_reducible]
    instance Lake.instMonadFinallyMainM :
    MonadFinally MainM
    source
    @[implicit_reducible]
    instance Lake.instMonadLiftBaseIOMainM :
    MonadLift BaseIO MainM

    Basics #

    source
    @[inline]
    def Lake.MainM.mk {α : Type} (x : EIO ExitCode α) :
    MainM α
    Instances For
      source
      @[inline]
      def Lake.MainM.toEIO {α : Type} (self : MainM α) :
      EIO ExitCode α
      Instances For
        source
        @[inline]
        def Lake.MainM.toBaseIO {α : Type} (self : MainM α) :
        BaseIO (Except ExitCode α)
        Instances For
          source
          @[inline]
          def Lake.MainM.run {α : Type} (self : MainM α) :
          BaseIO ExitCode
          Instances For

            Exits #

            source
            @[inline]
            def Lake.MainM.exit {α : Type} (rc : ExitCode) :
            MainM α

            Exit with given return code.

            Instances For
              source
              @[implicit_reducible]
              instance Lake.MainM.instMonadExit :
              MonadExit MainM
              source
              @[inline]
              def Lake.MainM.tryCatchExit {α : Type} (f : ExitCode → MainM α) (self : MainM α) :
              MainM α

              Try this and catch exits.

              Instances For
                source
                @[inline]
                def Lake.MainM.tryCatchError {α : Type} (f : ExitCode → MainM α) (self : MainM α) :
                MainM α

                Try this and catch error codes (i.e., non-zero exits).

                Instances For
                  source
                  @[inline]
                  def Lake.MainM.failure {α : Type} :
                  MainM α

                  Exit with a generic error code (i.e., 1).

                  Instances For
                    source
                    @[inline]
                    def Lake.MainM.orElse {α : Type} (self : MainM α) (other : Unit → MainM α) :
                    MainM α

                    If this exits with an error code (i.e., not 0), perform other.

                    Instances For

                      Logging and IO #

                      source
                      @[implicit_reducible]
                      instance Lake.MainM.instMonadLog :
                      MonadLog MainM
                      source
                      @[inline]
                      def Lake.MainM.error {α : Type} (msg : String) (rc : ExitCode := 1) :
                      MainM α

                      Print out a error line with the given message and then exit with an error code.

                      Instances For
                        source
                        @[implicit_reducible]
                        instance Lake.MainM.instMonadError :
                        MonadError MainM
                        source
                        @[implicit_reducible]
                        instance Lake.MainM.instMonadLiftIO :
                        MonadLift IO MainM
                        source
                        @[inline]
                        def Lake.MainM.runLogIO {α : Type} (x : LogIO α) (cfg : LogConfig := { }) :
                        MainM α
                        Instances For
                          source
                          def Lake.MainM.liftLogIO {α : Type} (x : LogIO α) :
                          MainM α
                          Instances For
                            source
                            @[implicit_reducible, instance 100]
                            instance Lake.MainM.instMonadLiftLogIO :
                            MonadLift LogIO MainM
                            source
                            @[inline]
                            def Lake.MainM.runLoggerIO {α : Type} (x : LoggerIO α) (cfg : LogConfig := { }) :
                            MainM α
                            Instances For
                              source
                              def Lake.MainM.liftLoggerIO {α : Type} (x : LoggerIO α) :
                              MainM α
                              Instances For
                                source
                                @[implicit_reducible, instance 100]
                                instance Lake.MainM.instMonadLiftLoggerIO :
                                MonadLift LoggerIO MainM