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 }

@[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 : 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 : 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} [ToJson α] (r : JsonRpc.Request α) : 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} [ToJson α] (n : JsonRpc.Notification α) : 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) : IpcM Unit

Equations

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

def Lean.Lsp.Ipc.readMessage : IpcM 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) [FromJson α] : IpcM (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 : 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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Lsp.Ipc.CallHierarchy : Type

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

@[implicit_reducible]

instance Lean.Lsp.Ipc.instFromJsonCallHierarchy : FromJson CallHierarchy

Equations

• Lean.Lsp.Ipc.instFromJsonCallHierarchy = { fromJson? := Lean.Lsp.Ipc.instFromJsonCallHierarchy.fromJson }

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

Equations

• Lean.Lsp.Ipc.instToJsonCallHierarchy = { toJson := Lean.Lsp.Ipc.instToJsonCallHierarchy.toJson }

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

Equations

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

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

Equations

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

structure Lean.Lsp.Ipc.ModuleHierarchy : Type

• item : LeanImport
• children : Array ModuleHierarchy

@[implicit_reducible]

instance Lean.Lsp.Ipc.instFromJsonModuleHierarchy : FromJson ModuleHierarchy

Equations

• Lean.Lsp.Ipc.instFromJsonModuleHierarchy = { fromJson? := Lean.Lsp.Ipc.instFromJsonModuleHierarchy.fromJson }

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

Equations

• Lean.Lsp.Ipc.instToJsonModuleHierarchy = { toJson := Lean.Lsp.Ipc.instToJsonModuleHierarchy.toJson }

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

Equations

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

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

Equations

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

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

Equations

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