Documentation

Lean.Log

source
class Lean.MonadLog (m : Type → Type) extends Lean.MonadFileMap m :
Type

The MonadLog interface for logging error messages.

  • getFileMap : m Lean.FileMap
  • getRef : m Lean.Syntax

    Return the current reference syntax being used to provide position information.

  • getFileName : m String

    The name of the file being processed.

  • hasErrors : m Bool

    Return true if errors have been logged.

  • logMessage : Lean.Message → m Unit

    Log a new message.

Instances
    source
    instance Lean.instMonadLogOfMonadLift (m n : Type → Type) [MonadLift m n] [Lean.MonadLog m] :
    Lean.MonadLog n
    source
    def Lean.getRefPos {m : Type → Type} [Monad m] [Lean.MonadLog m] :
    m String.Pos

    Return the position (as String.pos) associated with the current reference syntax (i.e., the syntax object returned by getRef.)

    Equations
    • Lean.getRefPos = do let ref ← Lean.MonadLog.getRef pure (ref.getPos?.getD 0)
    Instances For
      source
      def Lean.getRefPosition {m : Type → Type} [Monad m] [Lean.MonadLog m] :
      m Lean.Position

      Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by getRef.)

      Instances For
        source
        opaque Lean.warningAsError :
        Lean.Option Bool

        If warningAsError is set to true, then warning messages are treated as errors.

        source
        def Lean.logAt {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : Lean.MessageSeverity := Lean.MessageSeverity.error) :
        m Unit

        Log the message msgData at the position provided by ref with the given severity. If getRef has position information but ref does not, we use getRef. We use the fileMap to find the line and column numbers for the error message.

        Instances For
          source
          def Lean.logErrorAt {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (ref : Lean.Syntax) (msgData : Lean.MessageData) :
          m Unit

          Log a new error message using the given message data. The position is provided by ref.

          Equations
          Instances For
            source
            def Lean.logWarningAt {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (ref : Lean.Syntax) (msgData : Lean.MessageData) :
            m Unit

            Log a new warning message using the given message data. The position is provided by ref.

            Equations
            Instances For
              source
              def Lean.logInfoAt {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (ref : Lean.Syntax) (msgData : Lean.MessageData) :
              m Unit

              Log a new information message using the given message data. The position is provided by ref.

              Instances For
                source
                def Lean.log {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (msgData : Lean.MessageData) (severity : Lean.MessageSeverity := Lean.MessageSeverity.error) :
                m Unit

                Log a new error/warning/information message using the given message data and severity. The position is provided by getRef.

                Equations
                • Lean.log msgData severity = do let ref ← Lean.MonadLog.getRef Lean.logAt ref msgData severity
                Instances For
                  source
                  def Lean.logError {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (msgData : Lean.MessageData) :
                  m Unit

                  Log a new error message using the given message data. The position is provided by getRef.

                  Equations
                  Instances For
                    source
                    def Lean.logWarning {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (msgData : Lean.MessageData) :
                    m Unit

                    Log a new warning message using the given message data. The position is provided by getRef.

                    Instances For
                      source
                      def Lean.logInfo {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (msgData : Lean.MessageData) :
                      m Unit

                      Log a new information message using the given message data. The position is provided by getRef.

                      Equations
                      Instances For
                        source
                        def Lean.logUnknownDecl {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (declName : Lean.Name) :
                        m Unit

                        Log the error message "unknown declaration"

                        Equations
                        Instances For