For general server architecture, see README.md
. This module implements the watchdog process.
Watchdog state #
Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes to the header and thus restart the corresponding worker, freeing its imports.
TODO(WN): We may eventually want to keep track of approximately (since this isn't knowable exactly) where in the file a worker crashed. Then on restart, we tell said worker to only parse up to that point and query the user about how to proceed (continue OR allow the user to fix the bug and then continue OR ..). Without this, if the crash is deterministic, users may be confused about why the server seemingly stopped working for a single file.
Watchdog <-> worker communication #
The watchdog process and its file worker processes communicate via LSP. If the necessity arises, we might add non-standard commands similarly based on JSON-RPC. Most requests and notifications are forwarded to the corresponding file worker process, with the exception of these notifications:
- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a task to asynchronously receive LSP packets from the worker (e.g. request responses).
- textDocument/didChange: Update the local file state. If the header was mutated,
signal a shutdown to the file worker by closing the I/O channels.
Then restart the file worker. Otherwise, forward the
didChange
notification. - textDocument/didClose: Signal a shutdown to the file worker and remove the associated watchdog state.
Moreover, we don't implement the full protocol at this level:
- Upon starting, the
initialize
request is forwarded to the worker, but it must not respond with its server capabilities. Consequently, the watchdog will not send aninitialized
notification to the worker. - After
initialize
, the watchdog sends the correspondingdidOpen
notification with the full current state of the file. No additionaldidOpen
notifications will be forwarded to the worker process. $/cancelRequest
notifications are forwarded to all file workers.- File workers are always terminated with an
exit
notification, without previously receiving ashutdown
request. Similarly, they never receive adidClose
notification.
Watchdog <-> client communication #
The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add non-standard extensions in case they're needed, for example to communicate tactic state.
- meta : Lean.Server.DocumentMeta
- headerAst : Lean.Syntax
Equations
- Lean.Server.Watchdog.workerCfg = { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.inherit }
- processGroupedEdits: Lean.Server.Watchdog.WorkerEvent
- terminated: Lean.Server.Watchdog.WorkerEvent
- crashed: IO.Error → Lean.Server.Watchdog.WorkerEvent
- ioError: IO.Error → Lean.Server.Watchdog.WorkerEvent
Events that worker-specific tasks signal to the main thread.
When to process the edits.
applyTime : Nat- params : Lean.Lsp.DidChangeTextDocumentParams
Signals when
applyTime
has been reached.signalTask : Task Lean.Server.Watchdog.WorkerEventWe should not reorder messages when delaying edits, so we queue other messages since the last request here.
queuedMsgs : Array Lean.JsonRpc.Message
A group of edits which will be processed at a future instant.
- commTask : Task Lean.Server.Watchdog.WorkerEvent
- state : Lean.Server.Watchdog.WorkerState
The pending requests map contains all requests that have been received from the LSP client, but were not answered yet. This includes the queued messages in the grouped edits.
pendingRequestsRef : IO.Ref Lean.Server.Watchdog.PendingRequestMap- groupedEditsRef : IO.Ref (Option Lean.Server.Watchdog.GroupedEdits)
Equations
- Lean.Server.Watchdog.FileWorker.stdin fw = IO.FS.Stream.ofHandle fw.proc.stdin
Equations
- Lean.Server.Watchdog.FileWorker.stdout fw = IO.FS.Stream.ofHandle fw.proc.stdout
Equations
- Lean.Server.Watchdog.FileWorker.erasePendingRequest fw id = ST.Ref.modify fw.pendingRequestsRef fun pendingRequests => Std.RBMap.erase pendingRequests id
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- hIn : IO.FS.Stream
- hOut : IO.FS.Stream
- hLog : IO.FS.Stream
Command line arguments.
- fileWorkersRef : IO.Ref Lean.Server.Watchdog.FileWorkerMap
We store these to pass them to workers.
initParams : Lean.Lsp.InitializeParams- editDelay : Nat
- workerPath : System.FilePath
- srcSearchPath : System.SearchPath
- references : IO.Ref Lean.Server.References
Equations
- Lean.Server.Watchdog.updateFileWorkers val = do let a ← read ST.Ref.modify a.fileWorkersRef fun fileWorkers => Std.RBMap.insert fileWorkers val.doc.meta.uri val
Equations
- Lean.Server.Watchdog.findFileWorker? uri = do let a ← read let a ← ST.Ref.get a.fileWorkersRef pure (Std.RBMap.find? a uri)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Server.Watchdog.log msg = do let st ← read liftM (IO.FS.Stream.putStrLn st.hLog msg) liftM st.hLog.flush
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Tries to write a message, sets the state of the FileWorker to crashed
if it does not succeed
and restarts the file worker if the crashed
flag was already set. Just logs an error if there
is no FileWorker at this uri
.
Messages that couldn't be sent can be queued up via the queueFailedMessage flag and
will be discharged after the FileWorker is restarted.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Server.Watchdog.handleDidOpen p = let doc := p.textDocument; Lean.Server.Watchdog.startFileWorker { uri := doc.uri, version := doc.version, text := String.toFileMap doc.text }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Server.Watchdog.handleDidClose p = Lean.Server.Watchdog.terminateFileWorker p.textDocument.uri
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- workerEvent: Lean.Server.Watchdog.FileWorker → Lean.Server.Watchdog.WorkerEvent → Lean.Server.Watchdog.ServerEvent
- clientMsg: Lean.JsonRpc.Message → Lean.Server.Watchdog.ServerEvent
- clientError: IO.Error → Lean.Server.Watchdog.ServerEvent
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.