Documentation

Lean.Server.Watchdog

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 so that it can be resent to restarted workers. Then 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 an initialized notification to the worker.
After initialize, the watchdog sends the corresponding didOpen notification with the full current state of the file. No additional didOpen 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 a shutdown request. Similarly, they never receive a didClose 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.

def Lean.Server.Watchdog.workerCfg :

IO.Process.StdioConfig

Equations

Lean.Server.Watchdog.workerCfg = { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.inherit }

inductive Lean.Server.Watchdog.WorkerEvent :

Events that worker-specific tasks signal to the main thread.

terminated : WorkerEvent
importsChanged : WorkerEvent
crashed (e : IO.Error) : WorkerEvent
ioError (e : IO.Error) : WorkerEvent

inductive Lean.Server.Watchdog.CrashOrigin :

fileWorkerToClientForwarding : CrashOrigin
clientToFileWorkerForwarding : CrashOrigin

inductive Lean.Server.Watchdog.WorkerState :

crashed (queuedMsgs : Array JsonRpc.Message) (origin : CrashOrigin) : WorkerState
The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker and when reading a request reply. In the latter case, the forwarding task terminates and delegates a crashed event to the main task. Then, in both cases, the file worker has its state set to crashed and requests that are in-flight are errored. Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file worker arrives.
running : WorkerState

@[reducible, inline]

abbrev Lean.Server.Watchdog.PendingRequestMap :

Equations

Lean.Server.Watchdog.PendingRequestMap = Lean.RBMap Lean.JsonRpc.RequestID Lean.JsonRpc.Message compare

structure Lean.Server.Watchdog.FileWorker :

doc : DocumentMeta
proc : IO.Process.Child workerCfg
exitCode : Std.Mutex (Option UInt32)
commTask : Task WorkerEvent
state : WorkerState
pendingRequestsRef : IO.Ref PendingRequestMap
The pending requests map contains all requests that have been received from the LSP client, but were not answered yet. We need them for forwarding cancellation requests to the correct worker as well as cleanly aborting requests on worker crashes.

def Lean.Server.Watchdog.FileWorker.stdin (fw : FileWorker) :

Equations

fw.stdin = IO.FS.Stream.ofHandle fw.proc.stdin

def Lean.Server.Watchdog.FileWorker.stdout (fw : FileWorker) :

Equations

fw.stdout = IO.FS.Stream.ofHandle fw.proc.stdout

def Lean.Server.Watchdog.FileWorker.erasePendingRequest (fw : FileWorker) (id : JsonRpc.RequestID) :

Equations

fw.erasePendingRequest id = ST.Ref.modify fw.pendingRequestsRef fun (pendingRequests : Lean.Server.Watchdog.PendingRequestMap) => Lean.RBMap.erase pendingRequests id

def Lean.Server.Watchdog.FileWorker.errorPendingRequests (fw : FileWorker) (hError : IO.FS.Stream) (code : JsonRpc.ErrorCode) (msg : String) :

Equations

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

def Lean.Server.Watchdog.FileWorker.queuedMsgs (fw : FileWorker) :

Array JsonRpc.Message

Equations

fw.queuedMsgs = match fw.state with | Lean.Server.Watchdog.WorkerState.running => #[] | Lean.Server.Watchdog.WorkerState.crashed queuedMsgs origin => queuedMsgs

def Lean.Server.Watchdog.FileWorker.waitForProc (fw : FileWorker) :

Equations

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

def Lean.Server.Watchdog.FileWorker.killProcAndWait (fw : FileWorker) :

Equations

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

@[reducible, inline]

abbrev Lean.Server.Watchdog.FileWorkerMap :

Equations

Lean.Server.Watchdog.FileWorkerMap = Lean.RBMap Lean.Lsp.DocumentUri Lean.Server.Watchdog.FileWorker compare

@[reducible, inline]

abbrev Lean.Server.Watchdog.ImportMap :

Equations

Lean.Server.Watchdog.ImportMap = Lean.RBMap Lean.Lsp.DocumentUri (Lean.RBTree Lean.Lsp.DocumentUri compare) compare

structure Lean.Server.Watchdog.ImportData :

Global import data for all open files managed by this watchdog.

imports : ImportMap
For every open file, the files that it imports.
importedBy : ImportMap
For every open file, the files that it is imported by.

def Lean.Server.Watchdog.ImportData.update (d : ImportData) (uri : Lsp.DocumentUri) (imports : RBTree Lsp.DocumentUri compare) :

Updates d with the new set of imports for the file uri.

Equations

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

def Lean.Server.Watchdog.ImportData.eraseImportsOf (d : ImportData) (uri : Lsp.DocumentUri) :

Sets the imports of uri in d to the empty set.

Equations

d.eraseImportsOf uri = d.update uri ∅

structure Lean.Server.Watchdog.RequestIDTranslation :

sourceUri : Lsp.DocumentUri
localID : JsonRpc.RequestID

@[reducible, inline]

