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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
inductive Lean.MessageSeverity :
Type

- information : MessageSeverity
- warning : MessageSeverity
- error : MessageSeverity

Instances For

source
instance Lean.instInhabitedMessageSeverity :
Inhabited MessageSeverity
Equations

- Lean.instInhabitedMessageSeverity = { default := Lean.instInhabitedMessageSeverity.default }

source
def Lean.instInhabitedMessageSeverity.default :
MessageSeverity
Equations

- Lean.instInhabitedMessageSeverity.default = Lean.MessageSeverity.information

Instances For

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

- Lean.instBEqMessageSeverity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance Lean.instBEqMessageSeverity :
BEq MessageSeverity
Equations

- Lean.instBEqMessageSeverity = { beq := Lean.instBEqMessageSeverity.beq }

source
instance Lean.instToJsonMessageSeverity :
ToJson MessageSeverity
Equations

- Lean.instToJsonMessageSeverity = { toJson := Lean.instToJsonMessageSeverity.toJson }

source
def Lean.instToJsonMessageSeverity.toJson :
MessageSeverity → Json
Equations

- Lean.instToJsonMessageSeverity.toJson Lean.MessageSeverity.information = Lean.toJson "information"
- Lean.instToJsonMessageSeverity.toJson Lean.MessageSeverity.warning = Lean.toJson "warning"
- Lean.instToJsonMessageSeverity.toJson Lean.MessageSeverity.error = Lean.toJson "error"

Instances For

source
instance Lean.instFromJsonMessageSeverity :
FromJson MessageSeverity
Equations

- Lean.instFromJsonMessageSeverity = { fromJson? := Lean.instFromJsonMessageSeverity.fromJson }

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.MessageSeverity.toString :
MessageSeverity → String
Equations

- Lean.MessageSeverity.information.toString = "information"
- Lean.MessageSeverity.warning.toString = "warning"
- Lean.MessageSeverity.error.toString = "error"

Instances For

source
instance Lean.instToStringMessageSeverity :
ToString MessageSeverity
Equations

- Lean.instToStringMessageSeverity = { toString := Lean.MessageSeverity.toString }

source
structure Lean.MessageDataContext :
Type

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

source
def Lean.instInhabitedMessageData.default :
MessageData
Equations

- Lean.instInhabitedMessageData.default = Lean.MessageData.ofGoal default

Instances For

source
instance Lean.instInhabitedMessageData :
Inhabited MessageData
Equations

- Lean.instInhabitedMessageData = { default := Lean.instInhabitedMessageData.default }

source
instance Lean.instTypeNameMessageData :
TypeName MessageData
Equations

- Lean.instTypeNameMessageData = Lean.inst✝

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

Eagerly formatted text.

Equations

- Lean.MessageData.ofFormat fmt = Lean.MessageData.ofFormatWithInfos { fmt := fmt, infos := Std.TreeMap.empty }

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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`.

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

Equations

- (Lean.MessageData.withContext a msg).kind = msg.kind
- (Lean.MessageData.withNamingContext a msg).kind = msg.kind
- (Lean.MessageData.tagged n a).kind = n
- x✝.kind = Lean.Name.anonymous

Instances For

source
def Lean.MessageData.isTrace :
MessageData → Bool
Equations

- (Lean.MessageData.withContext a msg).isTrace = msg.isTrace
- (Lean.MessageData.withNamingContext a msg).isTrace = msg.isTrace
- (Lean.MessageData.tagged a msg).isTrace = msg.isTrace
- (Lean.MessageData.trace data msg children).isTrace = true
- x✝.isTrace = false

Instances For

source
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`.

Equations

- (Lean.MessageData.withContext ctx msg).composePreservingKind x✝ = Lean.MessageData.withContext ctx (msg.composePreservingKind x✝)
- (Lean.MessageData.withNamingContext nc msg).composePreservingKind x✝ = Lean.MessageData.withNamingContext nc (msg.composePreservingKind x✝)
- (Lean.MessageData.tagged t msg).composePreservingKind x✝ = Lean.MessageData.tagged t (msg.compose x✝)
- x✝¹.composePreservingKind x✝ = x✝¹.compose x✝

