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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticSeverity : BEq DiagnosticSeverity

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticSeverity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

• Lean.Lsp.instOrdDiagnosticSeverity.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticSeverity : Ord DiagnosticSeverity

Equations

• Lean.Lsp.instOrdDiagnosticSeverity = { compare := Lean.Lsp.instOrdDiagnosticSeverity.ord }

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticSeverity : FromJson DiagnosticSeverity

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticCode : Inhabited DiagnosticCode

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticCode : BEq DiagnosticCode

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticCode.beq (Lean.Lsp.DiagnosticCode.int a) (Lean.Lsp.DiagnosticCode.int b) = (a == b)
• Lean.Lsp.instBEqDiagnosticCode.beq (Lean.Lsp.DiagnosticCode.string a) (Lean.Lsp.DiagnosticCode.string b) = (a == b)
• Lean.Lsp.instBEqDiagnosticCode.beq x✝¹ x✝ = false

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

Equations

• Lean.Lsp.instOrdDiagnosticCode.ord (Lean.Lsp.DiagnosticCode.int a) (Lean.Lsp.DiagnosticCode.int b) = (compare a b).then Ordering.eq
• Lean.Lsp.instOrdDiagnosticCode.ord (Lean.Lsp.DiagnosticCode.int a) x✝ = Ordering.lt
• Lean.Lsp.instOrdDiagnosticCode.ord x✝ (Lean.Lsp.DiagnosticCode.int a) = Ordering.gt
• Lean.Lsp.instOrdDiagnosticCode.ord (Lean.Lsp.DiagnosticCode.string a) (Lean.Lsp.DiagnosticCode.string b) = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticCode : Ord DiagnosticCode

Equations

• Lean.Lsp.instOrdDiagnosticCode = { compare := Lean.Lsp.instOrdDiagnosticCode.ord }

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticCode : FromJson DiagnosticCode

Equations

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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticTag : Inhabited DiagnosticTag

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticTag : BEq DiagnosticTag

Equations

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

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

Equations

• Lean.Lsp.instOrdDiagnosticTag.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticTag : Ord DiagnosticTag

Equations

• Lean.Lsp.instOrdDiagnosticTag = { compare := Lean.Lsp.instOrdDiagnosticTag.ord }

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticTag : FromJson DiagnosticTag

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedLeanDiagnosticTag : Inhabited LeanDiagnosticTag

Equations

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

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

Equations

• Lean.Lsp.instBEqLeanDiagnosticTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Lsp.instBEqLeanDiagnosticTag : BEq LeanDiagnosticTag

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instOrdLeanDiagnosticTag : Ord LeanDiagnosticTag

Equations

• Lean.Lsp.instOrdLeanDiagnosticTag = { compare := Lean.Lsp.instOrdLeanDiagnosticTag.ord }

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

Equations

• Lean.Lsp.instOrdLeanDiagnosticTag.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance Lean.Lsp.instFromJsonLeanDiagnosticTag : FromJson LeanDiagnosticTag

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation : Inhabited DiagnosticRelatedInformation

Equations

• Lean.Lsp.instInhabitedDiagnosticRelatedInformation = { default := Lean.Lsp.instInhabitedDiagnosticRelatedInformation.default }

@[implicit_reducible]

instance Lean.Lsp.instBEqDiagnosticRelatedInformation : BEq DiagnosticRelatedInformation

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticRelatedInformation.beq { location := a, message := a_1 } { location := b, message := b_1 } = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqDiagnosticRelatedInformation.beq x✝¹ x✝ = false

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

Equations

• Lean.Lsp.instToJsonDiagnosticRelatedInformation.toJson x✝ = Lean.Json.mkObj [[("location", Lean.toJson x✝.location)], [("message", Lean.toJson x✝.message)]].flatten

@[implicit_reducible]

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation : ToJson DiagnosticRelatedInformation

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation : FromJson DiagnosticRelatedInformation

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instOrdDiagnosticRelatedInformation : Ord DiagnosticRelatedInformation

Equations

• Lean.Lsp.instOrdDiagnosticRelatedInformation = { compare := Lean.Lsp.instOrdDiagnosticRelatedInformation.ord }

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

Equations

• Lean.Lsp.instOrdDiagnosticRelatedInformation.ord { location := a, message := a_1 } { location := b, message := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

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

Equations

• Lean.Lsp.instInhabitedDiagnosticWith = { default := Lean.Lsp.instInhabitedDiagnosticWith.default }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqDiagnosticWith.beq x✝¹ x✝ = false

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

@[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
• 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

Equations

• Lean.Lsp.instInhabitedPublishDiagnosticsParams = { default := Lean.Lsp.instInhabitedPublishDiagnosticsParams.default }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Lsp.instBEqPublishDiagnosticsParams.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Lsp.instBEqPublishDiagnosticsParams : BEq PublishDiagnosticsParams

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonPublishDiagnosticsParams : ToJson PublishDiagnosticsParams

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams : FromJson PublishDiagnosticsParams

Equations

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