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

Creates a string describing an error message msg produced at pos, optionally ending at endPos, in fileName.

Additional optional arguments can be used to prepend a label kind describing the severity of the error (e.g., "warning" or "error") and a bracketed name label displaying the name of the error if it has one.

inductive Lean.MessageSeverity : Type

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

@[instance_reducible]

instance Lean.instInhabitedMessageSeverity : Inhabited MessageSeverity

def Lean.instBEqMessageSeverity.beq : MessageSeverity → MessageSeverity → Bool

@[instance_reducible]

instance Lean.instBEqMessageSeverity : BEq MessageSeverity

def Lean.instToJsonMessageSeverity.toJson : MessageSeverity → Json

@[instance_reducible]

instance Lean.instToJsonMessageSeverity : ToJson MessageSeverity

@[instance_reducible]

instance Lean.instFromJsonMessageSeverity : FromJson MessageSeverity

def Lean.instFromJsonMessageSeverity.fromJson : Json → Except String MessageSeverity

def Lean.MessageSeverity.toString : MessageSeverity → String

@[instance_reducible]

instance Lean.instToStringMessageSeverity : ToString 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

inductive Lean.TraceResult : Type

Structured result status of a trace node action, produced by withTraceNode and withTraceNodeBefore and included in the TraceData of trace messages. Either .success (✅️), .failure (❌️), or .error (💥️).

This is used both to render emojis in trace messages and to allow more robust inspection of trace logs via metaprogramming.

See also Except.toTraceResult for converting an Except ε α to a TraceResult.

• success : TraceResult

  The traced action succeeded (✅️, checkEmoji).

• failure : TraceResult

  The traced action failed (❌️, crossEmoji).

• error : TraceResult

  An exception was thrown during the traced action (💥️, bombEmoji).

@[instance_reducible]

instance Lean.instInhabitedTraceResult : Inhabited TraceResult

@[instance_reducible]

instance Lean.instBEqTraceResult : BEq TraceResult

def Lean.instBEqTraceResult.beq : TraceResult → TraceResult → Bool

@[instance_reducible]

instance Lean.instReprTraceResult : Repr TraceResult

def Lean.instReprTraceResult.repr : TraceResult → Nat → Format

def Lean.TraceResult.toEmoji : TraceResult → String

Convert a TraceResult to its emoji representation.

structure Lean.TraceData : Type

• cls : Name

  Trace class, e.g. Elab.step.

• result? : Option TraceResult

  Structured success/failure result set by withTraceNode/withTraceNodeBefore. none for trace nodes not created by these functions (e.g. addTrace, diagnostic nodes).

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

• ofOriginatingSyntax : Syntax → MessageData → MessageData

  Preserves the originating syntax of the message.

@[instance_reducible]

instance Lean.instInhabitedMessageData : Inhabited MessageData