Instances For

source
def Lean.MessageData.nil :
MessageData

An empty message.

Equations

- Lean.MessageData.nil = Lean.MessageData.ofFormat Std.Format.nil

Instances For

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

- Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

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

Equations

- Lean.MessageData.ofName n = Lean.MessageData.ofFormat (Std.format n)

Instances For

source
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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- msg.hasSyntheticSorry = Lean.MessageData.hasSyntheticSorry.visit✝ none msg

Instances For

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

source
partial def Lean.MessageData.formatAux :
NamingContext → Option MessageDataContext → MessageData → BaseIO Format
source
def Lean.MessageData.format (msgData : MessageData) (ctx? : Option MessageDataContext := none) :
BaseIO Format
Equations

- msgData.format ctx? = Lean.MessageData.formatAux { currNamespace := Lean.Name.anonymous, openDecls := [] } ctx? msgData

Instances For

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

- msgData.toString = do let __do_lift ← msgData.format pure (toString __do_lift)

Instances For

source
instance Lean.MessageData.instAppend :
Append MessageData
Equations

- Lean.MessageData.instAppend = { append := Lean.MessageData.compose }

source
instance Lean.MessageData.instCoeString :
Coe String MessageData
Equations

- Lean.MessageData.instCoeString = { coe := Lean.MessageData.ofFormat ∘ Std.format }

source
instance Lean.MessageData.instCoeFormat :
Coe Format MessageData
Equations

- Lean.MessageData.instCoeFormat = { coe := Lean.MessageData.ofFormat }

source
instance Lean.MessageData.instCoeLevel :
Coe Level MessageData
Equations

- Lean.MessageData.instCoeLevel = { coe := Lean.MessageData.ofLevel }

source
instance Lean.MessageData.instCoeExpr :
Coe Expr MessageData
Equations

- Lean.MessageData.instCoeExpr = { coe := Lean.MessageData.ofExpr }

source
instance Lean.MessageData.instCoeName :
Coe Name MessageData
Equations

- Lean.MessageData.instCoeName = { coe := Lean.MessageData.ofName }

source
instance Lean.MessageData.instCoeSyntax :
Coe Syntax MessageData
Equations

- Lean.MessageData.instCoeSyntax = { coe := Lean.MessageData.ofSyntax }

source
instance Lean.MessageData.instCoeMVarId :
Coe MVarId MessageData
Equations

- Lean.MessageData.instCoeMVarId = { coe := Lean.MessageData.ofGoal }

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

- One or more equations did not get rendered due to their size.

source
partial def Lean.MessageData.arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) :
MessageData
source
instance Lean.MessageData.instCoeArrayExpr :
Coe (Array Expr) MessageData
Equations

- Lean.MessageData.instCoeArrayExpr = { coe := fun (es : Array Lean.Expr) => Lean.MessageData.arrayExpr.toMessageData es 0 ((Lean.MessageData.ofFormat ∘ Std.format) "#[") }

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

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

Equations

- Lean.MessageData.bracket l f r = (Lean.MessageData.nest l.length ((Lean.MessageData.ofFormat ∘ Std.format) l ++ f ++ (Lean.MessageData.ofFormat ∘ Std.format) r)).group

Instances For

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

Wrap the given message in parentheses `()`.

Equations

- f.paren = Lean.MessageData.bracket "(" f ")"

Instances For

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

Wrap the given message in square brackets `[]`.

Equations

- f.sbracket = Lean.MessageData.bracket "[" f "]"

Instances For

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

Append the given list of messages with the given separator.

Equations

- Lean.MessageData.joinSep [] x✝ = Lean.MessageData.ofFormat Std.Format.nil
- Lean.MessageData.joinSep [a] x✝ = a
- Lean.MessageData.joinSep (a :: as) x✝ = a ++ x✝ ++ Lean.MessageData.joinSep as x✝

