Documentation

Lean.Data.Lsp.Extra

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

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.

Instances For

      textDocument/waitForDiagnostics client<-server reply.

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

        $/lean/fileProgress client<-server notification.

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

        Instances For

            $/lean/plainGoal client->server request.

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

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

              Instances For

                  $/lean/plainTermGoal client->server request.

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

                  Instances For

                    $/lean/plainTermGoal client<-server reply.

                    Instances For

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

                      Instances For

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

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

                        Instances For

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

                          Instances For

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

                            Instances For

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

                              Instances For

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

                                Instances For
                                  Equations