def Lean.mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (endPos : Option Position := none) : String

inductive Lean.MessageSeverity : Type

• information : MessageSeverity
• warning : MessageSeverity
• error : MessageSeverity

instance Lean.instInhabitedMessageSeverity : Inhabited MessageSeverity

instance Lean.instBEqMessageSeverity : BEq MessageSeverity

instance Lean.instToJsonMessageSeverity : ToJson MessageSeverity

instance Lean.instFromJsonMessageSeverity : FromJson MessageSeverity

structure Lean.MessageDataContext : Type

• env : Environment
• mctx : MetavarContext
• lctx : LocalContext
• opts : Options

structure Lean.NamingContext : Type

A naming context is the information needed to shorten names in pretty printing.

It gives the current namespace and the list of open declarations.

• currNamespace : Name
• openDecls : List OpenDecl

structure Lean.TraceData : Type

• cls : Name

  Trace class, e.g. Elab.step.

• startTime : Float

  Start time in seconds; 0 if unknown to avoid Option allocation.

• stopTime : Float

  Stop time in seconds; 0 if unknown to avoid Option allocation.

• collapsed : Bool

  Whether trace node defaults to collapsed in the infoview.

• tag : String

  Optional tag shown in trace.profiler.output output after the trace class name.

inductive Lean.MessageData : Type

Structured message data. We use it for reporting errors, trace messages, etc.

• ofFormatWithInfos : FormatWithInfos → MessageData

  Eagerly formatted text with info annotations. This constructor is inspected in various hacks.

• ofGoal : MVarId → MessageData
• ofWidget : Widget.WidgetInstance → MessageData → MessageData

  A widget instance.

  In ofWidget wi alt, the nested message alt should approximate the contents of the widget without itself using ofWidget wi _. This is used as fallback in environments that cannot display user widgets. alt may nest any structured message, for example ofGoal to approximate a tactic state widget, and, if necessary, even other widget instances (for which approximations are computed recursively).

  Note that unlike with Widget.savePanelWidgetInfo, the infoview will not pass any additional props to the widget instance.

• withContext : MessageDataContext → MessageData → MessageData

  withContext ctx d specifies the pretty printing context (env, mctx, lctx, opts) for the nested expressions in d.

• withNamingContext : NamingContext → MessageData → MessageData
• nest : Nat → MessageData → MessageData

  Lifted Format.nest

• group : MessageData → MessageData

  Lifted Format.group

• compose : MessageData → MessageData → MessageData

  Lifted Format.compose

• tagged : Name → MessageData → MessageData

  Tagged sections. Name should be viewed as a "kind", and is used by MessageData inspector functions. Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure".

• trace (data : TraceData) (msg : MessageData) (children : Array MessageData) : MessageData
• ofLazy (f : Option PPContext → BaseIO Dynamic) (hasSyntheticSorry : MetavarContext → Bool) : MessageData

  A lazy message. The provided thunk will not be run until it is about to be displayed. This can save computation in cases where the message may never be seen.

  The Dynamic value is expected to be a MessageData, which is a workaround for the positivity restriction.

  If the thunked message is produced for a term that contains a synthetic sorry, hasSyntheticSorry should return true. This is used to filter out certain messages.

instance Lean.instInhabitedMessageData : Inhabited MessageData

instance Lean.instTypeNameMessageData : TypeName MessageData

def Lean.MessageData.ofFormat (fmt : Format) : MessageData

Eagerly formatted text.

def Lean.MessageData.lazy (f : PPContext → BaseIO MessageData) (hasSyntheticSorry : MetavarContext → Bool := fun (x : MetavarContext) => false) (onMissingContext : Unit → BaseIO MessageData := fun (x : Unit) => pure (ofFormat (Std.Format.text "(invalid MessageData.lazy, missing context)"))) : MessageData

Lazy message data production, with access to the context as given by a surrounding MessageData.withContext (which is expected to exist).

partial def Lean.MessageData.hasTag (p : Name → Bool) : MessageData → Bool

Returns true when the message contains a MessageData.tagged tag .. constructor where p tag is true.