abbrev Lean.Server.Watchdog.PendingServerRequestMap :

Equations

Lean.Server.Watchdog.PendingServerRequestMap = Lean.RBMap Lean.JsonRpc.RequestID Lean.Server.Watchdog.RequestIDTranslation compare

structure Lean.Server.Watchdog.ServerRequestData :

pendingServerRequests : PendingServerRequestMap
freshServerRequestID : Nat

def Lean.Server.Watchdog.ServerRequestData.trackOutboundRequest (data : ServerRequestData) (sourceUri : Lsp.DocumentUri) (localID : JsonRpc.RequestID) :

JsonRpc.RequestID × ServerRequestData

Equations

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

def Lean.Server.Watchdog.ServerRequestData.translateInboundResponse (data : ServerRequestData) (globalID : JsonRpc.RequestID) :

Option RequestIDTranslation × ServerRequestData

Equations

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

structure Lean.Server.Watchdog.ServerContext :

hIn : IO.FS.Stream
hOut : IO.FS.Stream
hLog : IO.FS.Stream
args : List String
Command line arguments.
fileWorkersRef : IO.Ref FileWorkerMap
initParams : Lsp.InitializeParams
We store these to pass them to workers.
workerPath : System.FilePath
srcSearchPath : System.SearchPath
references : IO.Ref References
serverRequestData : IO.Ref ServerRequestData
importData : IO.Ref ImportData

@[reducible, inline]

abbrev Lean.Server.Watchdog.ServerM (α : Type) :

Equations

Lean.Server.Watchdog.ServerM = ReaderT Lean.Server.Watchdog.ServerContext IO

def Lean.Server.Watchdog.updateFileWorkers (val : FileWorker) :

Equations

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

def Lean.Server.Watchdog.findFileWorker? (uri : Lsp.DocumentUri) :

ServerM (Option FileWorker)

Equations

Lean.Server.Watchdog.findFileWorker? uri = do let __do_lift ← read let __do_lift ← ST.Ref.get __do_lift.fileWorkersRef pure (Lean.RBMap.find? __do_lift uri)

def Lean.Server.Watchdog.eraseFileWorker (uri : Lsp.DocumentUri) :

Equations

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

def Lean.Server.Watchdog.log (msg : String) :

Equations

Lean.Server.Watchdog.log msg = do let st ← read liftM (st.hLog.putStrLn msg) liftM st.hLog.flush

def Lean.Server.Watchdog.handleIleanInfoUpdate (fw : FileWorker) (params : Lsp.LeanIleanInfoParams) :

Equations

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

def Lean.Server.Watchdog.handleIleanInfoFinal (fw : FileWorker) (params : Lsp.LeanIleanInfoParams) :

Equations

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

def Lean.Server.Watchdog.handleImportClosure (fw : FileWorker) (params : Lsp.LeanImportClosureParams) :

Updates the global import data with the import closure provided by the file worker after it successfully processed its header.

Equations

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

def Lean.Server.Watchdog.startFileWorker (m : DocumentMeta) :

Equations

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

def Lean.Server.Watchdog.terminateFileWorker (uri : Lsp.DocumentUri) :

Equations

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

def Lean.Server.Watchdog.handleCrash (uri : Lsp.DocumentUri) (queuedMsgs : Array JsonRpc.Message) (origin : CrashOrigin) :

Equations

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

def Lean.Server.Watchdog.tryDischargeQueuedMessages (uri : Lsp.DocumentUri) (queuedMsgs : Array JsonRpc.Message) :

Equations

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

def Lean.Server.Watchdog.tryWriteMessage (uri : Lsp.DocumentUri) (msg : JsonRpc.Message) (queueFailedMessage : Bool := true) (restartCrashedWorker : Bool := false) :

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.

def Lean.Server.Watchdog.notifyAboutStaleDependency (uri staleDependency : Lsp.DocumentUri) :

Sends a notification to the file worker identified by uri that its dependency staleDependency is out-of-date.

Equations

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

def Lean.Server.Watchdog.findDefinitions (p : Lsp.TextDocumentPositionParams) :

ServerM (Array Lsp.Location)

Equations

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

def Lean.Server.Watchdog.handleReference (p : Lsp.ReferenceParams) :

ServerM (Array Lsp.Location)

Equations

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

structure Lean.Server.Watchdog.CallHierarchyItemData :

Used in CallHierarchyItem.data? to retain all the data needed to quickly re-identify the call hierarchy item.

module : Name
name : Name

Instances For

instance Lean.Server.Watchdog.instFromJsonCallHierarchyItemData :

FromJson CallHierarchyItemData

Equations

Lean.Server.Watchdog.instFromJsonCallHierarchyItemData = { fromJson? := Lean.Server.Watchdog.fromJsonCallHierarchyItemData✝ }

instance Lean.Server.Watchdog.instToJsonCallHierarchyItemData :

ToJson CallHierarchyItemData

Equations

