source
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.

Instances

source
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.

source
def Lean.getRefPos {m : Type → Type} [Monad m] [MonadLog m] :
m String.Pos.Raw

Return the position (as `String.Pos.Raw`) 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] [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)

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.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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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 "'")

Instances For