Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.

LSP: Diagnostic; LSP: textDocument/publishDiagnostics

inductive Lean.Lsp.DiagnosticSeverity : Type

• error : DiagnosticSeverity
• warning : DiagnosticSeverity
• information : DiagnosticSeverity
• hint : DiagnosticSeverity

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticSeverity : Inhabited DiagnosticSeverity

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticSeverity : BEq DiagnosticSeverity

def Lean.Lsp.instBEqDiagnosticSeverity.beq : DiagnosticSeverity → DiagnosticSeverity → Bool

def Lean.Lsp.instOrdDiagnosticSeverity.ord : DiagnosticSeverity → DiagnosticSeverity → Ordering

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticSeverity : Ord DiagnosticSeverity

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticSeverity : FromJson DiagnosticSeverity

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticSeverity : ToJson DiagnosticSeverity

inductive Lean.Lsp.DiagnosticCode : Type

Some languages have specific codes for each error type.

• int (i : Int) : DiagnosticCode
• string (s : String) : DiagnosticCode

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticCode : Inhabited DiagnosticCode

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticCode : BEq DiagnosticCode

def Lean.Lsp.instBEqDiagnosticCode.beq : DiagnosticCode → DiagnosticCode → Bool

def Lean.Lsp.instOrdDiagnosticCode.ord : DiagnosticCode → DiagnosticCode → Ordering

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticCode : Ord DiagnosticCode

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticCode : FromJson DiagnosticCode

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticCode : ToJson DiagnosticCode

inductive Lean.Lsp.DiagnosticTag : Type

Tags representing additional metadata about the diagnostic.

• unnecessary : DiagnosticTag

  Unused or unnecessary code. Rendered as faded out eg for unused variables.

• deprecated : DiagnosticTag

  Deprecated or obsolete code. Rendered with a strike-through.

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticTag : Inhabited DiagnosticTag

def Lean.Lsp.instBEqDiagnosticTag.beq : DiagnosticTag → DiagnosticTag → Bool

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticTag : BEq DiagnosticTag

def Lean.Lsp.instOrdDiagnosticTag.ord : DiagnosticTag → DiagnosticTag → Ordering

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticTag : Ord DiagnosticTag

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticTag : FromJson DiagnosticTag

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticTag : ToJson DiagnosticTag

inductive Lean.Lsp.LeanDiagnosticTag : Type

Custom diagnostic tags provided by the language server. We use a separate diagnostic field for this to avoid confusing LSP clients with our custom tags.

• unsolvedGoals : LeanDiagnosticTag

  Diagnostics representing an "unsolved goals" error. Corresponds to MessageData.tagged Tactic.unsolvedGoals ..`.

• goalsAccomplished : LeanDiagnosticTag

  Diagnostics representing a "goals accomplished" silent message. Corresponds to MessageData.tagged goalsAccomplished ..`.

@[implicit_reducible]

instance Lean.Lsp.instInhabitedLeanDiagnosticTag : Inhabited LeanDiagnosticTag

def Lean.Lsp.instBEqLeanDiagnosticTag.beq : LeanDiagnosticTag → LeanDiagnosticTag → Bool

@[implicit_reducible]

instance Lean.Lsp.instBEqLeanDiagnosticTag : BEq LeanDiagnosticTag

@[implicit_reducible]

instance Lean.Lsp.instOrdLeanDiagnosticTag : Ord LeanDiagnosticTag

def Lean.Lsp.instOrdLeanDiagnosticTag.ord : LeanDiagnosticTag → LeanDiagnosticTag → Ordering

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanDiagnosticTag : FromJson LeanDiagnosticTag

@[implicit_reducible]

instance Lean.Lsp.instToJsonLeanDiagnosticTag : ToJson LeanDiagnosticTag

structure Lean.Lsp.DiagnosticRelatedInformation : Type

Represents a related message and source code location for a diagnostic. This should be used to point to code locations that cause or are related to a diagnostics, e.g when duplicating a symbol in a scope.

• location : Location
• message : String

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation : Inhabited DiagnosticRelatedInformation

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticRelatedInformation : BEq DiagnosticRelatedInformation

def Lean.Lsp.instBEqDiagnosticRelatedInformation.beq : DiagnosticRelatedInformation → DiagnosticRelatedInformation → Bool

