Documentation

Lake.Util.Log

inductive Lake.Verbosity :
Instances For
    Equations
    inductive Lake.AnsiMode :

    Whether to ANSI escape codes.

    • auto: Lake.AnsiMode

      Automatically determine whether to use ANSI escape codes based on whether the stream written to is a terminal.

    • ansi: Lake.AnsiMode

      Use ANSI escape codes.

    • noAnsi: Lake.AnsiMode

      Do not use ANSI escape codes.

    Instances For

      Returns whether to ANSI escape codes with the stream out.

      Equations
      Instances For
        def Lake.Ansi.chalk (colorCode : String) (text : String) :

        Wrap text in ANSI escape sequences to make it bold and color it the ANSI colorCode. Resets all terminal font attributes at the end of the text.

        Equations
        Instances For
          inductive Lake.OutStream :

          A pure representation of output stream.

          Instances For

            Returns the real output stream associated with OutStream.

            Equations
            Instances For
              inductive Lake.LogLevel :
              Instances For
                Equations

                Unicode icon for representing the log level.

                Equations
                Instances For

                  ANSI escape code for coloring text of at the log level.

                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        structure Lake.LogEntry :
                        Instances For
                          Equations
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            class Lake.MonadLog (m : Type u → Type v) :
                            Instances
                              @[inline]
                              def Lake.logVerbose {m : Type u_1 → Type u_2} [Monad m] [Lake.MonadLog m] (message : String) :
                              Equations
                              Instances For
                                @[inline]
                                def Lake.logInfo {m : Type u_1 → Type u_2} [Monad m] [Lake.MonadLog m] (message : String) :
                                Equations
                                Instances For
                                  @[inline]
                                  def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                                    Equations
                                    Instances For
                                      @[specialize #[]]
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[deprecated]
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          def Lake.logToStream (e : Lake.LogEntry) (out : IO.FS.Stream) (minLv : Lake.LogLevel) (useAnsi : Bool) :
                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev Lake.MonadLog.nop {m : TypeType u_1} [Pure m] :
                                            Equations
                                            Instances For
                                              Equations
                                              • Lake.MonadLog.instInhabitedOfPure = { default := Lake.MonadLog.nop }
                                              @[reducible, inline]
                                              abbrev Lake.MonadLog.lift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLiftT m n] (self : Lake.MonadLog m) :
                                              Equations
                                              Instances For
                                                instance Lake.MonadLog.instOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [methods : Lake.MonadLog m] :
                                                Equations
                                                • Lake.MonadLog.instOfMonadLift = methods.lift
                                                @[reducible, inline, deprecated]
                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                      • out.logger minLv ansiMode = { logEntry := fun (e : Lake.LogEntry) => liftM (out.logEntry e minLv ansiMode) }
                                                      Instances For
                                                        @[reducible, inline]
                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) :
                                                              Type (max v w)

                                                              A monad equipped with a MonadLog instance

                                                              Equations
                                                              Instances For
                                                                instance Lake.MonadLogT.instInhabitedOfPure {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] :
                                                                Equations
                                                                • Lake.MonadLogT.instInhabitedOfPure = { default := fun (x : Lake.MonadLog m) => pure default }
                                                                instance Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] :
                                                                Equations
                                                                @[inline]
                                                                def Lake.MonadLogT.adaptMethods {n : Type u_1 → Type u_2} {m : Type u_3 → Type u_1} {m' : Type u_4 → Type u_1} {α : Type u_1} [Monad n] (f : Lake.MonadLog mLake.MonadLog m') (self : Lake.MonadLogT m' n α) :
                                                                Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Lake.MonadLogT.ignoreLog {m : TypeType u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : Lake.MonadLogT m n α) :
                                                                  n α
                                                                  Equations
                                                                  • self.ignoreLog = self Lake.MonadLog.nop
                                                                  Instances For
                                                                    structure Lake.Log :
                                                                    Instances For
                                                                      Equations
                                                                      structure Lake.Log.Pos :

                                                                      A position in a Log (i.e., an array index). Can be past the log's end.

                                                                      Instances For
                                                                        Equations
                                                                        Equations
                                                                        @[inline]
                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          Equations
                                                                          • log.size = log.entries.size
                                                                          Instances For
                                                                            @[inline]
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                • log.endPos = { val := log.entries.size }
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                  • log.push e = { entries := log.entries.push e }
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    Equations
                                                                                    • log.append o = { entries := log.entries.append o.entries }
                                                                                    Instances For
                                                                                      @[inline]

                                                                                      Takes log entries between start (inclusive) and stop (exclusive).

                                                                                      Equations
                                                                                      • log.extract start stop = { entries := log.entries.extract start.val stop.val }
                                                                                      Instances For
                                                                                        @[inline]

                                                                                        Removes log entries after pos (inclusive).

                                                                                        Equations
                                                                                        • log.dropFrom pos = { entries := log.entries.shrink pos.val }
                                                                                        Instances For
                                                                                          @[inline]

                                                                                          Takes log entries before pos (exclusive).

                                                                                          Equations
                                                                                          • log.takeFrom pos = log.extract pos log.endPos
                                                                                          Instances For
                                                                                            @[inline]

                                                                                            Splits the log into two from pos. The first log is from the start to pos (exclusive), and the second log is from pos (inclusive) to the end.

                                                                                            Equations
                                                                                            • log.split pos = (log.dropFrom pos, log.takeFrom pos)
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[inline]
                                                                                                def Lake.Log.replay {m : Type u_1 → Type u_2} [Monad m] [logger : Lake.MonadLog m] (log : Lake.Log) :
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      The max log level of entries in this log. If empty, returns trace.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]

                                                                                                        Add a LogEntry to the end of the monad's Log.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[reducible, inline]
                                                                                                          Equations
                                                                                                          • Lake.MonadLog.ofMonadState = { logEntry := Lake.pushLogEntry }
                                                                                                          Instances For
                                                                                                            @[inline]

                                                                                                            Returns the monad's log.

                                                                                                            Equations
                                                                                                            • Lake.getLog = get
                                                                                                            Instances For
                                                                                                              @[inline]

                                                                                                              Returns the current end position of the monad's log (i.e., its size).

                                                                                                              Equations
                                                                                                              • Lake.getLogPos = (fun (x : Lake.Log) => x.endPos) <$> Lake.getLog
                                                                                                              Instances For
                                                                                                                @[inline]

                                                                                                                Removes the section monad's log starting and returns it.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]

                                                                                                                  Removes the monad's log starting at pos and returns it. Useful for extracting logged errors after catching an error position from an ELogT (e.g., LogIO).

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]

                                                                                                                    Backtracks the monad's log to pos. Useful for discarding logged errors after catching an error position from an ELogT (e.g., LogIO).

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Lake.extractLog {m : TypeType u_1} [Monad m] [MonadStateOf Lake.Log m] (x : m PUnit) :

                                                                                                                      Returns the log from x while leaving it intact in the monad.

                                                                                                                      Equations
                                                                                                                      • Lake.extractLog x = do let iniPosLake.getLogPos x let logLake.getLog pure (log.takeFrom iniPos)
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Lake.withExtractLog {m : TypeType u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] (x : m α) :
                                                                                                                        m (α × Lake.Log)

                                                                                                                        Returns the log from x and its result while leaving it intact in the monad.

                                                                                                                        Equations
                                                                                                                        • Lake.withExtractLog x = do let iniPosLake.getLogPos let ax let logLake.getLog pure (a, log.takeFrom iniPos)
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Lake.withLogErrorPos {m : TypeType u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m α) :
                                                                                                                          m α

                                                                                                                          Performs x and backtracks any error to the log position before x.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Lake.errorWithLog {m : TypeType u_1} {β : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m PUnit) :
                                                                                                                            m β

                                                                                                                            Performs x and groups all logs generated into an error block.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def Lake.withLoggedIO {m : TypeType u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [Lake.MonadLog m] [MonadFinally m] (x : m α) :
                                                                                                                              m α

                                                                                                                              Captures IO in x into an informational log entry.

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def Lake.ELog.error {m : TypeType u_1} {α : Type} [Monad m] [Lake.MonadLog m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (msg : String) :
                                                                                                                                m α

                                                                                                                                Throw with the logged error message.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[reducible, inline]

                                                                                                                                  Alternative instance for monads with Log state and Log.Pos errors.

                                                                                                                                  Equations
                                                                                                                                  • Lake.ELog.monadError = { error := fun {α : Type} => Lake.ELog.error }
                                                                                                                                  Instances For
                                                                                                                                    @[inline]

                                                                                                                                    Fail without logging anything.

                                                                                                                                    Equations
                                                                                                                                    • Lake.ELog.failure = do let __do_liftLake.getLogPos throw __do_lift
                                                                                                                                    Instances For
                                                                                                                                      @[inline]
                                                                                                                                      def Lake.ELog.orElse {m : TypeType u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (x : m α) (y : Unitm α) :
                                                                                                                                      m α

                                                                                                                                      Performs x. If it fails, drop its log and perform y.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible, inline]

                                                                                                                                        Alternative instance for monads with Log state and Log.Pos errors.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[reducible, inline]
                                                                                                                                          abbrev Lake.LogT (m : TypeType) (α : Type) :

                                                                                                                                          A monad equipped with a log.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                            • Lake.instMonadLogLogTOfMonad = Lake.MonadLog.ofMonadState
                                                                                                                                            @[reducible, inline]
                                                                                                                                            abbrev Lake.LogT.run {m : TypeType} {α : Type} [Functor m] (self : Lake.LogT m α) (log : optParam Lake.Log ) :
                                                                                                                                            m (α × Lake.Log)
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline]
                                                                                                                                              abbrev Lake.LogT.run' {m : TypeType} {α : Type} [Functor m] (self : Lake.LogT m α) (log : optParam Lake.Log ) :
                                                                                                                                              m α
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Lake.LogT.takeAndRun {n : TypeType u_1} {m : TypeType} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadLiftT m n] [MonadFinally n] (self : Lake.LogT m α) :
                                                                                                                                                n α

                                                                                                                                                Run self with the log taken from the state of the monad n.

                                                                                                                                                Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail.

                                                                                                                                                Equations
                                                                                                                                                • self.takeAndRun = do let __do_liftLake.takeLog let __discrliftM (self __do_lift) match __discr with | (a, log) => do set log pure a
                                                                                                                                                Instances For
                                                                                                                                                  @[inline]
                                                                                                                                                  def Lake.LogT.replayLog {n : TypeType u_1} {m : TypeType} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.LogT m α) :
                                                                                                                                                  n α

                                                                                                                                                  Runs self in n and then replays the entries of the resulting log using the new monad's logger.

                                                                                                                                                  Equations
                                                                                                                                                  • self.replayLog = do let __discrliftM (self ) match __discr with | (a, log) => do log.replay pure a
                                                                                                                                                  Instances For
                                                                                                                                                    @[reducible, inline]
                                                                                                                                                    abbrev Lake.ELogT (m : TypeType) (α : Type) :

                                                                                                                                                    A monad equipped with a log and the ability to error at some log position.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[reducible, inline]
                                                                                                                                                      abbrev Lake.ELogResult (α : Type u_1) :
                                                                                                                                                      Type u_1
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                        • Lake.instMonadLogELogTOfMonad = Lake.MonadLog.ofMonadState
                                                                                                                                                        Equations
                                                                                                                                                        • Lake.instMonadErrorELogTOfMonad = Lake.ELog.monadError
                                                                                                                                                        Equations
                                                                                                                                                        • Lake.instAlternativeELogTOfMonad = Lake.ELog.alternative
                                                                                                                                                        @[reducible, inline]
                                                                                                                                                        abbrev Lake.ELogT.run {m : TypeType} {α : Type} (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[reducible, inline]
                                                                                                                                                          abbrev Lake.ELogT.run' {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[reducible, inline]
                                                                                                                                                            abbrev Lake.ELogT.toLogT {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) :
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[reducible, inline]
                                                                                                                                                              abbrev Lake.ELogT.toLogT? {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) :
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                abbrev Lake.ELogT.run? {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                  abbrev Lake.ELogT.run?' {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                                  m (Option α)
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def Lake.ELogT.catchLog {m : TypeType} {α : Type} [Monad m] (f : Lake.LogLake.LogT m α) (self : Lake.ELogT m α) :
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[reducible, inline, deprecated Lake.ELogT.run?]
                                                                                                                                                                      abbrev Lake.ELogT.captureLog {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Lake.ELogT.takeAndRun {n : TypeType u_1} {m : TypeType} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadExceptOf Lake.Log.Pos n] [MonadLiftT m n] (self : Lake.ELogT m α) :
                                                                                                                                                                        n α

                                                                                                                                                                        Run self with the log taken from the state of the monad n,

                                                                                                                                                                        Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail. Note excludes the native log position failure of ELogT, which are lifted safely.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          def Lake.ELogT.replayLog? {n : TypeType u_1} {m : TypeType} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) :
                                                                                                                                                                          n (Option α)

                                                                                                                                                                          Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a none result.

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Lake.ELogT.replayLog {n : TypeType u_1} {m : TypeType} {α : Type} [Alternative n] [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) :
                                                                                                                                                                            n α

                                                                                                                                                                            Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a failure in the new monad.

                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                              abbrev Lake.LogIO (α : Type) :

                                                                                                                                                                              A monad equipped with a log, a log error position, and the ability to perform I/O.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                @[reducible, inline, deprecated Lake.ELogT.run?]
                                                                                                                                                                                abbrev Lake.LogIO.captureLog {m : TypeType} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : optParam Lake.Log ) :
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]

                                                                                                                                                                                  Runs a LogIO action in BaseIO. Prints log entries of at least minLv to out.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For