Lean.Data.Lsp.Extra

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

source

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.

source

instance Lean.Lsp.instFromJsonWaitForDiagnosticsParams:

Lean.FromJson Lean.Lsp.WaitForDiagnosticsParams

Equations

Lean.Lsp.instFromJsonWaitForDiagnosticsParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonWaitForDiagnosticsParams:

Lean.ToJson Lean.Lsp.WaitForDiagnosticsParams

Equations

Lean.Lsp.instToJsonWaitForDiagnosticsParams = { toJson := [anonymous] }

source

structure Lean.Lsp.WaitForDiagnostics:

Type

textDocument/waitForDiagnostics client<-server reply.

source

instance Lean.Lsp.instFromJsonWaitForDiagnostics:

Lean.FromJson Lean.Lsp.WaitForDiagnostics

Equations

Lean.Lsp.instFromJsonWaitForDiagnostics = { fromJson? := fun x => pure { } }

source

instance Lean.Lsp.instToJsonWaitForDiagnostics:

Lean.ToJson Lean.Lsp.WaitForDiagnostics

Equations

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

source

inductive Lean.Lsp.LeanFileProgressKind:

Type

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

source

instance Lean.Lsp.instInhabitedLeanFileProgressKind:

Inhabited Lean.Lsp.LeanFileProgressKind

Equations

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

source

instance Lean.Lsp.instBEqLeanFileProgressKind:

BEq Lean.Lsp.LeanFileProgressKind

Equations

Lean.Lsp.instBEqLeanFileProgressKind = { beq := [anonymous] }

source

instance Lean.Lsp.instFromJsonLeanFileProgressKind:

Lean.FromJson Lean.Lsp.LeanFileProgressKind

Equations

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

source

instance Lean.Lsp.instToJsonLeanFileProgressKind:

Lean.ToJson Lean.Lsp.LeanFileProgressKind

Equations

Lean.Lsp.instToJsonLeanFileProgressKind = { toJson := fun x => match x with | Lean.Lsp.LeanFileProgressKind.processing => 1 | Lean.Lsp.LeanFileProgressKind.fatalError => 2 }

source

structure Lean.Lsp.LeanFileProgressProcessingInfo:

Type

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

source

instance Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo:

Lean.FromJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

Lean.Lsp.instFromJsonLeanFileProgressProcessingInfo = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonLeanFileProgressProcessingInfo:

Lean.ToJson Lean.Lsp.LeanFileProgressProcessingInfo

Equations

Lean.Lsp.instToJsonLeanFileProgressProcessingInfo = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonLeanFileProgressParams:

Lean.FromJson Lean.Lsp.LeanFileProgressParams

Equations

Lean.Lsp.instFromJsonLeanFileProgressParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonLeanFileProgressParams:

Lean.ToJson Lean.Lsp.LeanFileProgressParams

Equations

Lean.Lsp.instToJsonLeanFileProgressParams = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonPlainGoalParams:

Lean.FromJson Lean.Lsp.PlainGoalParams

Equations

Lean.Lsp.instFromJsonPlainGoalParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonPlainGoalParams:

Lean.ToJson Lean.Lsp.PlainGoalParams

Equations

Lean.Lsp.instToJsonPlainGoalParams = { toJson := [anonymous] }

source

structure Lean.Lsp.PlainGoal:

Type

The goals as pretty-printed Markdown, or something like "no goals" if accomplished.
rendered : String
The pretty-printed goals, empty if all accomplished.
goals : Array String

$/lean/plainGoal client<-server reply.

source

instance Lean.Lsp.instFromJsonPlainGoal:

Lean.FromJson Lean.Lsp.PlainGoal

Equations

Lean.Lsp.instFromJsonPlainGoal = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonPlainGoal:

Lean.ToJson Lean.Lsp.PlainGoal

Equations

Lean.Lsp.instToJsonPlainGoal = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonPlainTermGoalParams:

Lean.FromJson Lean.Lsp.PlainTermGoalParams

Equations

Lean.Lsp.instFromJsonPlainTermGoalParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonPlainTermGoalParams:

Lean.ToJson Lean.Lsp.PlainTermGoalParams

Equations

Lean.Lsp.instToJsonPlainTermGoalParams = { toJson := [anonymous] }

source

structure Lean.Lsp.PlainTermGoal:

Type

goal : String
range : Lean.Lsp.Range

$/lean/plainTermGoal client<-server reply.

source

instance Lean.Lsp.instFromJsonPlainTermGoal:

Lean.FromJson Lean.Lsp.PlainTermGoal

Equations

Lean.Lsp.instFromJsonPlainTermGoal = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonPlainTermGoal:

Lean.ToJson Lean.Lsp.PlainTermGoal

Equations

Lean.Lsp.instToJsonPlainTermGoal = { toJson := [anonymous] }

source

structure Lean.Lsp.RpcRef:

Type

p : USize

An object which RPC clients can refer to without marshalling.

source

instance Lean.Lsp.instBEqRpcRef:

BEq Lean.Lsp.RpcRef

Equations

Lean.Lsp.instBEqRpcRef = { beq := [anonymous] }

source

instance Lean.Lsp.instHashableRpcRef:

Hashable Lean.Lsp.RpcRef

Equations

Lean.Lsp.instHashableRpcRef = { hash := [anonymous] }

source

instance Lean.Lsp.instFromJsonRpcRef:

Lean.FromJson Lean.Lsp.RpcRef

Equations

Lean.Lsp.instFromJsonRpcRef = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonRpcRef:

Lean.ToJson Lean.Lsp.RpcRef

Equations

Lean.Lsp.instToJsonRpcRef = { toJson := [anonymous] }

source

instance Lean.Lsp.instToStringRpcRef:

ToString Lean.Lsp.RpcRef

Equations

Lean.Lsp.instToStringRpcRef = { toString := fun r => toString r.p }

source

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.

source

instance Lean.Lsp.instFromJsonRpcConnectParams:

Lean.FromJson Lean.Lsp.RpcConnectParams

Equations

Lean.Lsp.instFromJsonRpcConnectParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonRpcConnectParams:

Lean.ToJson Lean.Lsp.RpcConnectParams

Equations

Lean.Lsp.instToJsonRpcConnectParams = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonRpcConnected:

Lean.FromJson Lean.Lsp.RpcConnected

Equations

Lean.Lsp.instFromJsonRpcConnected = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonRpcConnected:

Lean.ToJson Lean.Lsp.RpcConnected

Equations

Lean.Lsp.instToJsonRpcConnected = { toJson := [anonymous] }

source

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

Type

sessionId : UInt64
Procedure to invoke. Must be fully qualified.
method : Lean.Name
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.

source

instance Lean.Lsp.instFromJsonRpcCallParams:

Lean.FromJson Lean.Lsp.RpcCallParams

Equations

Lean.Lsp.instFromJsonRpcCallParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonRpcCallParams:

Lean.ToJson Lean.Lsp.RpcCallParams

Equations

Lean.Lsp.instToJsonRpcCallParams = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonRpcReleaseParams:

Lean.FromJson Lean.Lsp.RpcReleaseParams

Equations

Lean.Lsp.instFromJsonRpcReleaseParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonRpcReleaseParams:

Lean.ToJson Lean.Lsp.RpcReleaseParams

Equations

Lean.Lsp.instToJsonRpcReleaseParams = { toJson := [anonymous] }

source

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.

source

instance Lean.Lsp.instFromJsonRpcKeepAliveParams:

Lean.FromJson Lean.Lsp.RpcKeepAliveParams

Equations