def Lean.Lsp.instToJsonDiagnosticRelatedInformation.toJson : DiagnosticRelatedInformation → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation : ToJson DiagnosticRelatedInformation

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation : FromJson DiagnosticRelatedInformation

def Lean.Lsp.instFromJsonDiagnosticRelatedInformation.fromJson : Json → Except String DiagnosticRelatedInformation

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticRelatedInformation : Ord DiagnosticRelatedInformation

def Lean.Lsp.instOrdDiagnosticRelatedInformation.ord : DiagnosticRelatedInformation → DiagnosticRelatedInformation → Ordering

structure Lean.Lsp.DiagnosticWith (α : Type) : Type

Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.

LSP accepts a Diagnostic := DiagnosticWith String. The infoview also accepts InteractiveDiagnostic := DiagnosticWith InteractiveMessage.

reference

• range : Range

  The range at which the message applies.

• fullRange? : Option Range

  Extension: preserve semantic range of errors when truncating them for display purposes.

• severity? : Option DiagnosticSeverity
• isSilent? : Option Bool

  Extension: whether this diagnostic should not be displayed as a regular diagnostic in the editor. In VS Code, this means that the diagnostic does not have a squiggly and is not displayed in the InfoView under 'All Messages', but it is still displayed under 'Messages'. Defaults to false.

• code? : Option DiagnosticCode

  The diagnostic's code, which might appear in the user interface.

• source? : Option String

  A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.

• message : α

  Parametrised by the type of message data. LSP diagnostics use String, whereas in Lean's interactive diagnostics we use the type of widget-enriched text. See Lean.Widget.InteractiveDiagnostic.

• tags? : Option (Array DiagnosticTag)

  Additional metadata about the diagnostic.

• leanTags? : Option (Array LeanDiagnosticTag)

  Additional Lean-specific metadata about the diagnostic.

• relatedInformation? : Option (Array DiagnosticRelatedInformation)

  An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property.

• data? : Option Json

  A data entry field that is preserved between a textDocument/publishDiagnostics notification and textDocument/codeAction request.

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticWith {a✝ : Type} [Inhabited a✝] : Inhabited (DiagnosticWith a✝)

def Lean.Lsp.instBEqDiagnosticWith.beq {α✝ : Type} [BEq α✝] : DiagnosticWith α✝ → DiagnosticWith α✝ → Bool

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticWith {α✝ : Type} [BEq α✝] : BEq (DiagnosticWith α✝)

def Lean.Lsp.instToJsonDiagnosticWith.toJson {α✝ : Type} [ToJson α✝] : DiagnosticWith α✝ → Json

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticWith {α✝ : Type} [ToJson α✝] : ToJson (DiagnosticWith α✝)

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticWith {α✝ : Type} [FromJson α✝] : FromJson (DiagnosticWith α✝)

def Lean.Lsp.instFromJsonDiagnosticWith.fromJson {α✝ : Type} [FromJson α✝] : Json → Except String (DiagnosticWith α✝)

def Lean.Lsp.DiagnosticWith.fullRange {α : Type} (d : DiagnosticWith α) : Range

@[reducible, inline]

abbrev Lean.Lsp.Diagnostic : Type

structure Lean.Lsp.PublishDiagnosticsParams : Type

Parameters for the textDocument/publishDiagnostics notification.

• uri : DocumentUri
• version? : Option Int
• isIncremental? : Option Bool

  Whether the client should append this set of diagnostics to the previous set rather than replacing the previous set by this one (the default LSP behavior). false means the client should replace. none is equivalent to false. This is a Lean-specific extension (see LeanClientCapabilities).

• diagnostics : Array Diagnostic

@[implicit_reducible]

instance Lean.Lsp.instInhabitedPublishDiagnosticsParams : Inhabited PublishDiagnosticsParams

def Lean.Lsp.instBEqPublishDiagnosticsParams.beq : PublishDiagnosticsParams → PublishDiagnosticsParams → Bool

@[implicit_reducible]

instance Lean.Lsp.instBEqPublishDiagnosticsParams : BEq PublishDiagnosticsParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonPublishDiagnosticsParams : ToJson PublishDiagnosticsParams

def Lean.Lsp.instToJsonPublishDiagnosticsParams.toJson : PublishDiagnosticsParams → Json

def Lean.Lsp.instFromJsonPublishDiagnosticsParams.fromJson : Json → Except String PublishDiagnosticsParams

@[implicit_reducible]

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams : FromJson PublishDiagnosticsParams