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 public 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.
• 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 }

inductive Lean.Server.Watchdog.WorkerEvent : Type

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

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

inductive Lean.Server.Watchdog.WorkerState : Type

• crashed : WorkerState
• cannotWrite : WorkerState
• terminating : WorkerState
• running : WorkerState

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

Equations

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

structure Lean.Server.Watchdog.RequestQueueMap : Type

• i : Nat
• reqs : Std.TreeMap JsonRpc.RequestID (Nat × JsonRpc.Request Json) compare
• queue : Std.TreeMap Nat (JsonRpc.RequestID × JsonRpc.Request Json) compare

instance Lean.Server.Watchdog.instInhabitedRequestQueueMap : Inhabited RequestQueueMap

Equations

• Lean.Server.Watchdog.instInhabitedRequestQueueMap = { default := { i := default, reqs := default, queue := default } }

def Lean.Server.Watchdog.RequestQueueMap.empty : RequestQueueMap

Equations

• Lean.Server.Watchdog.RequestQueueMap.empty = { i := 0, reqs := ∅, queue := ∅ }

instance Lean.Server.Watchdog.RequestQueueMap.instEmptyCollection : EmptyCollection RequestQueueMap

Equations

• Lean.Server.Watchdog.RequestQueueMap.instEmptyCollection = { emptyCollection := Lean.Server.Watchdog.RequestQueueMap.empty }

def Lean.Server.Watchdog.RequestQueueMap.enqueue (m : RequestQueueMap) (req : JsonRpc.Request Json) : RequestQueueMap

Equations

• m.enqueue req = { i := m.i + 1, reqs := m.reqs.insert req.id (m.i, req), queue := m.queue.insert m.i (req.id, req) }

def Lean.Server.Watchdog.RequestQueueMap.erase (m : RequestQueueMap) (id : JsonRpc.RequestID) : RequestQueueMap

Equations

• m.erase id = (match m.reqs.get? id with | some (i, snd) => pure { i := m.i, reqs := m.reqs.erase id, queue := m.queue.erase i } | x => pure m).run

def Lean.Server.Watchdog.RequestQueueMap.get? (m : RequestQueueMap) (id : JsonRpc.RequestID) : Option (JsonRpc.Request Json)

Equations

• m.get? id = do let __discr ← m.reqs.get? id match __discr with | (fst, msg) => pure msg

def Lean.Server.Watchdog.RequestQueueMap.contains (m : RequestQueueMap) (id : JsonRpc.RequestID) : Bool

Equations

• m.contains id = m.reqs.contains id

instance Lean.Server.Watchdog.RequestQueueMap.instForInProdRequestIDRequestJson {m : Type u_1 → Type u_2} : ForIn m RequestQueueMap (JsonRpc.RequestID × JsonRpc.Request Json)

Equations

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

structure Lean.Server.Watchdog.RequestData : Type

• requestQueues : Std.TreeMap Lsp.DocumentUri RequestQueueMap compare
• uriByRequest : Std.TreeMap JsonRpc.RequestID Lsp.DocumentUri compare

instance Lean.Server.Watchdog.instInhabitedRequestData : Inhabited RequestData

Equations

• Lean.Server.Watchdog.instInhabitedRequestData = { default := { requestQueues := default, uriByRequest := default } }

def Lean.Server.Watchdog.RequestData.empty : RequestData

Equations

• Lean.Server.Watchdog.RequestData.empty = { requestQueues := ∅, uriByRequest := ∅ }

def Lean.Server.Watchdog.RequestData.clearWorkerRequestData (d : RequestData) (uri : Lsp.DocumentUri) : RequestData

Equations

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

def Lean.Server.Watchdog.RequestData.enqueue (d : RequestData) (uri : Lsp.DocumentUri) (req : JsonRpc.Request Json) : RequestData

Equations

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