This does not descend into lazily generated subtrees (.ofLazy); message tags of interest (like those added by logLinter) are expected to be near the root of the MessageData, and not hidden inside .ofLazy.

def Lean.MessageData.kind : MessageData → Name

Returns the top-level tag of the message. If none, returns Name.anonymous.

This does not descend into message subtrees (e.g., .compose, .ofLazy). The message kind is expected to describe the whole message.

def Lean.MessageData.isTrace : MessageData → Bool

def Lean.MessageData.nil : MessageData

An empty message.

def Lean.MessageData.mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext

def Lean.MessageData.ofSyntax (stx : Syntax) : MessageData

def Lean.MessageData.ofExpr (e : Expr) : MessageData

def Lean.MessageData.ofLevel (l : Level) : MessageData

def Lean.MessageData.ofName (n : Name) : MessageData

Simply formats the name. See MessageData.ofConstName for richer messages.

def Lean.MessageData.ofConstName (constName : Name) (fullNames : Bool := false) : MessageData

Represents a constant name such that hovering and "go to definition" works. If there is no such constant in the environment, the name is simply formatted, but sanitized if it is a hygienic name. Use MessageData.ofName if hovers are undesired.

If fullNames is true, then pretty prints as if pp.fullNames is true. Otherwise, pretty prints using the current user setting for pp.fullNames.

def Lean.MessageData.hasSyntheticSorry (msg : MessageData) : Bool

partial def Lean.MessageData.hasSyntheticSorry.visit (mctx? : Option MetavarContext) : MessageData → Bool

opaque Lean.MessageData.maxTraceChildren : Lean.Option Nat

Maximum number of trace node children to display by default to prevent slowdowns from rendering. In the info view, more children can be expanded interactively.

partial def Lean.MessageData.formatAux : NamingContext → Option MessageDataContext → MessageData → BaseIO Format

def Lean.MessageData.format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : BaseIO Format

def Lean.MessageData.toString (msgData : MessageData) : BaseIO String

instance Lean.MessageData.instAppend : Append MessageData

instance Lean.MessageData.instCoeString : Coe String MessageData

instance Lean.MessageData.instCoeFormat : Coe Format MessageData

instance Lean.MessageData.instCoeLevel : Coe Level MessageData

instance Lean.MessageData.instCoeExpr : Coe Expr MessageData

instance Lean.MessageData.instCoeName : Coe Name MessageData

instance Lean.MessageData.instCoeSyntax : Coe Syntax MessageData

instance Lean.MessageData.instCoeMVarId : Coe MVarId MessageData

instance Lean.MessageData.instCoeOptionExpr : Coe (Option Expr) MessageData

partial def Lean.MessageData.arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData

instance Lean.MessageData.instCoeArrayExpr : Coe (Array Expr) MessageData

def Lean.MessageData.bracket (l : String) (f : MessageData) (r : String) : MessageData

Wrap the given message in l and r. See also Format.bracket.

def Lean.MessageData.paren (f : MessageData) : MessageData

Wrap the given message in parentheses ().

def Lean.MessageData.sbracket (f : MessageData) : MessageData

Wrap the given message in square brackets [].

def Lean.MessageData.joinSep : List MessageData → MessageData → MessageData

Append the given list of messages with the given separator.

def Lean.MessageData.ofList : List MessageData → MessageData

Write the given list of messages as a list, separating each item with ,\n and surrounding with square brackets.

def Lean.MessageData.ofArray (msgs : Array MessageData) : MessageData

See MessageData.ofList.

def Lean.MessageData.orList (xs : List MessageData) : MessageData

Puts MessageData into a comma-separated list with "or" at the back (with the serial comma).

Best used on non-empty lists; returns "– none –" for an empty list.

def Lean.MessageData.andList (xs : List MessageData) : MessageData

Puts MessageData into a comma-separated list with "and" at the back (with the serial comma).

Best used on non-empty lists; returns "– none –" for an empty list.

def Lean.MessageData.note (note : MessageData) : MessageData

Produces a labeled note that can be appended to an error message.

def Lean.MessageData.hint' (hint : MessageData) : MessageData

Produces a labeled hint without an associated code action (non-monadic variant of MessageData.hint).

