This file contains Lean-specific extensions to LSP. See the structures below for which additional requests and notifications are supported.

inductive Lean.Lsp.DependencyBuildMode : Type

Controls when dependencies are built on textDocument/didOpen notifications.

• always: Lean.Lsp.DependencyBuildMode

  Always build dependencies.

• once: Lean.Lsp.DependencyBuildMode

  Build dependencies once, but then do not build them again on import changes / crashes. Used for didOpen notifications that are explicitly intended for manually triggering the build.

• never: Lean.Lsp.DependencyBuildMode

  Never build dependencies.

instance Lean.Lsp.instFromJsonDependencyBuildMode : Lean.FromJson Lean.Lsp.DependencyBuildMode

Equations

• Lean.Lsp.instFromJsonDependencyBuildMode = { fromJson? := Lean.Lsp.fromJsonDependencyBuildMode✝ }

instance Lean.Lsp.instToJsonDependencyBuildMode : Lean.ToJson Lean.Lsp.DependencyBuildMode

Equations

• Lean.Lsp.instToJsonDependencyBuildMode = { toJson := Lean.Lsp.toJsonDependencyBuildMode✝ }

instance Lean.Lsp.instInhabitedDependencyBuildMode : Inhabited Lean.Lsp.DependencyBuildMode

Equations

• Lean.Lsp.instInhabitedDependencyBuildMode = { default := Lean.Lsp.DependencyBuildMode.always }

structure Lean.Lsp.LeanDidOpenTextDocumentParamsextends Lean.Lsp.DidOpenTextDocumentParams : Type

• textDocument : Lean.Lsp.TextDocumentItem
• dependencyBuildMode? : Option Lean.Lsp.DependencyBuildMode

instance Lean.Lsp.instFromJsonLeanDidOpenTextDocumentParams : Lean.FromJson Lean.Lsp.LeanDidOpenTextDocumentParams

Equations

• Lean.Lsp.instFromJsonLeanDidOpenTextDocumentParams = { fromJson? := Lean.Lsp.fromJsonLeanDidOpenTextDocumentParams✝ }

instance Lean.Lsp.instToJsonLeanDidOpenTextDocumentParams : Lean.ToJson Lean.Lsp.LeanDidOpenTextDocumentParams

Equations

• Lean.Lsp.instToJsonLeanDidOpenTextDocumentParams = { toJson := Lean.Lsp.toJsonLeanDidOpenTextDocumentParams✝ }

structure Lean.Lsp.WaitForDiagnosticsParams : Type

textDocument/waitForDiagnostics client->server request.

Yields a response when all the diagnostics for a version of the document greater or equal to the specified one have been emitted. If the request specifies a version above the most recently processed one, the server will delay the response until it does receive the specified version. Exists for synchronization purposes, e.g. during testing or when external tools might want to use our LSP server.

• uri : Lean.Lsp.DocumentUri
• version : Nat

instance Lean.Lsp.instFromJsonWaitForDiagnosticsParams : Lean.FromJson Lean.Lsp.WaitForDiagnosticsParams

Equations

• Lean.Lsp.instFromJsonWaitForDiagnosticsParams = { fromJson? := Lean.Lsp.fromJsonWaitForDiagnosticsParams✝ }

instance Lean.Lsp.instToJsonWaitForDiagnosticsParams : Lean.ToJson Lean.Lsp.WaitForDiagnosticsParams

Equations

• Lean.Lsp.instToJsonWaitForDiagnosticsParams = { toJson := Lean.Lsp.toJsonWaitForDiagnosticsParams✝ }

structure Lean.Lsp.WaitForDiagnostics : Type

textDocument/waitForDiagnostics client<-server reply.

instance Lean.Lsp.instFromJsonWaitForDiagnostics : Lean.FromJson Lean.Lsp.WaitForDiagnostics

Equations

• Lean.Lsp.instFromJsonWaitForDiagnostics = { fromJson? := fun (x : Lean.Json) => pure { } }

