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

instance Lean.Lsp.instInhabitedDiagnosticSeverity : Inhabited DiagnosticSeverity

Equations

• Lean.Lsp.instInhabitedDiagnosticSeverity = { default := Lean.Lsp.DiagnosticSeverity.error }

instance Lean.Lsp.instBEqDiagnosticSeverity : BEq DiagnosticSeverity

Equations

• Lean.Lsp.instBEqDiagnosticSeverity = { beq := Lean.Lsp.beqDiagnosticSeverity✝ }

instance Lean.Lsp.instOrdDiagnosticSeverity : Ord DiagnosticSeverity

Equations

• Lean.Lsp.instOrdDiagnosticSeverity = { compare := Lean.Lsp.ordDiagnosticSeverity✝ }

instance Lean.Lsp.instFromJsonDiagnosticSeverity : FromJson DiagnosticSeverity

Equations

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

instance Lean.Lsp.instToJsonDiagnosticSeverity : ToJson DiagnosticSeverity

Equations

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

inductive Lean.Lsp.DiagnosticCode : Type

Some languages have specific codes for each error type.

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

instance Lean.Lsp.instInhabitedDiagnosticCode : Inhabited DiagnosticCode

Equations

• Lean.Lsp.instInhabitedDiagnosticCode = { default := Lean.Lsp.DiagnosticCode.int default }

instance Lean.Lsp.instBEqDiagnosticCode : BEq DiagnosticCode

Equations

• Lean.Lsp.instBEqDiagnosticCode = { beq := Lean.Lsp.beqDiagnosticCode✝ }

instance Lean.Lsp.instOrdDiagnosticCode : Ord DiagnosticCode

Equations

• Lean.Lsp.instOrdDiagnosticCode = { compare := Lean.Lsp.ordDiagnosticCode✝ }

instance Lean.Lsp.instFromJsonDiagnosticCode : FromJson DiagnosticCode

Equations

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

instance Lean.Lsp.instToJsonDiagnosticCode : ToJson DiagnosticCode

Equations

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

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.

instance Lean.Lsp.instInhabitedDiagnosticTag : Inhabited DiagnosticTag

Equations

• Lean.Lsp.instInhabitedDiagnosticTag = { default := Lean.Lsp.DiagnosticTag.unnecessary }

instance Lean.Lsp.instBEqDiagnosticTag : BEq DiagnosticTag

Equations

• Lean.Lsp.instBEqDiagnosticTag = { beq := Lean.Lsp.beqDiagnosticTag✝ }

instance Lean.Lsp.instOrdDiagnosticTag : Ord DiagnosticTag

Equations

• Lean.Lsp.instOrdDiagnosticTag = { compare := Lean.Lsp.ordDiagnosticTag✝ }

instance Lean.Lsp.instFromJsonDiagnosticTag : FromJson DiagnosticTag

Equations

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

instance Lean.Lsp.instToJsonDiagnosticTag : ToJson DiagnosticTag

Equations

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

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

instance Lean.Lsp.instInhabitedLeanDiagnosticTag : Inhabited LeanDiagnosticTag

Equations

• Lean.Lsp.instInhabitedLeanDiagnosticTag = { default := Lean.Lsp.LeanDiagnosticTag.unsolvedGoals }

instance Lean.Lsp.instBEqLeanDiagnosticTag : BEq LeanDiagnosticTag

Equations

• Lean.Lsp.instBEqLeanDiagnosticTag = { beq := Lean.Lsp.beqLeanDiagnosticTag✝ }

instance Lean.Lsp.instOrdLeanDiagnosticTag : Ord LeanDiagnosticTag

Equations

• Lean.Lsp.instOrdLeanDiagnosticTag = { compare := Lean.Lsp.ordLeanDiagnosticTag✝ }

instance Lean.Lsp.instFromJsonLeanDiagnosticTag : FromJson LeanDiagnosticTag

Equations

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

