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

The MonadLog interface for logging error messages.

• getFileMap : m FileMap
• getRef : m 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 : Message → m Unit

  Log a new message.

instance Lean.instMonadLogOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadLog m] : MonadLog n

Equations

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

def Lean.getRefPos {m : Type → Type} [Monad m] [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)

def Lean.getRefPosition {m : Type → Type} [Monad m] [MonadLog m] : m Position

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

Equations

• Lean.getRefPosition = do let fileMap ← Lean.getFileMap let __do_lift ← Lean.getRefPos pure (fileMap.toPosition __do_lift)

opaque Lean.warningAsError : Lean.Option Bool

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

def Lean.errorDescriptionWidget : Widget.Module

A widget for displaying error names and explanation links.

Equations

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

def Lean.logAt {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : 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.

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

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

Equations

• Lean.logErrorAt ref msgData = Lean.logAt ref msgData

def Lean.logNamedErrorAt {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (ref : Syntax) (name : Name) (msgData : MessageData) : m Unit

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

Note: Use the macro logNamedErrorAt, which validates error names, instead of calling this function directly.

Equations

• Lean.logNamedErrorAt ref name msgData = Lean.logAt ref (msgData.tagWithErrorName name)

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

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

Equations

• Lean.logWarningAt ref msgData = Lean.logAt ref msgData Lean.MessageSeverity.warning

def Lean.logNamedWarningAt {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (ref : Syntax) (name : Name) (msgData : MessageData) : m Unit

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

Note: Use the macro logNamedWarningAt, which validates error names, instead of calling this function directly.

Equations

• Lean.logNamedWarningAt ref name msgData = Lean.logAt ref (msgData.tagWithErrorName name) Lean.MessageSeverity.warning

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

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

Equations

• Lean.logInfoAt ref msgData = Lean.logAt ref msgData Lean.MessageSeverity.information

def Lean.log {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : 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 isSilent = do let ref ← Lean.MonadLog.getRef Lean.logAt ref msgData severity isSilent

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

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

Equations

• Lean.logError msgData = Lean.log msgData

def Lean.logNamedError {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (name : Name) (msgData : MessageData) : m Unit

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

Note: Use the macro logNamedError, which validates error names, instead of calling this function directly.

Equations

• Lean.logNamedError name msgData = Lean.log (msgData.tagWithErrorName name)

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

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

Equations

• Lean.logWarning msgData = Lean.log msgData Lean.MessageSeverity.warning

def Lean.logNamedWarning {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (name : Name) (msgData : MessageData) : m Unit

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

Note: Use the macro logNamedWarning, which validates error names, instead of calling this function directly.

Equations

• Lean.logNamedWarning name msgData = Lean.log (msgData.tagWithErrorName name) Lean.MessageSeverity.warning

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

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

Equations

• Lean.logInfo msgData = Lean.log msgData Lean.MessageSeverity.information

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

Log the error message "unknown declaration"

Equations

• Lean.logUnknownDecl declName = Lean.logError (Lean.toMessageData "unknown declaration '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'")