instance Lean.Lsp.instToJsonWaitForDiagnostics : Lean.ToJson Lean.Lsp.WaitForDiagnostics

Equations

• Lean.Lsp.instToJsonWaitForDiagnostics = { toJson := fun (x : Lean.Lsp.WaitForDiagnostics) => Lean.Json.mkObj [] }

inductive Lean.Lsp.LeanFileProgressKind : Type

• processing: Lean.Lsp.LeanFileProgressKind
• fatalError: Lean.Lsp.LeanFileProgressKind

instance Lean.Lsp.instInhabitedLeanFileProgressKind : Inhabited Lean.Lsp.LeanFileProgressKind

Equations

• Lean.Lsp.instInhabitedLeanFileProgressKind = { default := Lean.Lsp.LeanFileProgressKind.processing }

instance Lean.Lsp.instBEqLeanFileProgressKind : BEq Lean.Lsp.LeanFileProgressKind

Equations

• Lean.Lsp.instBEqLeanFileProgressKind = { beq := Lean.Lsp.beqLeanFileProgressKind✝ }

instance Lean.Lsp.instFromJsonLeanFileProgressKind : Lean.FromJson Lean.Lsp.LeanFileProgressKind

Equations

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

instance Lean.Lsp.instToJsonLeanFileProgressKind : Lean.ToJson Lean.Lsp.LeanFileProgressKind

Equations

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

structure Lean.Lsp.LeanFileProgressProcessingInfo : Type

• range : Lean.Lsp.Range
• kind : Lean.Lsp.LeanFileProgressKind

instance Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo : Lean.FromJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

• Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo = { fromJson? := Lean.Lsp.fromJsonLeanFileProgressProcessingInfo✝ }

instance Lean.Lsp.instToJsonLeanFileProgressProcessingInfo : Lean.ToJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

• Lean.Lsp.instToJsonLeanFileProgressProcessingInfo = { toJson := Lean.Lsp.toJsonLeanFileProgressProcessingInfo✝ }

structure Lean.Lsp.LeanFileProgressParams : Type

$/lean/fileProgress client<-server notification.

Contains the ranges of the document that are currently being processed by the server.

• textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
• processing : Array Lean.Lsp.LeanFileProgressProcessingInfo

instance Lean.Lsp.instFromJsonLeanFileProgressParams : Lean.FromJson Lean.Lsp.LeanFileProgressParams

Equations

• Lean.Lsp.instFromJsonLeanFileProgressParams = { fromJson? := Lean.Lsp.fromJsonLeanFileProgressParams✝ }

instance Lean.Lsp.instToJsonLeanFileProgressParams : Lean.ToJson Lean.Lsp.LeanFileProgressParams

Equations

• Lean.Lsp.instToJsonLeanFileProgressParams = { toJson := Lean.Lsp.toJsonLeanFileProgressParams✝ }

structure Lean.Lsp.PlainGoalParamsextends Lean.Lsp.TextDocumentPositionParams : Type

$/lean/plainGoal client->server request.

If there is a tactic proof at the specified position, returns the current goals. Otherwise returns null.

instance Lean.Lsp.instFromJsonPlainGoalParams : Lean.FromJson Lean.Lsp.PlainGoalParams

Equations

• Lean.Lsp.instFromJsonPlainGoalParams = { fromJson? := Lean.Lsp.fromJsonPlainGoalParams✝ }

instance Lean.Lsp.instToJsonPlainGoalParams : Lean.ToJson Lean.Lsp.PlainGoalParams

Equations

• Lean.Lsp.instToJsonPlainGoalParams = { toJson := Lean.Lsp.toJsonPlainGoalParams✝ }

structure Lean.Lsp.PlainGoal : Type

$/lean/plainGoal client<-server reply.

• rendered : String

  The goals as pretty-printed Markdown, or something like "no goals" if accomplished.

• goals : Array String

  The pretty-printed goals, empty if all accomplished.

