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

structure Lean.Lsp.WaitForDiagnosticsParams : Type

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

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.

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

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

structure Lean.Lsp.WaitForDiagnostics : Type

textDocument/waitForDiagnostics client<-server reply.

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

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

inductive Lean.Lsp.LeanFileProgressKind : Type

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

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

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

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

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

structure Lean.Lsp.LeanFileProgressProcessingInfo : Type

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

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

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

structure Lean.Lsp.LeanFileProgressParams : Type

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

$/lean/fileProgress client<-server notification.

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

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

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

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

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

structure Lean.Lsp.PlainGoal : Type

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

$/lean/plainGoal client<-server reply.

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

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

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

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

structure Lean.Lsp.PlainTermGoal : Type

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

$/lean/plainTermGoal client<-server reply.

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

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

structure Lean.Lsp.RpcConnectParams : Type

• uri : Lean.Lsp.DocumentUri

$/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.

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

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

structure Lean.Lsp.RpcConnected : Type

• sessionId : UInt64

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

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

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

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

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

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

  Procedure to invoke. Must be fully qualified.

• params : Lean.Json

$/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.

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

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

structure Lean.Lsp.RpcReleaseParams : Type

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

$/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.

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

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

structure Lean.Lsp.RpcKeepAliveParams : Type

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

$/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.

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

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

structure Lean.Lsp.LineRange : Type

• start : Nat
• end : Nat

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

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

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

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

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