instance Lean.MessageData.instCoeList : Coe (List MessageData) MessageData

instance Lean.MessageData.instCoeListExpr : Coe (List Expr) MessageData

structure Lean.BaseMessage (α : Type u) : Type u

A BaseMessage is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. There are two varieties in the Lean core:

• Message: Uses structured, effectful MessageData for formatting content.
• SerialMessage: Stores pure String data. Obtained by running the effectful Message.serialize.

• fileName : String
• pos : Position
• endPos : Option Position
• keepFullRange : Bool

  If true, report range as given; see msgToInteractiveDiagnostic.

• severity : MessageSeverity
• isSilent : Bool

  If true, filter this message from non-language server output. In the language server, silent messages are served as silent diagnostics. See also DiagnosticWith.isSilent?.

• caption : String
• data : α

  The content of the message.

instance Lean.instInhabitedBaseMessage {a✝ : Type u_1} [Inhabited a✝] : Inhabited (BaseMessage a✝)

instance Lean.instToJsonBaseMessage {α✝ : Type u_1} [ToJson α✝] : ToJson (BaseMessage α✝)

instance Lean.instFromJsonBaseMessage {α✝ : Type} [FromJson α✝] : FromJson (BaseMessage α✝)

@[reducible, inline]

abbrev Lean.Message : Type

A Message is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows.

structure Lean.SerialMessageextends Lean.BaseMessage String : Type

A SerialMessage is a Message whose MessageData has been eagerly serialized and is thus appropriate for use in pure contexts where the effectful MessageData.toString cannot be used.

• fileName : String
• pos : Position
• endPos : Option Position
• keepFullRange : Bool
• severity : MessageSeverity
• isSilent : Bool
• caption : String
• data : String
• kind : Name

  The message kind (i.e., the top-level tag).

instance Lean.instToJsonSerialMessage : ToJson SerialMessage

instance Lean.instFromJsonSerialMessage : FromJson SerialMessage

@[inline]

def Lean.SerialMessage.toMessage (msg : SerialMessage) : Message

def Lean.SerialMessage.toString (msg : SerialMessage) (includeEndPos : Bool := false) : String

instance Lean.SerialMessage.instToString : ToString SerialMessage

@[reducible, inline]

abbrev Lean.Message.kind (msg : Message) : Name

Returns the top-level tag of the message. If none, returns Name.anonymous.

This does not descend into message subtrees (e.g., .compose, .ofLazy). The message kind is expected to describe the whole message.

def Lean.Message.isTrace (msg : Message) : Bool

@[inline]

def Lean.Message.serialize (msg : Message) : BaseIO SerialMessage

Serializes the message, converting its data into a string and saving its kind.

def Lean.Message.toString (msg : Message) (includeEndPos : Bool := false) : BaseIO String

def Lean.Message.toJson (msg : Message) : BaseIO Json

structure Lean.MessageLog : Type

A persistent array of messages.

In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at various points inside a command, which will empty unreported and move its messages to reported. Reported messages are preserved for some specific "lookback" operations such as hasError that should consider the entire message history of the current command; most other functions such as add and toList will only operate on unreported messages.

• reported : PersistentArray Message

  The list of messages already reported (i.e. saved in a Snapshot), in insertion order.

• unreported : PersistentArray Message

  The list of messages not already reported, in insertion order.

• loggedKinds : NameSet

  Set of message kinds that have been added to the log. For example, we have the kind unsafe.exponentiation.warning for warning messages associated with the configuration option exponentiation.threshold. We don't produce a warning if the kind is already in the following set.

instance Lean.instInhabitedMessageLog : Inhabited MessageLog

def Lean.MessageLog.empty : MessageLog

