Lean.Elab.Log

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

Type

getRef : m Lean.Syntax
getFileName : m String
logMessage : Lean.Message → m Unit

Instances

instance Lean.Elab.instMonadLog (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.Elab.MonadLog m] :

Lean.Elab.MonadLog n

Equations

Lean.Elab.instMonadLog m n = Lean.Elab.MonadLog.mk (liftM Lean.Elab.MonadLog.getRef) (liftM Lean.Elab.getFileName) fun msg => liftM (Lean.Elab.logMessage msg)

source

def Lean.Elab.getRefPos {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] :

m String.Pos

Equations

Lean.Elab.getRefPos = do let ref ← Lean.Elab.MonadLog.getRef pure (Option.getD (Lean.Syntax.getPos? ref) 0)

source

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

m Lean.Position

Equations

Lean.Elab.getRefPosition = do let fileMap ← Lean.getFileMap let a ← Lean.Elab.getRefPos pure (Lean.FileMap.toPosition fileMap a)

source

def Lean.Elab.logAt {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : optParam Lean.MessageSeverity Lean.MessageSeverity.error) :

m Unit

Equations

Lean.Elab.logAt ref msgData severity = if (severity == Lean.MessageSeverity.error && Lean.MessageData.hasSyntheticSorry msgData) = true then pure PUnit.unit else do let a ← Lean.Elab.MonadLog.getRef let ref : Lean.Syntax := Lean.replaceRef ref a let pos : String.Pos := Option.getD (Lean.Syntax.getPos? ref) 0 let endPos : String.Pos := Option.getD (Lean.Syntax.getTailPos? ref) pos let fileMap ← Lean.getFileMap let msgData ← Lean.addMessageContext msgData let a ← Lean.Elab.getFileName Lean.Elab.logMessage { fileName := a, pos := Lean.FileMap.toPosition fileMap pos, endPos := some (Lean.FileMap.toPosition fileMap endPos), severity := severity, caption := "", data := msgData }

source

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

m Unit

Equations

Lean.Elab.logErrorAt ref msgData = Lean.Elab.logAt ref msgData

source

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

m Unit

Equations

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

source

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

m Unit

Equations

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

source

def Lean.Elab.log {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] (msgData : Lean.MessageData) (severity : optParam Lean.MessageSeverity Lean.MessageSeverity.error) :

m Unit

Equations

Lean.Elab.log msgData severity = do let ref ← Lean.Elab.MonadLog.getRef Lean.Elab.logAt ref msgData severity

source

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

m Unit

Equations

Lean.Elab.logError msgData = Lean.Elab.log msgData

source

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

m Unit

Equations

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

source

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

m Unit

Equations

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

source

def Lean.Elab.logException {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] [inst : MonadLiftT IO m] (ex : Lean.Exception) :

m Unit

Equations

Lean.Elab.logException ex = match ex with | Lean.Exception.error ref msg => Lean.Elab.logErrorAt ref msg | Lean.Exception.internal id x => if Lean.Elab.isAbortExceptionId id = true then pure PUnit.unit else do let name ← liftM (Lean.InternalExceptionId.getName id) Lean.Elab.logError (Lean.toMessageData "internal exception: " ++ Lean.toMessageData name ++ Lean.toMessageData "")

source

def Lean.Elab.logTrace {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] (cls : Lean.Name) (msgData : Lean.MessageData) :

m Unit

Equations

Lean.Elab.logTrace cls msgData = Lean.Elab.logInfo (Lean.MessageData.tagged cls (Lean.toMessageData "[" ++ Lean.toMessageData cls ++ Lean.toMessageData "] " ++ Lean.toMessageData msgData ++ Lean.toMessageData ""))

source

@[inline]

def Lean.Elab.trace {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (cls : Lean.Name) (msg : Unit → Lean.MessageData) :

m Unit

Equations

Lean.Elab.trace cls msg = do let a ← Lean.getOptions if Lean.checkTraceOption a cls = true then Lean.Elab.logTrace cls (msg ()) else pure PUnit.unit

source

def Lean.Elab.logDbgTrace {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (msg : Lean.MessageData) :

m Unit

Equations

Lean.Elab.logDbgTrace msg = Lean.Elab.trace `Elab.debug fun x => msg

source

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

m Unit

Equations

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