Documentation

Lean.Log

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

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

    getRef : m Lean.Syntax

  • The name of the file being processed.

    getFileName : m String

  • Return true if errors have been logged.

    hasErrors : m Bool

  • Log a new message.

    logMessage : Lean.Message → m Unit

The MonadLog interface for logging error messages.

Instances
    source
    instance Lean.instMonadLog (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.MonadLog m] :
    Lean.MonadLog n
    Equations
    source
    def Lean.getRefPos {m : Type → Type} [inst : Monad m] [inst : 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
    source
    def Lean.getRefPosition {m : Type → Type} [inst : Monad m] [inst : 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.)

    Equations
    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} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : optParam 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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.logErrorAt {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : 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
    source
    def Lean.logWarningAt {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : 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
    source
    def Lean.logInfoAt {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : 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.

    Equations
    source
    def Lean.log {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (msgData : Lean.MessageData) (severity : optParam 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
    source
    def Lean.logError {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : 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
    source
    def Lean.logWarning {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (msgData : Lean.MessageData) :
    m Unit

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

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.logInfo {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : 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
    source
    def Lean.logUnknownDecl {m : Type → Type} [inst : Monad m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
    m Unit

    Log the error message "unknown declaration"

    Equations