Instances For

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

Equations

- Lean.MessageData.ofList [] = (Lean.MessageData.ofFormat ∘ Std.format) "[]"
- Lean.MessageData.ofList x✝ = (Lean.MessageData.joinSep x✝ (Lean.MessageData.ofFormat (Std.Format.text ",") ++ Lean.MessageData.ofFormat Std.Format.line)).sbracket

Instances For

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

See `MessageData.ofList`.

Equations

- Lean.MessageData.ofArray msgs = Lean.MessageData.ofList msgs.toList

Instances For

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

Equations

- Lean.MessageData.orList [] = (Lean.MessageData.ofFormat ∘ Std.format) "– none –"
- Lean.MessageData.orList [x] = x
- Lean.MessageData.orList [x₀, x₁] = x₀ ++ (Lean.MessageData.ofFormat ∘ Std.format) " or " ++ x₁
- Lean.MessageData.orList xs = Lean.MessageData.joinSep xs.dropLast ((Lean.MessageData.ofFormat ∘ Std.format) ", ") ++ (Lean.MessageData.ofFormat ∘ Std.format) ", or " ++ xs.getLast!

Instances For

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

Equations

- Lean.MessageData.andList [] = (Lean.MessageData.ofFormat ∘ Std.format) "– none –"
- Lean.MessageData.andList [x] = x
- Lean.MessageData.andList [x₀, x₁] = x₀ ++ (Lean.MessageData.ofFormat ∘ Std.format) " and " ++ x₁
- Lean.MessageData.andList xs = Lean.MessageData.joinSep xs.dropLast ((Lean.MessageData.ofFormat ∘ Std.format) ", ") ++ (Lean.MessageData.ofFormat ∘ Std.format) ", and " ++ xs.getLast!

Instances For

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

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

Equations

- note.note = Lean.MessageData.ofFormat Std.Format.line ++ Lean.MessageData.ofFormat Std.Format.line ++ (Lean.MessageData.ofFormat ∘ Std.format) "Note: " ++ note

Instances For

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

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

Equations

- hint.hint' = Lean.MessageData.ofFormat Std.Format.line ++ Lean.MessageData.ofFormat Std.Format.line ++ (Lean.MessageData.ofFormat ∘ Std.format) "Hint: " ++ hint

Instances For

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

- Lean.MessageData.instCoeList = { coe := Lean.MessageData.ofList }

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

- Lean.MessageData.instCoeListExpr = { coe := fun (es : List Lean.Expr) => Lean.MessageData.ofList (List.map Lean.MessageData.ofExpr es) }

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

Instances For

source
def Lean.instInhabitedBaseMessage.default {a✝ : Type u_1} [Inhabited a✝] :
BaseMessage a✝
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- Lean.instInhabitedBaseMessage = { default := Lean.instInhabitedBaseMessage.default }

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

- Lean.instToJsonBaseMessage = { toJson := Lean.instToJsonBaseMessage.toJson }

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

- One or more equations did not get rendered due to their size.

Instances For

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

- Lean.instFromJsonBaseMessage = { fromJson? := Lean.instFromJsonBaseMessage.fromJson }

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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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.

Equations

- Lean.Message = Lean.BaseMessage Lean.MessageData

Instances For

source
structure Lean.SerialMessage extends 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).

Instances For

source
def Lean.instToJsonSerialMessage.toJson :
SerialMessage → Json
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.instToJsonSerialMessage :
ToJson SerialMessage
Equations

- Lean.instToJsonSerialMessage = { toJson := Lean.instToJsonSerialMessage.toJson }

source
instance Lean.instFromJsonSerialMessage :
FromJson SerialMessage
Equations

- Lean.instFromJsonSerialMessage = { fromJson? := Lean.instFromJsonSerialMessage.fromJson }

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.errorNameSuffix :
String

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

Equations

- Lean.errorNameSuffix = "_namedError"

Instances For