Lean.Server.Watchdog.instToJsonCallHierarchyItemData = { toJson := Lean.Server.Watchdog.toJsonCallHierarchyItemData✝ }

def Lean.Server.Watchdog.CallHierarchyItemData.fromItem? (item : Lsp.CallHierarchyItem) :

Option CallHierarchyItemData

Extracts the CallHierarchyItemData from item.data? and returns none if this is not possible.

Equations

Lean.Server.Watchdog.CallHierarchyItemData.fromItem? item = do let __do_lift ← item.data? (Lean.fromJson? __do_lift).toOption

def Lean.Server.Watchdog.handlePrepareCallHierarchy (p : Lsp.CallHierarchyPrepareParams) :

ServerM (Array Lsp.CallHierarchyItem)

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyIncomingCalls (p : Lsp.CallHierarchyIncomingCallsParams) :

ServerM (Array Lsp.CallHierarchyIncomingCall)

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyIncomingCalls.collapseSameIncomingCalls (incomingCalls : Array Lsp.CallHierarchyIncomingCall) :

Array Lsp.CallHierarchyIncomingCall

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyOutgoingCalls (p : Lsp.CallHierarchyOutgoingCallsParams) :

ServerM (Array Lsp.CallHierarchyOutgoingCall)

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyOutgoingCalls.collapseSameOutgoingCalls (outgoingCalls : Array Lsp.CallHierarchyOutgoingCall) :

Array Lsp.CallHierarchyOutgoingCall

Equations

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

def Lean.Server.Watchdog.handleWorkspaceSymbol (p : Lsp.WorkspaceSymbolParams) :

ServerM (Array Lsp.SymbolInformation)

Equations

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

def Lean.Server.Watchdog.handlePrepareRename (p : Lsp.PrepareRenameParams) :

ServerM (Option Lsp.Range)

Equations

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

def Lean.Server.Watchdog.handleRename (p : Lsp.RenameParams) :

ServerM Lsp.WorkspaceEdit

Equations

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

def Lean.Server.Watchdog.handleDidOpen (p : Lsp.LeanDidOpenTextDocumentParams) :

Equations

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

def Lean.Server.Watchdog.handleDidChange (p : Lsp.DidChangeTextDocumentParams) :

Equations

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

def Lean.Server.Watchdog.handleDidSave (p : Lsp.DidSaveTextDocumentParams) :

When a file is saved, notifies all file workers for files that depend on this file that this specific import is now stale so that the file worker can issue a diagnostic asking users to restart the file.

Equations

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

def Lean.Server.Watchdog.handleDidClose (p : Lsp.DidCloseTextDocumentParams) :

Equations

Lean.Server.Watchdog.handleDidClose p = Lean.Server.Watchdog.terminateFileWorker p.textDocument.uri

def Lean.Server.Watchdog.handleDidChangeWatchedFiles (p : Lsp.DidChangeWatchedFilesParams) :

Equations

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

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

Equations

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

def Lean.Server.Watchdog.forwardNotification {α : Type} [ToJson α] [Lsp.FileSource α] (method : String) (params : α) :

Equations

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

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

ServerM paramType

Equations

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

def Lean.Server.Watchdog.forwardRequestToWorker (id : JsonRpc.RequestID) (method : String) (params : Json) :

Equations

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

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

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

def Lean.Server.Watchdog.handleResponse (id : JsonRpc.RequestID) (result : Json) :

Equations

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

def Lean.Server.Watchdog.handleResponseError (id : JsonRpc.RequestID) (code : JsonRpc.ErrorCode) (message : String) (data? : Option Json) :

Equations

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

def Lean.Server.Watchdog.shutdown :

Equations

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

inductive Lean.Server.Watchdog.ServerEvent :

workerEvent (fw : FileWorker) (ev : WorkerEvent) : ServerEvent
clientMsg (msg : JsonRpc.Message) : ServerEvent
clientError (e : IO.Error) : ServerEvent

def Lean.Server.Watchdog.runClientTask :

ServerM (Task ServerEvent)

Equations

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

partial def Lean.Server.Watchdog.mainLoop (clientTask : Task ServerEvent) :

def Lean.Server.Watchdog.mkLeanServerCapabilities :

Lsp.ServerCapabilities

Equations

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

def Lean.Server.Watchdog.initAndRunWatchdogAux :

Equations

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

def Lean.Server.Watchdog.findWorkerPath :

IO System.FilePath

Equations

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

def Lean.Server.Watchdog.startLoadingReferences (references : IO.Ref References) :

Starts loading .ileans present in the search path asynchronously in an IO task. This ensures that server startup is not blocked by loading the .ileans. In return, while the .ileans are being loaded, users will only get incomplete results in requests that need references.

Equations

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

def Lean.Server.Watchdog.initAndRunWatchdog (args : List String) (i o e : IO.FS.Stream) :

Equations

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

@[export lean_server_watchdog_main]

def Lean.Server.Watchdog.watchdogMain (args : List String) :

Equations

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