@[instance_reducible]

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 (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.originatingSyntax? : MessageData → Option Syntax × MessageData

def Lean.MessageData.isTrace : MessageData → Bool

def Lean.MessageData.composePreservingKind : MessageData → MessageData → MessageData

composePreservingKind msg msg' appends the contents of msg' to the end of msg but ensures that the resulting message preserves the kind (as given by MessageData.kind) of msg.

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.withExprHover (fmt : Format) (expr : Expr) (lctx : LocalContext) (location? : Option DeclarationLocation := none) (docString? : Option String := none) (mkDocString? : Option (PPContext → IO String) := none) (explicit : Bool := false) : MessageData

Creates message data wrapping fmt that gives information about expr when hovered over.

Options:

• location? overrides what "go to definition" does
• docString? allows overriding the docstring for the expression
• mkDocString? allows generating a dynamic docstring; if this is provided, docString? is ignored
• explicit makes the hover pretty print the head application in explicit mode; the default value is false (note: delaboration expression hovers normally set this to true, since their purpose is to get more information about a given expression)

def Lean.MessageData.withExprHoverM {m : Type → Type} [Monad m] [MonadLCtx m] (fmt : Format) (expr : Expr) (lctx? : Option LocalContext := none) (location? : Option DeclarationLocation := none) (docString? : Option String := none) (mkDocString? : Option (PPContext → IO String) := none) (explicit : Bool := false) : m MessageData

Calls withExprHover, but uses the current local context if one is not given. See withExprHover for a description of each parameter.

def Lean.MessageData.ofUserName {m : Type → Type} [Monad m] [MonadLCtx m] (userName : Name) : m MessageData

Render userName as MessageData, attaching hover information for the local declaration with that user-facing name if it is bound in the current LocalContext. The lookup uses userName verbatim (so macro scopes are preserved for matching) and the rendered name uses userName.simpMacroScopes. Falls back to plain text when the variable is not in scope.

def Lean.MessageData.hasSyntheticSorry (msg : 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_reducible]

instance Lean.MessageData.instAppend : Append MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeString : Coe String MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeFormat : Coe Format MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeLevel : Coe Level MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeExpr : Coe Expr MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeName : Coe Name MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeSyntax : Coe Syntax MessageData

@[instance_reducible]

instance Lean.MessageData.instCoeMVarId : Coe MVarId MessageData

@[instance_reducible]

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

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

@[instance_reducible]

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

def Lean.instToJsonBaseMessage.toJson {α✝ : Type u_1} [ToJson α✝] : BaseMessage α✝ → Json

def Lean.instFromJsonBaseMessage.fromJson {α✝ : Type} [FromJson α✝] : Json → Except String (BaseMessage α✝)

@[instance_reducible]

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

def Lean.instToJsonSerialMessage.toJson : SerialMessage → Json

@[instance_reducible]

instance Lean.instToJsonSerialMessage : ToJson SerialMessage

def Lean.instFromJsonSerialMessage.fromJson : Json → Except String SerialMessage

@[instance_reducible]

instance Lean.instFromJsonSerialMessage : FromJson SerialMessage

def Lean.errorNameSuffix : String

A suffix added to diagnostic name-containing tags to indicate that they should be used as an error code.

def Lean.kindOfErrorName (errorName : Name) : Name

Creates a tag (i.e., message kind) for an error message with (user-facing) name errorName.

def Lean.MessageData.tagWithErrorName (msg : MessageData) (name : Name) : MessageData

Produces a MessageData tagged with an identifier for error name.

Note: this function generally should not be called directly; instead, use the macros logNamedError and throwNamedError.

def Lean.MessageData.stripNestedTags : MessageData → MessageData

Strip the `nested prefix components added to tags by throwNestedTacticEx.

def Lean.errorNameOfKind? : Name → Option Name

If the provided name is labeled as a diagnostic name, removes the label and returns the corresponding diagnostic name.

Note: we use this labeling mechanism so that we can have error kinds that are not intended to be shown to the user, without having to validate the presence of an error explanation at runtime.

def Lean.MessageData.errorName? (msg : MessageData) : Option Name

Returns the error name with which msg is tagged, if one exists.

Note that this is distinct from msg.kind: the kind of a named-error message is not equal to its name, and there exist message kinds that are not error-name kinds.

def Lean.Message.errorName? (msg : Message) : Option Name

Returns the error name with which msg is tagged, if one exists.

Note that this is distinct from msg.kind: the kind of a named-error message is not equal to its name, and there exist message kinds that are not error-name kinds.

@[inline]

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

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

@[instance_reducible]

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

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

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.getWarningMessages (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.inlineExprTrailing (e : Expr) (maxInlineLength : Nat := 30) : MessageData

See Lean.inlineExpr. This variation is to be used when the expression is the trailing element of a message; it does not append a newline or space after the expression.

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

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

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

@[instance_reducible]

instance Lean.instToMessageDataExpr : ToMessageData Expr

@[instance_reducible]

instance Lean.instToMessageDataLevel : ToMessageData Level

@[instance_reducible]

instance Lean.instToMessageDataName : ToMessageData Name

@[instance_reducible]

instance Lean.instToMessageDataString : ToMessageData String

@[instance_reducible]

instance Lean.instToMessageDataSyntax : ToMessageData Syntax

@[instance_reducible]

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

@[instance_reducible]

instance Lean.instToMessageDataFormat : ToMessageData Format

@[instance_reducible]

instance Lean.instToMessageDataMVarId : ToMessageData MVarId

@[instance_reducible, defaultInstance 1000]

instance Lean.instToMessageDataMessageData : ToMessageData MessageData

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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.