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

@[reducible, inline]

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

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

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

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

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

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

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

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

partial def Lean.Lsp.Ipc.readResponseAs (expectedID : JsonRpc.RequestID) (α : Type) [FromJson α] : IpcM (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 : IpcM UInt32

def Lean.Lsp.Ipc.normalizePublishDiagnosticsParams (p : PublishDiagnosticsParams) : PublishDiagnosticsParams

def Lean.Lsp.Ipc.mergePublishDiagnosticsParams (prev? : Option PublishDiagnosticsParams) (next : PublishDiagnosticsParams) : PublishDiagnosticsParams

Merges a new textDocument/publishDiagnostics notification into a previously accumulated one.

• If there is no previous notification, the new one is used as-is.
• If isIncremental? is true, the new diagnostics are appended.
• Otherwise the new notification replaces the previous one.

The returned params always have isIncremental? := some false since they represent the full accumulated set.

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

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

Incoming notifications are merged using mergePublishDiagnosticsParams.

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.

def Lean.Lsp.Ipc.waitForILeans (waitForILeansId : JsonRpc.RequestID := 0) (target : DocumentUri) (version : Nat) : IpcM Unit

def Lean.Lsp.Ipc.waitForWatchdogILeans (waitForILeansId : JsonRpc.RequestID := 0) : IpcM Unit

structure Lean.Lsp.Ipc.CallHierarchy : Type

• item : CallHierarchyItem
• fromRanges : Array Range
• children : Array CallHierarchy

@[implicit_reducible]

instance Lean.Lsp.Ipc.instFromJsonCallHierarchy : FromJson CallHierarchy

partial def Lean.Lsp.Ipc.instFromJsonCallHierarchy.fromJson : Json → Except String CallHierarchy

partial def Lean.Lsp.Ipc.instToJsonCallHierarchy.toJson : CallHierarchy → Json

@[implicit_reducible]

instance Lean.Lsp.Ipc.instToJsonCallHierarchy : ToJson CallHierarchy

def Lean.Lsp.Ipc.expandIncomingCallHierarchy (requestNo : Nat) (uri : DocumentUri) (pos : Position) : IpcM (Array CallHierarchy × Nat)

def Lean.Lsp.Ipc.expandOutgoingCallHierarchy (requestNo : Nat) (uri : DocumentUri) (pos : Position) : IpcM (Array CallHierarchy × Nat)

structure Lean.Lsp.Ipc.ModuleHierarchy : Type

• item : LeanImport
• children : Array ModuleHierarchy

@[implicit_reducible]

instance Lean.Lsp.Ipc.instFromJsonModuleHierarchy : FromJson ModuleHierarchy

partial def Lean.Lsp.Ipc.instFromJsonModuleHierarchy.fromJson : Json → Except String ModuleHierarchy

partial def Lean.Lsp.Ipc.instToJsonModuleHierarchy.toJson : ModuleHierarchy → Json

@[implicit_reducible]

instance Lean.Lsp.Ipc.instToJsonModuleHierarchy : ToJson ModuleHierarchy

def Lean.Lsp.Ipc.expandModuleHierarchyImports (requestNo : Nat) (uri : DocumentUri) : IpcM (Option ModuleHierarchy × Nat)

def Lean.Lsp.Ipc.expandModuleHierarchyImportedBy (requestNo : Nat) (uri : DocumentUri) : IpcM (Option ModuleHierarchy × Nat)

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