instance Lean.Lsp.instFromJsonPlainGoal : Lean.FromJson Lean.Lsp.PlainGoal

Equations

• Lean.Lsp.instFromJsonPlainGoal = { fromJson? := Lean.Lsp.fromJsonPlainGoal✝ }

instance Lean.Lsp.instToJsonPlainGoal : Lean.ToJson Lean.Lsp.PlainGoal

Equations

• Lean.Lsp.instToJsonPlainGoal = { toJson := Lean.Lsp.toJsonPlainGoal✝ }

structure Lean.Lsp.PlainTermGoalParamsextends Lean.Lsp.TextDocumentPositionParams : Type

$/lean/plainTermGoal client->server request.

Returns the expected type at the specified position, pretty-printed as a string.

instance Lean.Lsp.instFromJsonPlainTermGoalParams : Lean.FromJson Lean.Lsp.PlainTermGoalParams

Equations

• Lean.Lsp.instFromJsonPlainTermGoalParams = { fromJson? := Lean.Lsp.fromJsonPlainTermGoalParams✝ }

instance Lean.Lsp.instToJsonPlainTermGoalParams : Lean.ToJson Lean.Lsp.PlainTermGoalParams

Equations

• Lean.Lsp.instToJsonPlainTermGoalParams = { toJson := Lean.Lsp.toJsonPlainTermGoalParams✝ }

structure Lean.Lsp.PlainTermGoal : Type

$/lean/plainTermGoal client<-server reply.

• goal : String
• range : Lean.Lsp.Range

instance Lean.Lsp.instFromJsonPlainTermGoal : Lean.FromJson Lean.Lsp.PlainTermGoal

Equations

• Lean.Lsp.instFromJsonPlainTermGoal = { fromJson? := Lean.Lsp.fromJsonPlainTermGoal✝ }

instance Lean.Lsp.instToJsonPlainTermGoal : Lean.ToJson Lean.Lsp.PlainTermGoal

Equations

• Lean.Lsp.instToJsonPlainTermGoal = { toJson := Lean.Lsp.toJsonPlainTermGoal✝ }

structure Lean.Lsp.RpcConnectParams : Type

$/lean/rpc/connect client->server request.

Starts an RPC session at the given file's worker, replying with the new session ID. Multiple sessions may be started and operating concurrently.

A session may be destroyed by the server at any time (e.g. due to a crash), in which case further RPC requests for that session will reply with RpcNeedsReconnect errors. The client should discard references held from that session and connect again.

• uri : Lean.Lsp.DocumentUri

instance Lean.Lsp.instFromJsonRpcConnectParams : Lean.FromJson Lean.Lsp.RpcConnectParams

Equations

• Lean.Lsp.instFromJsonRpcConnectParams = { fromJson? := Lean.Lsp.fromJsonRpcConnectParams✝ }

instance Lean.Lsp.instToJsonRpcConnectParams : Lean.ToJson Lean.Lsp.RpcConnectParams

Equations

• Lean.Lsp.instToJsonRpcConnectParams = { toJson := Lean.Lsp.toJsonRpcConnectParams✝ }

structure Lean.Lsp.RpcConnected : Type

$/lean/rpc/connect client<-server reply.

Indicates that an RPC connection had been made and a session started for it.

• sessionId : UInt64

instance Lean.Lsp.instFromJsonRpcConnected : Lean.FromJson Lean.Lsp.RpcConnected

Equations

• Lean.Lsp.instFromJsonRpcConnected = { fromJson? := Lean.Lsp.fromJsonRpcConnected✝ }

instance Lean.Lsp.instToJsonRpcConnected : Lean.ToJson Lean.Lsp.RpcConnected

Equations

• Lean.Lsp.instToJsonRpcConnected = { toJson := Lean.Lsp.toJsonRpcConnected✝ }

structure Lean.Lsp.RpcCallParamsextends Lean.Lsp.TextDocumentPositionParams : Type

$/lean/rpc/call client->server request.

