Documentation

Lean.Data.Lsp.Ipc

Provides an IpcM monad for interacting with an external LSP process. Used for testing the Lean server.

@[reducible, inline]
abbrev Lean.Lsp.Ipc.IpcM (α : Type) :
Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      def Lean.Lsp.Ipc.shutdown (requestNo : Nat) :
                      Equations
                        Instances For
                          def Lean.Lsp.Ipc.readRequestAs (expectedMethod : String) (α : Type) [FromJson α] :
                          Equations
                            Instances For

                              Reads response, discarding notifications and server-to-client requests in between. This function is meant purely for testing where we use collectDiagnostics explicitly if we do care about such notifications.

                              Equations
                                Instances For

                                  Waits for the worker to emit all diagnostic notifications for the current document version and returns the last notification, if any.

                                  We used to return all notifications but with debouncing in the server, this would not be deterministic anymore as what messages are dropped depends on wall-clock timing.

                                  Equations
                                    Instances For
                                      def Lean.Lsp.Ipc.waitForILeans (waitForILeansId : JsonRpc.RequestID := 0) (target : DocumentUri) (version : Nat) :
                                      Equations
                                        Instances For

                                          Waits for a diagnostic notification with a specific message to be emitted. Discards all received messages, so should not be combined with collectDiagnostics.

                                          Equations
                                            Instances For
                                              def Lean.Lsp.Ipc.runWith {α : Type} (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) :
                                              IO α
                                              Equations
                                                Instances For