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 }

@[inline, reducible]

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 (IO.FS.Stream.writeLspRequest __do_lift 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 (IO.FS.Stream.writeLspNotification __do_lift 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 (IO.FS.Stream.readLspMessage __do_lift)

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 (IO.FS.Stream.readLspRequestAs __do_lift 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 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 (IO.Process.Child.wait __do_lift)

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

Waits for the worker to emit all diagnostics for the current document version and returns them as a list.

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 (List (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.