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

def Lean.Lsp.Ipc.ipcStdioConfig : IO.Process.StdioConfig

Equations

• Lean.Lsp.Ipc.ipcStdioConfig = { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.inherit }

@[reducible, inline]

abbrev Lean.Lsp.Ipc.IpcM (α : Type) : Type

Equations

• Lean.Lsp.Ipc.IpcM = ReaderT (IO.Process.Child Lean.Lsp.Ipc.ipcStdioConfig) IO

def Lean.Lsp.Ipc.stdin : Lean.Lsp.Ipc.IpcM IO.FS.Stream

Equations

• Lean.Lsp.Ipc.stdin = do let __do_lift ← read pure (IO.FS.Stream.ofHandle __do_lift.stdin)

def Lean.Lsp.Ipc.stdout : Lean.Lsp.Ipc.IpcM IO.FS.Stream

Equations

• Lean.Lsp.Ipc.stdout = do let __do_lift ← read pure (IO.FS.Stream.ofHandle __do_lift.stdout)

def Lean.Lsp.Ipc.writeRequest {α : Type u_1} [Lean.ToJson α] (r : Lean.JsonRpc.Request α) : Lean.Lsp.Ipc.IpcM Unit

Equations

• Lean.Lsp.Ipc.writeRequest r = do let __do_lift ← Lean.Lsp.Ipc.stdin liftM (__do_lift.writeLspRequest r)

def Lean.Lsp.Ipc.writeNotification {α : Type u_1} [Lean.ToJson α] (n : Lean.JsonRpc.Notification α) : Lean.Lsp.Ipc.IpcM Unit

Equations

• Lean.Lsp.Ipc.writeNotification n = do let __do_lift ← Lean.Lsp.Ipc.stdin liftM (__do_lift.writeLspNotification n)

def Lean.Lsp.Ipc.shutdown (requestNo : Nat) : Lean.Lsp.Ipc.IpcM Unit

Equations

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

def Lean.Lsp.Ipc.readMessage : Lean.Lsp.Ipc.IpcM Lean.JsonRpc.Message

Equations

• Lean.Lsp.Ipc.readMessage = do let __do_lift ← Lean.Lsp.Ipc.stdout liftM __do_lift.readLspMessage

def Lean.Lsp.Ipc.readRequestAs (expectedMethod : String) (α : Type) [Lean.FromJson α] : Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Request α)

Equations

• Lean.Lsp.Ipc.readRequestAs expectedMethod α = do let __do_lift ← Lean.Lsp.Ipc.stdout liftM (__do_lift.readLspRequestAs expectedMethod α)

partial def Lean.Lsp.Ipc.readResponseAs (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] : Lean.Lsp.Ipc.IpcM (Lean.JsonRpc.Response α)

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.

def Lean.Lsp.Ipc.waitForExit : Lean.Lsp.Ipc.IpcM UInt32

Equations

• Lean.Lsp.Ipc.waitForExit = do let __do_lift ← read liftM __do_lift.wait

def Lean.Lsp.Ipc.collectDiagnostics (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) (target : Lean.Lsp.DocumentUri) (version : Nat) : Lean.Lsp.Ipc.IpcM (Option (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))

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

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

partial def Lean.Lsp.Ipc.collectDiagnostics.loop (waitForDiagnosticsId : optParam Lean.JsonRpc.RequestID 0) : Lean.Lsp.Ipc.IpcM (Option (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))

def Lean.Lsp.Ipc.runWith {α : Type} (lean : Lake.FilePath) (args : optParam (Array String) #[]) (test : Lean.Lsp.Ipc.IpcM α) : IO α

Equations

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