Lean.Log

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

source

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

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

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] [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

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

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

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

Instances For

source

def Lean.log {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (msgData : MessageData) (severity : MessageSeverity := 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

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

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

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

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

Instances For