Documentation

Lean.Log

class Lean.MonadLog (m : TypeType) extends Lean.MonadFileMap m :

The MonadLog interface for logging error messages.

  • 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.Messagem Unit

    Log a new message.

Instances
Equations

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 refLean.MonadLog.getRef pure (ref.getPos?.getD 0)

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 fileMapLean.getFileMap let __do_liftLean.getRefPos pure (fileMap.toPosition __do_lift)

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

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.

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

Equations

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

Equations

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

Equations

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 refLean.MonadLog.getRef Lean.logAt ref msgData severity

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

Equations

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.

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

Equations

Log the error message "unknown declaration"

Equations