For general server architecture, see README.md. For details of IPC communication, see Watchdog.lean. This module implements per-file worker processes.

File processing and requests+notifications against a file should be concurrent for two reasons:

• By the LSP standard, requests should be cancellable.
• Since Lean allows arbitrary user code to be executed during elaboration via the tactic framework, elaboration can be extremely slow and even not halt in some cases. Users should be able to work with the file while this is happening, e.g. make new changes to the file or send requests.

To achieve these goals, elaboration is executed in a chain of tasks, where each task corresponds to the elaboration of one command. When the elaboration of one command is done, the next task is spawned. On didChange notifications, we search for the task in which the change occurred. If we stumble across a task that has not yet finished before finding the task we're looking for, we terminate it and start the elaboration there, otherwise we start the elaboration at the task where the change occurred.

Requests iterate over tasks until they find the command that they need to answer the request. In order to not block the main thread, this is done in a request task. If a task that the request task waits for is terminated, a change occurred somewhere before the command that the request is looking for and the request sends a "content changed" error.

structure Lean.Server.FileWorker.RefreshInfo : Type

• lastRefreshTimestamp : Nat
• successiveRefreshAttempts : Nat

structure Lean.Server.FileWorker.PartialHandlerInfo : Type

• refreshMethod : String
• requestsInFlight : Nat
• pendingRefreshInfo? : Option RefreshInfo

instance Lean.Server.FileWorker.instInhabitedPartialHandlerInfo : Inhabited PartialHandlerInfo

Equations

• Lean.Server.FileWorker.instInhabitedPartialHandlerInfo = { default := { refreshMethod := default, requestsInFlight := default, pendingRefreshInfo? := default } }

structure Lean.Server.FileWorker.WorkerContext : Type

• chanOut : Std.Channel JsonRpc.Message

  Synchronized output channel for LSP messages. Notifications for outdated versions are discarded on read.

• maxDocVersionRef : IO.Ref Int

  Latest document version received by the client, used for filtering out notifications from previous versions.

• freshRequestIdRef : IO.Ref Int
• stickyDiagnosticsRef : IO.Ref (Array Widget.InteractiveDiagnostic)

  Diagnostics that are included in every single textDocument/publishDiagnostics notification.

• partialHandlersRef : IO.Ref (RBMap String PartialHandlerInfo compare)
• pendingServerRequestsRef : IO.Ref (Std.TreeMap JsonRpc.RequestID (IO.Promise (ServerRequestResponse Json)) compare)
• hLog : IO.FS.Stream
• initParams : Lsp.InitializeParams
• processor : Parser.InputContext → BaseIO Language.Lean.InitialSnapshot
• clientHasWidgets : Bool
• cmdlineOpts : Options

  Options defined on the worker cmdline (i.e. not including options from setup-file), used for context-free tasks such as editing delay.

def Lean.Server.FileWorker.WorkerContext.modifyGetPartialHandler {α : Type} (ctx : WorkerContext) (method : String) (f : PartialHandlerInfo → α × PartialHandlerInfo) : BaseIO α

Equations

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

def Lean.Server.FileWorker.WorkerContext.modifyPartialHandler (ctx : WorkerContext) (method : String) (f : PartialHandlerInfo → PartialHandlerInfo) : BaseIO Unit

Equations

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

def Lean.Server.FileWorker.WorkerContext.updateRequestsInFlight (ctx : WorkerContext) (method : String) (f : Nat → Nat) : BaseIO Unit

Equations

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

def Lean.Server.FileWorker.WorkerContext.initPendingServerRequest (responseType : Type) [FromJson responseType] [Inhabited responseType] (ctx : WorkerContext) (id : JsonRpc.RequestID) : BaseIO (ServerTask (ServerRequestResponse responseType))

Equations

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

def Lean.Server.FileWorker.WorkerContext.resolveServerRequestResponse (ctx : WorkerContext) (id : JsonRpc.RequestID) (response : ServerRequestResponse Json) : BaseIO Unit

Equations

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

Asynchronous snapshot elaboration

instance Lean.Server.FileWorker.instInhabitedReportSnapshotsState : Inhabited Lean.Server.FileWorker.ReportSnapshotsState✝

Equations

• Lean.Server.FileWorker.instInhabitedReportSnapshotsState = { default := { hasBlocked := default, allInfoTrees := default, newInfoTrees := default, hasFatal := default } }

opaque Lean.Server.FileWorker.server.reportDelayMs : Lean.Option Nat

structure Lean.Server.FileWorker.MemorizedInteractiveDiagnostics : Type

Type of state stored in Snapshot.Diagnostics.cacheRef?.