def Lean.Server.Watchdog.RequestData.erase (d : RequestData) (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : RequestData

Equations

• d.erase uri id = { requestQueues := d.requestQueues.modify uri fun (x : Lean.Server.Watchdog.RequestQueueMap) => x.erase id, uriByRequest := d.uriByRequest.erase id }

def Lean.Server.Watchdog.RequestData.contains (d : RequestData) (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : Bool

Equations

• d.contains uri id = (match d.uriByRequest.get? id with | some uri' => pure (uri == uri') | x => pure false).run

def Lean.Server.Watchdog.RequestData.getUri? (d : RequestData) (id : JsonRpc.RequestID) : Option Lsp.DocumentUri

Equations

• d.getUri? id = d.uriByRequest.get? id

def Lean.Server.Watchdog.RequestData.getRequest? (d : RequestData) (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : Option (JsonRpc.Request Json)

Equations

• d.getRequest? uri id = do let q ← d.requestQueues.get? uri q.get? id

def Lean.Server.Watchdog.RequestData.getRequestQueue (d : RequestData) (uri : Lsp.DocumentUri) : RequestQueueMap

Equations

• d.getRequestQueue uri = (d.requestQueues.get? uri).getD ∅

@[reducible, inline]

abbrev Lean.Server.Watchdog.RequestDataMutex : Type

Equations

• Lean.Server.Watchdog.RequestDataMutex = Std.Mutex Lean.Server.Watchdog.RequestData

def Lean.Server.Watchdog.RequestDataMutex.new : BaseIO RequestDataMutex

Equations

• Lean.Server.Watchdog.RequestDataMutex.new = Std.Mutex.new Lean.Server.Watchdog.RequestData.empty

def Lean.Server.Watchdog.RequestDataMutex.clearWorkerRequestData (m : RequestDataMutex) (uri : Lsp.DocumentUri) : BaseIO Unit

Equations

• m.clearWorkerRequestData uri = Std.Mutex.atomically m (modify fun (x : Lean.Server.Watchdog.RequestData) => x.clearWorkerRequestData uri)

def Lean.Server.Watchdog.RequestDataMutex.enqueue (m : RequestDataMutex) (uri : Lsp.DocumentUri) (req : JsonRpc.Request Json) : BaseIO Unit

Equations

• m.enqueue uri req = Std.Mutex.atomically m (modify fun (x : Lean.Server.Watchdog.RequestData) => x.enqueue uri req)

def Lean.Server.Watchdog.RequestDataMutex.erase (m : RequestDataMutex) (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : BaseIO Unit

Equations

• m.erase uri id = Std.Mutex.atomically m (modify fun (x : Lean.Server.Watchdog.RequestData) => x.erase uri id)

def Lean.Server.Watchdog.RequestDataMutex.contains (m : RequestDataMutex) (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : BaseIO Bool

Equations

• m.contains uri id = Std.Mutex.atomically m do let __do_lift ← get pure (__do_lift.contains uri id)

def Lean.Server.Watchdog.RequestDataMutex.getUri? (m : RequestDataMutex) (id : JsonRpc.RequestID) : BaseIO (Option Lsp.DocumentUri)

Equations

• m.getUri? id = Std.Mutex.atomically m do let __do_lift ← get pure (__do_lift.getUri? id)

def Lean.Server.Watchdog.RequestDataMutex.getRequestQueue (m : RequestDataMutex) (uri : Lsp.DocumentUri) : BaseIO RequestQueueMap

Equations

• m.getRequestQueue uri = Std.Mutex.atomically m do let __do_lift ← get pure (__do_lift.getRequestQueue uri)

structure Lean.Server.Watchdog.FileWorker : Type

• doc : DocumentMeta
• proc : IO.Process.Child workerCfg
• exitCode : Std.Mutex (Option UInt32)
• commTask : ServerTask WorkerEvent
• state : Std.Mutex WorkerState

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Server.Watchdog.FileWorkerMap : Type

Equations

• Lean.Server.Watchdog.FileWorkerMap = Std.TreeMap Lean.Lsp.DocumentUri Lean.Server.Watchdog.FileWorker compare

@[reducible, inline]

abbrev Lean.Server.Watchdog.ImportMap : Type

Equations

• Lean.Server.Watchdog.ImportMap = Std.TreeMap Lean.Lsp.DocumentUri (Std.TreeSet Lean.Lsp.DocumentUri compare) compare

structure Lean.Server.Watchdog.ImportData : Type

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

• imports : ImportMap

  For every open file, the files that it imports (transitively).

• importedBy : ImportMap

  For every open file, the open files that it is imported by (transitively).

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

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) : ImportData

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

Equations

• d.eraseImportsOf uri = d.update uri ∅

structure Lean.Server.Watchdog.RequestIDTranslation : Type

• sourceUri : Lsp.DocumentUri
• localID : JsonRpc.RequestID

@[reducible, inline]

abbrev Lean.Server.Watchdog.PendingServerRequestMap : Type

Equations

• Lean.Server.Watchdog.PendingServerRequestMap = Std.TreeMap Lean.JsonRpc.RequestID Lean.Server.Watchdog.RequestIDTranslation compare

structure Lean.Server.Watchdog.ServerRequestData : Type

• 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.WaitForILeanRequest : Type

• uri : Lsp.DocumentUri
• id : JsonRpc.RequestID
• version : Nat

structure Lean.Server.Watchdog.ReferenceData : Type

• loadingTask : ServerTask Unit
• references : References
• finalizedWorkerILeanVersions : Std.TreeMap Lsp.DocumentUri Nat compare
• pendingWaitForILeanRequests : Array WaitForILeanRequest

def Lean.Server.Watchdog.ReferenceData.modifyReferences (rd : ReferenceData) (f : References → References) : ReferenceData

Equations

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

def Lean.Server.Watchdog.ReferenceData.modifyReferencesM {m : Type → Type u_1} [Monad m] (rd : ReferenceData) (f : References → m References) : m ReferenceData

Equations

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

def Lean.Server.Watchdog.ReferenceData.modifyPendingWaitForILeanRequests (rd : ReferenceData) (f : Array WaitForILeanRequest → Array WaitForILeanRequest) : ReferenceData

Equations

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

def Lean.Server.Watchdog.ReferenceData.modifyFinalizedWorkerILeanVersions (rd : ReferenceData) (f : Std.TreeMap Lsp.DocumentUri Nat compare → Std.TreeMap Lsp.DocumentUri Nat compare) : ReferenceData

Equations

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

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 FileWorkerMap
• initParams : Lsp.InitializeParams

  We store these to pass them to workers.

• workerPath : System.FilePath
• referenceData : Std.Mutex ReferenceData
• serverRequestData : IO.Ref ServerRequestData
• importData : IO.Ref ImportData
• requestData : RequestDataMutex

structure Lean.Server.Watchdog.ReferenceRequestContext : Type

• fileWorkerMods : Std.TreeMap Lsp.DocumentUri Name compare
• references : References

@[reducible, inline]

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

Equations

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

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

Equations

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

def Lean.Server.Watchdog.getReferences : ServerM References

Equations

• Lean.Server.Watchdog.getReferences = do let __do_lift ← read let rd ← __do_lift.referenceData.atomically get pure rd.references

def Lean.Server.Watchdog.modifyReferences (f : References → References) : ServerM Unit

Equations

• Lean.Server.Watchdog.modifyReferences f = do let __do_lift ← read __do_lift.referenceData.atomically (modify fun (x : Lean.Server.Watchdog.ReferenceData) => x.modifyReferences f)

def Lean.Server.Watchdog.modifyReferencesIO (f : References → IO References) : ServerM Unit

Equations

• Lean.Server.Watchdog.modifyReferencesIO f = do let __do_lift ← read __do_lift.referenceData.atomically do let rd ← get let rd ← liftM (rd.modifyReferencesM f) set rd

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

Equations

• Lean.Server.Watchdog.getFileWorker? uri = do let __do_lift ← read let __do_lift ← ST.Ref.get __do_lift.fileWorkersRef pure (Std.TreeMap.get? __do_lift uri)

def Lean.Server.Watchdog.getFileWorkerMod? (uri : Lsp.DocumentUri) : ServerM (Option Name)

Equations

• Lean.Server.Watchdog.getFileWorkerMod? uri = do let __do_lift ← Lean.Server.Watchdog.getFileWorker? uri pure (Option.map (fun (x : Lean.Server.Watchdog.FileWorker) => x.doc.mod) __do_lift)

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

Equations

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

def Lean.Server.Watchdog.setWorkerState (fw : FileWorker) (s : WorkerState) : ServerM Unit

Equations

• Lean.Server.Watchdog.setWorkerState fw s = fw.state.atomically (set s)

def Lean.Server.Watchdog.getWorkerState (fw : FileWorker) : ServerM WorkerState

Equations

• Lean.Server.Watchdog.getWorkerState fw = fw.state.atomically get

def Lean.Server.Watchdog.errorPendingRequests (uri : Lsp.DocumentUri) (code : JsonRpc.ErrorCode) (msg : String) : ServerM Unit

Equations

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

def Lean.Server.Watchdog.eraseGetPendingRequest (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : ServerM (Option (JsonRpc.Request Json))

Equations

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

def Lean.Server.Watchdog.erasePendingRequest (uri : Lsp.DocumentUri) (id : JsonRpc.RequestID) : ServerM Bool

Equations

• Lean.Server.Watchdog.erasePendingRequest uri id = do let r? ← Lean.Server.Watchdog.eraseGetPendingRequest uri id pure r?.isSome

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

Equations

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

def Lean.Server.Watchdog.handleILeanHeaderInfo (fw : FileWorker) (params : Lsp.LeanILeanHeaderInfoParams) : ServerM Unit

Equations

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

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

Equations

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

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

Equations

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

def Lean.Server.Watchdog.emitServerRequestResponse {α : Type u_1} [ToJson α] (fw : FileWorker) (r : JsonRpc.Response α) : IO Unit

Equations

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

def Lean.Server.Watchdog.emitServerRequestResponseError (fw : FileWorker) (r : JsonRpc.ResponseError Unit) : IO Unit

Equations

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

structure Lean.Server.Watchdog.ModuleQueryMatchScore : Type

• isExactMatch : Bool
• score : Float

def Lean.Server.Watchdog.ModuleQueryMatchScore.compare (ms1 ms2 : ModuleQueryMatchScore) : Ordering

Equations

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

structure Lean.Server.Watchdog.ModuleQueryMatchextends Lean.Server.Watchdog.ModuleQueryMatchScore : Type

• isExactMatch : Bool
• score : Float
• decl : Name
• declAsString : String

def Lean.Server.Watchdog.ModuleQueryMatch.fastCompare (m1 m2 : ModuleQueryMatch) : Ordering

Equations

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

def Lean.Server.Watchdog.ModuleQueryMatch.compare (m1 m2 : ModuleQueryMatch) : Ordering

Equations

• m1.compare m2 = if m2.decl.isSuffixOf m1.decl = true then Ordering.lt else if m1.decl.isSuffixOf m2.decl = true then Ordering.gt else m1.fastCompare m2

def Lean.Server.Watchdog.matchAgainstQuery? (query : Lsp.LeanModuleQuery) (decl : Name) : Option ModuleQueryMatch

Equations

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

def Lean.Server.Watchdog.handleQueryModule (fw : FileWorker) (id : JsonRpc.RequestID) (params : Lsp.LeanQueryModuleParams) : ServerM (ServerTask Unit × IO.CancelToken)

Equations

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

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

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.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.handleResponseSpecialCases (req : JsonRpc.Request Json) (resp : JsonRpc.Response Json) : ServerM (JsonRpc.Response Json)

Equations

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

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

Equations

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

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

Equations

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

def Lean.Server.Watchdog.tryWriteMessage (uri : Lsp.DocumentUri) (msg : JsonRpc.Message) : ServerM Unit

Equations

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

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

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.handleReference (p : Lsp.ReferenceParams) : ReaderT ReferenceRequestContext IO (Array Lsp.Location)

Equations

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

structure Lean.Server.Watchdog.CallHierarchyItemData : Type

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

• module : Name
• name : Name

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) : ReaderT ReferenceRequestContext IO (Array Lsp.CallHierarchyItem)

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyIncomingCalls (p : Lsp.CallHierarchyIncomingCallsParams) : ReaderT ReferenceRequestContext IO (Array Lsp.CallHierarchyIncomingCall)

Equations

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

def Lean.Server.Watchdog.handleCallHierarchyOutgoingCalls (p : Lsp.CallHierarchyOutgoingCallsParams) : ReaderT ReferenceRequestContext IO (Array Lsp.CallHierarchyOutgoingCall)

Equations

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

def Lean.Server.Watchdog.handlePrepareModuleHierarchy (p : Lsp.LeanPrepareModuleHierarchyParams) : ReaderT ReferenceRequestContext IO (Option Lsp.LeanModule)

Equations

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

def Lean.Server.Watchdog.sortModuleImports (imports : Array ModuleImport) : Array ModuleImport

Equations

• Lean.Server.Watchdog.sortModuleImports imports = (imports.toList.mergeSort fun (x1 x2 : Lean.Server.ModuleImport) => compare x1.module.toString x2.module.toString == Ordering.lt).toArray

def Lean.Server.Watchdog.handleModuleHierarchyImports (p : Lsp.LeanModuleHierarchyImportsParams) : ReaderT ReferenceRequestContext IO (Array Lsp.LeanImport)

Equations

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

def Lean.Server.Watchdog.handleModuleHierarchyImportedBy (p : Lsp.LeanModuleHierarchyImportedByParams) : ReaderT ReferenceRequestContext IO (Array Lsp.LeanImport)

Equations

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

def Lean.Server.Watchdog.handleWorkspaceSymbol (p : Lsp.WorkspaceSymbolParams) : ReaderT ReferenceRequestContext IO (Array Lsp.SymbolInformation)

Equations

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

def Lean.Server.Watchdog.handlePrepareRename (p : Lsp.PrepareRenameParams) : ReaderT ReferenceRequestContext IO (Option Lsp.Range)

Equations

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

def Lean.Server.Watchdog.handleRename (p : Lsp.RenameParams) : ReaderT ReferenceRequestContext IO Lsp.WorkspaceEdit

Equations

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

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

Equations

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

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

Equations

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

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

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) : ServerM Unit

Equations

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

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

Equations

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

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

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 : α) : ServerM Unit

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) : ServerM Unit

Equations

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

def Lean.Server.Watchdog.handleReferenceRequest (α β : Type) [FromJson α] [ToJson β] (id : JsonRpc.RequestID) (params : Json) (handler : α → ReaderT ReferenceRequestContext IO β) : ServerM Unit

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) : ServerM Unit

Equations

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

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

Equations

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

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

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) : ServerM Unit

Equations

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

def Lean.Server.Watchdog.shutdown : ServerM Unit

Equations

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

inductive Lean.Server.Watchdog.ServerEvent : Type

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

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

Equations

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

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

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 : ServerM Unit

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 (referenceData : Std.Mutex ReferenceData) : IO Unit

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) : IO Unit

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) : IO UInt32

Equations

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