source
def Lean.kindOfErrorName (errorName : Name) :
Name

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

Equations

- Lean.kindOfErrorName errorName = errorName.str Lean.errorNameSuffix

Instances For

source
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`.

Equations

- msg.tagWithErrorName name = Lean.MessageData.tagged (Lean.kindOfErrorName name) msg

Instances For

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

Equations

- Lean.errorNameOfKind? (p.str last) = if (last == Lean.errorNameSuffix) = true then some p else none
- Lean.errorNameOfKind? x✝ = none

Instances For

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

Equations

- msg.errorName? = Lean.errorNameOfKind? msg.kind

Instances For

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

Equations

- msg.errorName? = msg.data.errorName?

Instances For

source
@[inline]
def Lean.SerialMessage.toMessage (msg : SerialMessage) :
Message
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
instance Lean.SerialMessage.instToString :
ToString SerialMessage
Equations

- Lean.SerialMessage.instToString = { toString := fun (msg : Lean.SerialMessage) => msg.toString }

source
@[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.

Equations

- msg.kind = msg.data.kind

Instances For

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

- msg.isTrace = msg.data.isTrace

Instances For

source
@[inline]
def Lean.Message.serialize (msg : Message) :
BaseIO SerialMessage

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- msg.toString includeEndPos = do let __do_lift ← msg.serialize pure (inline (__do_lift.toString includeEndPos))

Instances For

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

- msg.toJson = do let __do_lift ← msg.serialize pure (inline (Lean.toJson __do_lift))

Instances For

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

Instances For

source
def Lean.instInhabitedMessageLog.default :
MessageLog
Equations

- Lean.instInhabitedMessageLog.default = { reported := default, unreported := default, loggedKinds := default }

Instances For

source
instance Lean.instInhabitedMessageLog :
Inhabited MessageLog
Equations

- Lean.instInhabitedMessageLog = { default := Lean.instInhabitedMessageLog.default }

source
def Lean.MessageLog.empty :
MessageLog
Equations

- Lean.MessageLog.empty = { }

Instances For

source
@[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
Equations

- Lean.MessageLog.msgs = Lean.MessageLog.unreported

Instances For

source
def Lean.MessageLog.reportedPlusUnreported :
MessageLog → PersistentArray Message
Equations

- { reported := r, unreported := u, loggedKinds := loggedKinds }.reportedPlusUnreported = r ++ u

Instances For

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

- log.hasUnreported = !log.unreported.isEmpty

Instances For

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

- Lean.MessageLog.add msg log = { reported := log.reported, unreported := log.unreported.push msg, loggedKinds := log.loggedKinds }

Instances For

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

- l₁.append l₂ = { reported := l₁.reported ++ l₂.reported, unreported := l₁.unreported ++ l₂.unreported, loggedKinds := Std.TreeSet.merge l₁.loggedKinds l₂.loggedKinds }

Instances For

source
instance Lean.MessageLog.instAppend :
Append MessageLog
Equations

- Lean.MessageLog.instAppend = { append := Lean.MessageLog.append }

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Moves `unreported` messages to `reported`.

Equations

- log.markAllReported = { reported := log.reported ++ log.unreported, loggedKinds := log.loggedKinds }

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- log.forM f = log.unreported.forM f

Instances For

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

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

Equations

- log.toList = log.unreported.toList

Instances For

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

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

Equations

- log.toArray = log.unreported.toArray

Instances For

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

- msg.nestD = Lean.MessageData.nest 2 msg

Instances For

source
def Lean.indentD (msg : MessageData) :
MessageData
Equations

- Lean.indentD msg = (Lean.MessageData.ofFormat Std.Format.line ++ msg).nestD

Instances For

source
def Lean.indentExpr (e : Expr) :
MessageData
Equations

- Lean.indentExpr e = Lean.indentD (Lean.MessageData.ofExpr e)

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.aquote (msg : MessageData) :
MessageData

Atom quotes

Equations

- Lean.aquote msg = (Lean.MessageData.ofFormat ∘ Std.format) "「" ++ msg ++ (Lean.MessageData.ofFormat ∘ Std.format) "」"

Instances For

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

Instances

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

- Lean.instAddMessageContextOfMonadLift m n = { addMessageContext := fun (msg : Lean.MessageData) => liftM (Lean.addMessageContext msg) }

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

- Lean.addMessageContextPartial msgData = do let env ← Lean.getEnv let opts ← Lean.getOptions pure (Lean.MessageData.withContext { env := env, mctx := { }, lctx := { }, opts := opts } msgData)

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
class Lean.ToMessageData (α : Type) :
Type

- toMessageData : α → MessageData

Instances

source
def Lean.stringToMessageData (str : String) :
MessageData
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- Lean.instToMessageDataOfToFormat = { toMessageData := Lean.MessageData.ofFormat ∘ Std.format }

source
instance Lean.instToMessageDataExpr :
ToMessageData Expr
Equations

- Lean.instToMessageDataExpr = { toMessageData := Lean.MessageData.ofExpr }

source
instance Lean.instToMessageDataLevel :
ToMessageData Level
Equations

- Lean.instToMessageDataLevel = { toMessageData := Lean.MessageData.ofLevel }

source
instance Lean.instToMessageDataName :
ToMessageData Name
Equations

- Lean.instToMessageDataName = { toMessageData := Lean.MessageData.ofName }

source
instance Lean.instToMessageDataString :
ToMessageData String
Equations

- Lean.instToMessageDataString = { toMessageData := Lean.stringToMessageData }

source
instance Lean.instToMessageDataSyntax :
ToMessageData Syntax
Equations

- Lean.instToMessageDataSyntax = { toMessageData := Lean.MessageData.ofSyntax }

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

- Lean.instToMessageDataTSyntax = { toMessageData := fun (x : Lean.TSyntax k) => Lean.MessageData.ofSyntax x.raw }

source
instance Lean.instToMessageDataFormat :
ToMessageData Format
Equations

- Lean.instToMessageDataFormat = { toMessageData := Lean.MessageData.ofFormat }

source
instance Lean.instToMessageDataMVarId :
ToMessageData MVarId
Equations

- Lean.instToMessageDataMVarId = { toMessageData := Lean.MessageData.ofGoal }

source
@[defaultInstance 1000]
instance Lean.instToMessageDataMessageData :
ToMessageData MessageData
Equations

- Lean.instToMessageDataMessageData = { toMessageData := id }

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

- Lean.instToMessageDataList = { toMessageData := fun (as : List α) => Lean.MessageData.ofList (List.map Lean.toMessageData as) }

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

- Lean.instToMessageDataArray = { toMessageData := fun (as : Array α) => Lean.toMessageData as.toList }

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

- Lean.instToMessageDataSubarray = { toMessageData := fun (as : Subarray α) => Lean.toMessageData (Std.Slice.toList as) }

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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
instance Lean.instToMessageDataOptionExpr :
ToMessageData (Option Expr)
Equations

- One or more equations did not get rendered due to their size.

source
def Lean.termM!_ :
ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- Lean.toMessageList msgs = Lean.indentD (Lean.MessageData.joinSep msgs.toList (Lean.toMessageData "\n\n"))

Instances For

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

- One or more equations did not get rendered due to their size.
- (Lean.Kernel.Exception.other msg).toMessageData opts = Lean.toMessageData "(kernel) " ++ Lean.toMessageData msg
- Lean.Kernel.Exception.deterministicTimeout.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) deterministic timeout"
- Lean.Kernel.Exception.excessiveMemory.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) excessive memory consumption detected"
- Lean.Kernel.Exception.deepRecursion.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) deep recursion detected"
- Lean.Kernel.Exception.interrupted.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) interrupted"

Instances For

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

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

Equations

- Lean.toTraceElem e cls = Lean.MessageData.trace { cls := cls } (Lean.toMessageData e) #[]

Instances For