See also section "Communication" in Lean/Server/README.md.

• diags : Array Widget.InteractiveDiagnostic

instance Lean.Server.FileWorker.instTypeNameMemorizedInteractiveDiagnostics : TypeName MemorizedInteractiveDiagnostics

Equations

• Lean.Server.FileWorker.instTypeNameMemorizedInteractiveDiagnostics = Lean.Server.FileWorker.inst✝

structure Lean.Server.FileWorker.PendingRequest : Type

• requestTask : ServerTask (Except IO.Error Unit)
• cancelTk : RequestCancellationToken

@[reducible, inline]

abbrev Lean.Server.FileWorker.PendingRequestMap : Type

Equations

• Lean.Server.FileWorker.PendingRequestMap = Lean.RBMap Lean.JsonRpc.RequestID Lean.Server.FileWorker.PendingRequest compare

structure Lean.Server.FileWorker.AvailableImportsCache : Type

• availableImports : ImportCompletion.AvailableImports
• lastRequestTimestampMs : Nat

structure Lean.Server.FileWorker.WorkerState : Type

• doc : EditableDocument
• reporterCancelTk : IO.CancelToken

  Token flagged for aborting doc.reporter when a new document version comes in.

• importCachingTask? : Option (ServerTask (Except IO.Error AvailableImportsCache))
• pendingRequests : PendingRequestMap
• rpcSessions : RBMap UInt64 (IO.Ref RpcSession) compare

  A map of RPC session IDs. We allow asynchronous elab tasks and request handlers to modify sessions. A single Ref ensures atomic transactions.

@[reducible, inline]

abbrev Lean.Server.FileWorker.WorkerM (α : Type) : Type

Equations