@[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of using `MessageLog.toList/toArray`" (since := "2024-05-22")]

def Lean.MessageLog.msgs : MessageLog → PersistentArray Message

def Lean.MessageLog.reportedPlusUnreported : MessageLog → PersistentArray Message

def Lean.MessageLog.hasUnreported (log : MessageLog) : Bool

def Lean.MessageLog.add (msg : Message) (log : MessageLog) : MessageLog

def Lean.MessageLog.append (l₁ l₂ : MessageLog) : MessageLog

instance Lean.MessageLog.instAppend : Append MessageLog

def Lean.MessageLog.hasErrors (log : MessageLog) : Bool

Checks if either of reported or unreported contains an error, i.e. whether the current command has errored yet.

def Lean.MessageLog.markAllReported (log : MessageLog) : MessageLog

Moves unreported messages to reported.

def Lean.MessageLog.errorsToWarnings (log : MessageLog) : MessageLog

def Lean.MessageLog.errorsToInfos (log : MessageLog) : MessageLog

def Lean.MessageLog.getInfoMessages (log : MessageLog) : MessageLog

def Lean.MessageLog.forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit

def Lean.MessageLog.toList (log : MessageLog) : List Message

Converts the unreported messages to a list, oldest message first.

def Lean.MessageLog.toArray (log : MessageLog) : Array Message

Converts the unreported messages to an array, oldest message first.

def Lean.MessageData.nestD (msg : MessageData) : MessageData

def Lean.indentD (msg : MessageData) : MessageData

def Lean.indentExpr (e : Expr) : MessageData

def Lean.inlineExpr (e : Expr) (maxInlineLength : Nat := 30) : MessageData

Renders an expression e inline in a message unless it will exceed maxInlineLength characters, in which case the expression is indented on a new line.

Note that the output of this function is formatted with preceding and trailing space included. Thus, in m₁ ++ inlineExpr e ++ m₂, m₁ should not end with a space or new line, nor should m₂ begin with one.

def Lean.aquote (msg : MessageData) : MessageData

Atom quotes

class Lean.AddMessageContext (m : Type → Type) : Type

• addMessageContext : MessageData → m MessageData

  Without context, a MessageData object may be missing information (e.g. hover info) for pretty printing, or may print an error. Hence, addMessageContext should be called on all constructed MessageData (e.g. via m!) before taking it out of context (e.g. leaving MetaM or CoreM).

instance Lean.instAddMessageContextOfMonadLift (m n : Type → Type) [MonadLift m n] [AddMessageContext m] : AddMessageContext n

def Lean.addMessageContextPartial {m : Type → Type} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData

def Lean.addMessageContextFull {m : Type → Type} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData

class Lean.ToMessageData (α : Type) : Type

• toMessageData : α → MessageData

def Lean.stringToMessageData (str : String) : MessageData

instance Lean.instToMessageDataOfToFormat {α : Type} [ToFormat α] : ToMessageData α

instance Lean.instToMessageDataExpr : ToMessageData Expr

instance Lean.instToMessageDataLevel : ToMessageData Level

instance Lean.instToMessageDataName : ToMessageData Name

instance Lean.instToMessageDataString : ToMessageData String

instance Lean.instToMessageDataSyntax : ToMessageData Syntax

instance Lean.instToMessageDataTSyntax {k : SyntaxNodeKinds} : ToMessageData (TSyntax k)

instance Lean.instToMessageDataFormat : ToMessageData Format

instance Lean.instToMessageDataMVarId : ToMessageData MVarId

@[defaultInstance 1000]

instance Lean.instToMessageDataMessageData : ToMessageData MessageData

instance Lean.instToMessageDataList {α : Type} [ToMessageData α] : ToMessageData (List α)

instance Lean.instToMessageDataArray {α : Type} [ToMessageData α] : ToMessageData (Array α)

instance Lean.instToMessageDataSubarray {α : Type} [ToMessageData α] : ToMessageData (Subarray α)

instance Lean.instToMessageDataOption {α : Type} [ToMessageData α] : ToMessageData (Option α)

instance Lean.instToMessageDataProd {α β : Type} [ToMessageData α] [ToMessageData β] : ToMessageData (α × β)

instance Lean.instToMessageDataOptionExpr : ToMessageData (Option Expr)

def Lean.termM!_ : ParserDescr

def Lean.toMessageList (msgs : Array MessageData) : MessageData

def Lean.Kernel.Exception.toMessageData (e : Exception) (opts : Options) : MessageData

def Lean.toTraceElem {α : Type} [ToMessageData α] (e : α) (cls : Name := Name.mkSimple "_") : MessageData

Helper functions for creating a MessageData with the given header and elements.