Documentation

Lean.Server.FileWorker

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 occured. 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 occured.

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 occured somewhere before the command that the request is looking for and the request sends a "content changed" error.

structure Lean.Server.FileWorker.WorkerContext:

Type

hIn : IO.FS.Stream
hOut : IO.FS.Stream
hLog : IO.FS.Stream
headerTask : Task (Except IO.Error (Lean.Server.Snapshots.Snapshot × Lean.SearchPath))
initParams : Lean.Lsp.InitializeParams
clientHasWidgets : Bool

structure Lean.Server.FileWorker.AsyncElabState:

Type

snaps : Array Lean.Server.Snapshots.Snapshot

@[inline]

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

Type

Equations

Lean.Server.FileWorker.AsyncElabM = StateT Lean.Server.FileWorker.AsyncElabState (EIO Lean.Server.FileWorker.ElabTaskError)

def Lean.Server.FileWorker.unfoldCmdSnaps (m : Lean.Server.DocumentMeta) (snaps : Array Lean.Server.Snapshots.Snapshot) (cancelTk : Lean.Server.FileWorker.CancelToken) :

ReaderT Lean.Server.FileWorker.WorkerContext IO (IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot)

Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into hOut.

Equations

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

@[inline]

abbrev Lean.Server.FileWorker.PendingRequestMap:

Type

Equations

Lean.Server.FileWorker.PendingRequestMap = Std.RBMap Lean.JsonRpc.RequestID (Task (Except IO.Error Unit)) compare

structure Lean.Server.FileWorker.WorkerState:

Type

doc : Lean.Server.FileWorker.EditableDocument
pendingRequests : Lean.Server.FileWorker.PendingRequestMap
A map of RPC session IDs. We allow asynchronous elab tasks and request handlers to modify sessions. A single Ref ensures atomic transactions.
rpcSessions : Std.RBMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare

@[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.lakeSetupSearchPath (lakePath : System.FilePath) (m : Lean.Server.DocumentMeta) (imports : Array Lean.Import) (hOut : IO.FS.Stream) :

IO Lean.SearchPath

Use lake print-paths to compile dependencies on the fly and add them to LEAN_PATH. Compilation progress is reported to hOut via LSP notifications. Return the search path for source files.

Equations

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

partial def Lean.Server.FileWorker.lakeSetupSearchPath.processStderr (lakePath : System.FilePath) (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) (args : Array String) (lakeProc : IO.Process.Child { toStdioConfig := { stdin := IO.Process.Stdio.null, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }, cmd := lakePath.toString, args := args, cwd := none, env := #[] }.toStdioConfig) (acc : String) :

def Lean.Server.FileWorker.compileHeader (m : Lean.Server.DocumentMeta) (hOut : IO.FS.Stream) (opts : Lean.Options) (hasWidgets : Bool) :

IO (Lean.Server.Snapshots.Snapshot × Lean.SearchPath)

Equations

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

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

IO (Lean.Server.FileWorker.WorkerContext × Lean.Server.FileWorker.WorkerState)

Equations

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

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

Lean.Server.FileWorker.WorkerM Unit

Equations

Lean.Server.FileWorker.updatePendingRequests map = modify fun st => { doc := st.doc, pendingRequests := map st.pendingRequests, rpcSessions := st.rpcSessions }

def Lean.Server.FileWorker.updateDocument (newMeta : Lean.Server.DocumentMeta) :

Lean.Server.FileWorker.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 : Lean.Lsp.DidChangeTextDocumentParams) :

Lean.Server.FileWorker.WorkerM Unit

Equations

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

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

Lean.Server.FileWorker.WorkerM Unit

Equations

Lean.Server.FileWorker.handleCancelRequest p = Lean.Server.FileWorker.updatePendingRequests fun pendingRequests => Std.RBMap.erase pendingRequests p.id

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

Lean.Server.FileWorker.WorkerM Unit

Equations

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

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

Lean.Server.FileWorker.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:

Lean.Lsp.RpcConnectParams → Lean.Server.FileWorker.WorkerM Lean.Lsp.RpcConnected

Equations

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

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

Lean.Server.FileWorker.WorkerM paramType

Equations

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

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

Lean.Server.FileWorker.WorkerM Unit

Equations

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

def Lean.Server.FileWorker.queueRequest (id : Lean.JsonRpc.RequestID) (requestTask : Task (Except IO.Error Unit)) :

Lean.Server.FileWorker.WorkerM Unit

Equations

Lean.Server.FileWorker.queueRequest id requestTask = Lean.Server.FileWorker.updatePendingRequests fun pendingRequests => Std.RBMap.insert pendingRequests id requestTask

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

Lean.Server.FileWorker.WorkerM Unit

Equations

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

partial def Lean.Server.FileWorker.mainLoop:

Lean.Server.FileWorker.WorkerM Unit

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

Equations

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

@[export lean_server_worker_main]

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

Equations

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