A request to execute a procedure bound for RPC. If an incorrect session ID is present, the server errors with RpcNeedsReconnect.

Extending TDPP is weird. But in Lean, symbols exist in the context of a position within a source file. So we need this to refer to code in the environment at that position.

• textDocument : Lean.Lsp.TextDocumentIdentifier
• position : Lean.Lsp.Position
• sessionId : UInt64
• method : Lake.Name

  Procedure to invoke. Must be fully qualified.

• params : Lean.Json

instance Lean.Lsp.instFromJsonRpcCallParams : Lean.FromJson Lean.Lsp.RpcCallParams

Equations

• Lean.Lsp.instFromJsonRpcCallParams = { fromJson? := Lean.Lsp.fromJsonRpcCallParams✝ }

instance Lean.Lsp.instToJsonRpcCallParams : Lean.ToJson Lean.Lsp.RpcCallParams

Equations

• Lean.Lsp.instToJsonRpcCallParams = { toJson := Lean.Lsp.toJsonRpcCallParams✝ }

structure Lean.Lsp.RpcReleaseParams : Type

$/lean/rpc/release client->server notification.

A notification to release remote references. Should be sent by the client when it no longer needs RpcRefs it has previously received from the server. Not doing so is safe but will leak memory.

• uri : Lean.Lsp.DocumentUri
• sessionId : UInt64
• refs : Array Lean.Lsp.RpcRef

instance Lean.Lsp.instFromJsonRpcReleaseParams : Lean.FromJson Lean.Lsp.RpcReleaseParams

Equations

• Lean.Lsp.instFromJsonRpcReleaseParams = { fromJson? := Lean.Lsp.fromJsonRpcReleaseParams✝ }

instance Lean.Lsp.instToJsonRpcReleaseParams : Lean.ToJson Lean.Lsp.RpcReleaseParams

Equations

• Lean.Lsp.instToJsonRpcReleaseParams = { toJson := Lean.Lsp.toJsonRpcReleaseParams✝ }

structure Lean.Lsp.RpcKeepAliveParams : Type

$/lean/rpc/keepAlive client->server notification.

The client must send an RPC notification every 10s in order to keep the RPC session alive. This is the simplest one. On not seeing any notifications for three 10s periods, the server will drop the RPC session and its associated references.

• uri : Lean.Lsp.DocumentUri
• sessionId : UInt64

instance Lean.Lsp.instFromJsonRpcKeepAliveParams : Lean.FromJson Lean.Lsp.RpcKeepAliveParams

Equations

• Lean.Lsp.instFromJsonRpcKeepAliveParams = { fromJson? := Lean.Lsp.fromJsonRpcKeepAliveParams✝ }

instance Lean.Lsp.instToJsonRpcKeepAliveParams : Lean.ToJson Lean.Lsp.RpcKeepAliveParams

Equations

• Lean.Lsp.instToJsonRpcKeepAliveParams = { toJson := Lean.Lsp.toJsonRpcKeepAliveParams✝ }

structure Lean.Lsp.LineRange : Type

Range of lines in a document, including start but excluding end.

• start : Nat
• end : Nat

instance Lean.Lsp.instInhabitedLineRange : Inhabited Lean.Lsp.LineRange

Equations

• Lean.Lsp.instInhabitedLineRange = { default := { start := default, end := default } }

instance Lean.Lsp.instReprLineRange : Repr Lean.Lsp.LineRange

Equations

• Lean.Lsp.instReprLineRange = { reprPrec := Lean.Lsp.reprLineRange✝ }

instance Lean.Lsp.instFromJsonLineRange : Lean.FromJson Lean.Lsp.LineRange

Equations

• Lean.Lsp.instFromJsonLineRange = { fromJson? := Lean.Lsp.fromJsonLineRange✝ }

instance Lean.Lsp.instToJsonLineRange : Lean.ToJson Lean.Lsp.LineRange

Equations

• Lean.Lsp.instToJsonLineRange = { toJson := Lean.Lsp.toJsonLineRange✝ }