• Lean.Server.FileWorker.WorkerM = ReaderT Lean.Server.FileWorker.WorkerContext (StateRefT' IO.RealWorld Lean.Server.FileWorker.WorkerState IO)

def Lean.Server.FileWorker.setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Channel JsonRpc.Message) (stx : TSyntax `Lean.Parser.Module.header) : Language.ProcessingT IO (Except Language.Lean.HeaderProcessedSnapshot Language.Lean.SetupImportsResult)

Callback from Lean language processor after parsing imports that requests necessary information from Lake for processing imports.

Equations

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

def Lean.Server.FileWorker.initializeWorker (meta : DocumentMeta) (o e : IO.FS.Stream) (initParams : Lsp.InitializeParams) (opts : Options) : IO (WorkerContext × WorkerState)

Equations

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

def Lean.Server.FileWorker.initializeWorker.mkLspOutputChannel (o : IO.FS.Stream) (maxDocVersion : IO.Ref Int) : IO (Std.Channel JsonRpc.Message)

Creates an LSP message output channel along with a reader that sends out read messages on the output FS stream after discarding outdated notifications. This is the only component of the worker with access to the output stream, so we can synchronize messages from parallel elaboration tasks here.

Equations

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

def Lean.Server.FileWorker.initializeWorker.getImportClosure? (snap : Language.Lean.InitialSnapshot) : Array Name

Equations

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

def Lean.Server.FileWorker.sendServerRequest (paramType : Type u_1) [ToJson paramType] (responseType : Type) [FromJson responseType] [Inhabited responseType] (ctx : WorkerContext) (method : String) (param : paramType) : BaseIO (ServerTask (ServerRequestResponse responseType))

Equations

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

def Lean.Server.FileWorker.sendUntypedServerRequest (ctx : WorkerContext) (method : String) (param : Json) : BaseIO (ServerTask (ServerRequestResponse Json))

Equations

• Lean.Server.FileWorker.sendUntypedServerRequest ctx method param = Lean.Server.FileWorker.sendServerRequest Lean.Json Lean.Json ctx method param

def Lean.Server.FileWorker.updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : WorkerM Unit

Equations

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

def Lean.Server.FileWorker.updateDocument (meta : DocumentMeta) : WorkerM Unit

Given the new document, updates editable doc state.

Equations

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

def Lean.Server.FileWorker.handleDidChange (p : Lsp.DidChangeTextDocumentParams) : WorkerM Unit

Equations

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

def Lean.Server.FileWorker.handleCancelRequest (p : Lsp.CancelParams) : WorkerM Unit

Equations

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

def Lean.Server.FileWorker.handleStaleDependency : Lsp.LeanStaleDependencyParams → WorkerM Unit

Received from the watchdog when a dependency of this file is detected as being stale. Issues a sticky diagnostic to the client that it should run "Restart File".

Equations

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

def Lean.Server.FileWorker.handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit

Equations

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

def Lean.Server.FileWorker.handleRpcKeepAlive (p : Lsp.RpcKeepAliveParams) : WorkerM Unit

Equations

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

Requests here are handled synchronously rather than in the asynchronous RequestM.

def Lean.Server.FileWorker.handleRpcConnect : Lsp.RpcConnectParams → WorkerM Lsp.RpcConnected

Equations

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

def Lean.Server.FileWorker.parseParams (paramType : Type) [FromJson paramType] (params : Json) : WorkerM paramType

Equations

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

def Lean.Server.FileWorker.handleNotification (method : String) (params : Json) : WorkerM Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.FileWorker.handleNotification method params = liftM (IO.throwServerError (toString "Got unsupported notification method: " ++ toString method ++ toString ""))

def Lean.Server.FileWorker.queueRequest (id : JsonRpc.RequestID) (r : PendingRequest) : WorkerM Unit

Equations

• Lean.Server.FileWorker.queueRequest id r = Lean.Server.FileWorker.updatePendingRequests fun (x : Lean.Server.FileWorker.PendingRequestMap) => Lean.RBMap.insert x id r

def Lean.Server.FileWorker.handleImportCompletionRequest (id : JsonRpc.RequestID) (params : Lsp.CompletionParams) : WorkerM (ServerTask (Except IO.Error AvailableImportsCache))

Equations

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

def Lean.Server.FileWorker.handleStatefulPreRequestSpecialCases (id : JsonRpc.RequestID) (method : String) (params : Json) : WorkerM Bool

Equations

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

def Lean.Server.FileWorker.handleGetInteractiveDiagnosticsRequest (ctx : WorkerContext) (params : Widget.GetInteractiveDiagnosticsParams) : RequestM (Array Widget.InteractiveDiagnostic)

Equations

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

def Lean.Server.FileWorker.handlePreRequestSpecialCases? (ctx : WorkerContext) (st : WorkerState) (id : JsonRpc.RequestID) (method : String) (params : Json) : RequestM (Option (RequestTask (LspResponse Json)))

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.FileWorker.handlePreRequestSpecialCases? ctx st id method params = pure none

def Lean.Server.FileWorker.handlePostRequestSpecialCases (id : JsonRpc.RequestID) (method : String) (params : Json) (task : RequestTask (LspResponse Json)) : RequestM (RequestTask (LspResponse Json))

Equations

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

def Lean.Server.FileWorker.emitRequestResponse (requestTask? : Except RequestError (RequestTask (LspResponse Json))) (cancelTk : RequestCancellationToken) (id : JsonRpc.RequestID) (method : String) : WorkerM (ServerTask (Except IO.Error Unit))

Equations

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

def Lean.Server.FileWorker.emitRequestResponse.emitResponse (method : String) (ctx : WorkerContext) (m : JsonRpc.Message) (isComplete : Bool) : IO Unit

Equations

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

def Lean.Server.FileWorker.handleRequest (id : JsonRpc.RequestID) (method : String) (params : Json) : WorkerM Unit

Equations

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

def Lean.Server.FileWorker.handleResponse (id : JsonRpc.RequestID) (response : Json) : WorkerM Unit

Equations

• Lean.Server.FileWorker.handleResponse id response = do let ctx ← read liftM (ctx.resolveServerRequestResponse id (Lean.Server.ServerRequestResponse.success response))

def Lean.Server.FileWorker.handleResponseError (id : JsonRpc.RequestID) (code : JsonRpc.ErrorCode) (message : String) : WorkerM Unit

Equations

• Lean.Server.FileWorker.handleResponseError id code message = do let ctx ← read liftM (ctx.resolveServerRequestResponse id (Lean.Server.ServerRequestResponse.failure code message))

partial def Lean.Server.FileWorker.mainLoop (hIn : IO.FS.Stream) : WorkerM Unit

def Lean.Server.FileWorker.runRefreshTasks : WorkerM (Array (ServerTask Unit))

Equations

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

def Lean.Server.FileWorker.runRefreshTasks.sleepWithCancellation (ms : UInt32) : BaseIO Bool

Equations

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

def Lean.Server.FileWorker.initAndRunWorker (i o e : IO.FS.Stream) (opts : Options) : IO Unit

Equations

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

def Lean.Server.FileWorker.initAndRunWorker.writeErrorDiag (o : IO.FS.Stream) (meta : DocumentMeta) (err : IO.Error) : IO Unit

Equations

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

@[export lean_server_worker_main]

def Lean.Server.FileWorker.workerMain (opts : Options) : IO UInt32

Equations

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