instance Lean.Lsp.instToJsonLeanDiagnosticTag : ToJson LeanDiagnosticTag

Equations

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

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

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation : Inhabited DiagnosticRelatedInformation

Equations

• Lean.Lsp.instInhabitedDiagnosticRelatedInformation = { default := { location := default, message := default } }

instance Lean.Lsp.instBEqDiagnosticRelatedInformation : BEq DiagnosticRelatedInformation

Equations

• Lean.Lsp.instBEqDiagnosticRelatedInformation = { beq := Lean.Lsp.beqDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation : ToJson DiagnosticRelatedInformation

Equations

• Lean.Lsp.instToJsonDiagnosticRelatedInformation = { toJson := Lean.Lsp.toJsonDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation : FromJson DiagnosticRelatedInformation

Equations

• Lean.Lsp.instFromJsonDiagnosticRelatedInformation = { fromJson? := Lean.Lsp.fromJsonDiagnosticRelatedInformation✝ }

instance Lean.Lsp.instOrdDiagnosticRelatedInformation : Ord DiagnosticRelatedInformation

Equations

• Lean.Lsp.instOrdDiagnosticRelatedInformation = { compare := Lean.Lsp.ordDiagnosticRelatedInformation✝ }

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 (TaggedText MsgEmbed).

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.

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

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticWith = { beq := Lean.Lsp.beqDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instToJsonDiagnosticWith = { toJson := Lean.Lsp.toJsonDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instFromJsonDiagnosticWith = { fromJson? := Lean.Lsp.fromJsonDiagnosticWith✝ }

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

Equations

• d.fullRange = d.fullRange?.getD d.range

instance Lean.Lsp.DiagnosticWith.instOrdUserVisible {α✝ : Type} [Ord α✝] : Ord (Lean.Lsp.DiagnosticWith.UserVisible✝ α✝)

Equations

• Lean.Lsp.DiagnosticWith.instOrdUserVisible = { compare := Lean.Lsp.DiagnosticWith.ordUserVisible✝ }

def Lean.Lsp.compareByUserVisible {α : Type} [Ord α] (a b : DiagnosticWith α) : Ordering

Compares DiagnosticWith instances modulo non-user-facing properties.

Equations

• Lean.Lsp.compareByUserVisible a b = compare (Lean.Lsp.DiagnosticWith.UserVisible.ofDiagnostic✝ a) (Lean.Lsp.DiagnosticWith.UserVisible.ofDiagnostic✝ b)

@[reducible, inline]

abbrev Lean.Lsp.Diagnostic : Type

Equations

• Lean.Lsp.Diagnostic = Lean.Lsp.DiagnosticWith String

structure Lean.Lsp.PublishDiagnosticsParams : Type

Parameters for the textDocument/publishDiagnostics notification.

• uri : DocumentUri
• version? : Option Int
• diagnostics : Array Diagnostic

instance Lean.Lsp.instInhabitedPublishDiagnosticsParams : Inhabited PublishDiagnosticsParams

Equations

• Lean.Lsp.instInhabitedPublishDiagnosticsParams = { default := { uri := default, version? := default, diagnostics := default } }

instance Lean.Lsp.instBEqPublishDiagnosticsParams : BEq PublishDiagnosticsParams

Equations

• Lean.Lsp.instBEqPublishDiagnosticsParams = { beq := Lean.Lsp.beqPublishDiagnosticsParams✝ }

instance Lean.Lsp.instToJsonPublishDiagnosticsParams : ToJson PublishDiagnosticsParams

Equations

• Lean.Lsp.instToJsonPublishDiagnosticsParams = { toJson := Lean.Lsp.toJsonPublishDiagnosticsParams✝ }

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams : FromJson PublishDiagnosticsParams

Equations

• Lean.Lsp.instFromJsonPublishDiagnosticsParams = { fromJson? := Lean.Lsp.fromJsonPublishDiagnosticsParams✝ }