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

inductive Lean.Server.Watchdog.WorkerEvent : Type

• terminated: Lean.Server.Watchdog.WorkerEvent
• importsChanged: 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.

inductive Lean.Server.Watchdog.WorkerState : Type

• crashed: Array Lean.JsonRpc.Message → Lean.Server.Watchdog.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: Lean.Server.Watchdog.WorkerState

@[inline, reducible]

abbrev Lean.Server.Watchdog.PendingRequestMap : Type

structure Lean.Server.Watchdog.FileWorker : Type

• doc : Lean.Server.DocumentMeta
• proc : IO.Process.Child Lean.Server.Watchdog.workerCfg
• commTask : Task Lean.Server.Watchdog.WorkerEvent
• state : Lean.Server.Watchdog.WorkerState
• pendingRequestsRef : IO.Ref Lean.Server.Watchdog.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 forwaring cancellation requests to the correct worker as well as cleanly aborting requests on worker crashes.

def Lean.Server.Watchdog.FileWorker.stdin (fw : Lean.Server.Watchdog.FileWorker) : IO.FS.Stream

def Lean.Server.Watchdog.FileWorker.stdout (fw : Lean.Server.Watchdog.FileWorker) : IO.FS.Stream

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

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

@[inline, reducible]

abbrev Lean.Server.Watchdog.FileWorkerMap : Type

structure Lean.Server.Watchdog.ServerContext : Type

• hIn : IO.FS.Stream
• hOut : IO.FS.Stream
• hLog : IO.FS.Stream
• args : List String

  Command line arguments.

• fileWorkersRef : IO.Ref Lean.Server.Watchdog.FileWorkerMap
• initParams : Lean.Lsp.InitializeParams

  We store these to pass them to workers.

• workerPath : Lake.FilePath
• srcSearchPath : Lake.SearchPath
• references : IO.Ref Lean.Server.References

@[inline, reducible]

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

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

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

def Lean.Server.Watchdog.findFileWorker! (uri : Lean.Lsp.DocumentUri) : Lean.Server.Watchdog.ServerM Lean.Server.Watchdog.FileWorker

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

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

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

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

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

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

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

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

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.

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

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

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

def Lean.Server.Watchdog.handleDidOpen (p : Lean.Lsp.DidOpenTextDocumentParams) : Lean.Server.Watchdog.ServerM Unit

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

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

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

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

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

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

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

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

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

def Lean.Server.Watchdog.shutdown : Lean.Server.Watchdog.ServerM Unit

inductive Lean.Server.Watchdog.ServerEvent : Type

• 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

def Lean.Server.Watchdog.runClientTask : Lean.Server.Watchdog.ServerM (Task Lean.Server.Watchdog.ServerEvent)

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

def Lean.Server.Watchdog.mkLeanServerCapabilities : Lean.Lsp.ServerCapabilities

def Lean.Server.Watchdog.initAndRunWatchdogAux : Lean.Server.Watchdog.ServerM Unit

def Lean.Server.Watchdog.findWorkerPath : IO Lake.FilePath

def Lean.Server.Watchdog.loadReferences : IO Lean.Server.References

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

@[export lean_server_watchdog_main]

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