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.

source
def Lean.Server.Watchdog.workerCfg :
IO.Process.StdioConfig
Equations

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

Instances For

source
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

Instances For

source
inductive Lean.Server.Watchdog.WorkerState :
Type

- crashed : WorkerState
- cannotWrite : WorkerState
- terminating : WorkerState
- running : WorkerState

Instances For

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

Instances For

source
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

Instances For

source
def Lean.Server.Watchdog.instInhabitedRequestQueueMap.default :
RequestQueueMap
Equations

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

Instances For

source
instance Lean.Server.Watchdog.instInhabitedRequestQueueMap :
Inhabited RequestQueueMap
Equations

- Lean.Server.Watchdog.instInhabitedRequestQueueMap = { default := Lean.Server.Watchdog.instInhabitedRequestQueueMap.default }

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

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

Instances For

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

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

source
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) }

Instances For

source
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

Instances For

source
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

Instances For

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

- m.contains id = m.reqs.contains id

Instances For

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

source
structure Lean.Server.Watchdog.RequestData :
Type

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

Instances For

source
def Lean.Server.Watchdog.instInhabitedRequestData.default :
RequestData
Equations

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

Instances For

source
instance Lean.Server.Watchdog.instInhabitedRequestData :
Inhabited RequestData
Equations

- Lean.Server.Watchdog.instInhabitedRequestData = { default := Lean.Server.Watchdog.instInhabitedRequestData.default }

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

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

Instances For

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

Instances For

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

Instances For

source
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 }

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Lean.Server.Watchdog.RequestDataMutex :
Type
Equations

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
structure Lean.Server.Watchdog.FileWorker :
Type

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
structure Lean.Server.Watchdog.FileWorkerMap :
Type

- fileWorkers : Std.TreeMap Lsp.DocumentUri FileWorker compare
- uriByMod : Std.TreeMap Name Lsp.DocumentUri Name.quickCmp

Instances For

source
def Lean.Server.Watchdog.FileWorkerMap.getUri? (m : FileWorkerMap) (id : Lsp.FileIdent) :
Option Lsp.DocumentUri
Equations

- m.getUri? (Lean.Lsp.FileIdent.uri uri) = some uri
- m.getUri? (Lean.Lsp.FileIdent.mod mod) = m.uriByMod.get? mod

Instances For

source
def Lean.Server.Watchdog.FileWorkerMap.insert (m : FileWorkerMap) (uri : Lsp.DocumentUri) (fw : FileWorker) :
FileWorkerMap
Equations

- m.insert uri fw = { fileWorkers := m.fileWorkers.insert uri fw, uriByMod := m.uriByMod.insert fw.doc.mod uri }

Instances For

source
def Lean.Server.Watchdog.FileWorkerMap.erase (m : FileWorkerMap) (uri : Lsp.DocumentUri) :
FileWorkerMap
Equations

- m.erase uri = (match m.fileWorkers.get? uri with | some fw => pure { fileWorkers := m.fileWorkers.erase uri, uriByMod := m.uriByMod.erase fw.doc.mod } | x => pure m).run

Instances For

source
def Lean.Server.Watchdog.FileWorkerMap.get? (m : FileWorkerMap) (uri : Lsp.DocumentUri) :
Option FileWorker
Equations

- m.get? uri = m.fileWorkers.get? uri

Instances For

source
@[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

Instances For

source
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).

Instances For

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

Instances For

source
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 ∅

Instances For

source
structure Lean.Server.Watchdog.RequestIDTranslation :
Type

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

Instances For

source
@[reducible, inline]
abbrev Lean.Server.Watchdog.PendingServerRequestMap :
Type
Equations

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

Instances For

source
structure Lean.Server.Watchdog.ServerRequestData :
Type

- pendingServerRequests : PendingServerRequestMap
- freshServerRequestID : Nat

Instances For

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

Instances For

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

Instances For

source
structure Lean.Server.Watchdog.WaitForILeanRequest :
Type

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

Instances For

source
structure Lean.Server.Watchdog.ReferenceData :
Type

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
structure Lean.Server.Watchdog.ReferenceRequestContext :
Type

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

Instances For

source
@[reducible, inline]
abbrev Lean.Server.Watchdog.ServerM (α : Type) :
Type
Equations

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

Instances For

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

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

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
def Lean.Server.Watchdog.getFileWorkerUri? (id : Lsp.FileIdent) :
ServerM (Option Lsp.DocumentUri)
Equations

- Lean.Server.Watchdog.getFileWorkerUri? id = do let __do_lift ← read let __do_lift ← ST.Ref.get __do_lift.fileWorkersRef pure (__do_lift.getUri? id)

Instances For

source
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 (__do_lift.get? uri)

Instances For

source
def Lean.Server.Watchdog.fileWorkerExists (id : Lsp.FileIdent) :
ServerM Bool
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
structure Lean.Server.Watchdog.ModuleQueryMatchScore :
Type

- isExactMatch : Bool
- score : Float

Instances For

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

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

Instances For

source
structure Lean.Server.Watchdog.ModuleQueryMatch extends Lean.Server.Watchdog.ModuleQueryMatchScore :
Type

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

Instances For

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

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Server.Watchdog.findDefinitions (fw : FileWorker) (p : Lsp.TextDocumentPositionParams) :
ServerM (Array Lsp.Location)
Equations

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

Instances For

source
def Lean.Server.Watchdog.parseRequestParams? (α : Type) [FromJson α] (request : String) :
Except String α
Equations

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

Instances For

source
def Lean.Server.Watchdog.parseNotificationParams? (α : Type) [FromJson α] (notification : String) :
Except String α
Equations

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

Instances For

source
def Lean.Server.Watchdog.parseResponseResult? (α : Type) [FromJson α] (response : String) :
Except String α
Equations

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

Instances For

source
def Lean.Server.Watchdog.bendLocationLinks (fw : FileWorker) (req : JsonRpc.Request Json) (r : Array Lsp.LeanLocationLink) :
ServerM Json
Equations

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

Instances For

source
def Lean.Server.Watchdog.handleResponseSpecialCases (fw : FileWorker) (req : JsonRpc.Request Json) (resp : String) :
ServerM String
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Server.Watchdog.tryWriteMessage (id : Lsp.FileIdent) (msg : JsonRpc.Message) :
ServerM Unit
Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
def Lean.Server.Watchdog.instFromJsonCallHierarchyItemData.fromJson :
Json → Except String CallHierarchyItemData
Equations

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

Instances For

source
instance Lean.Server.Watchdog.instFromJsonCallHierarchyItemData :
FromJson CallHierarchyItemData
Equations

- Lean.Server.Watchdog.instFromJsonCallHierarchyItemData = { fromJson? := Lean.Server.Watchdog.instFromJsonCallHierarchyItemData.fromJson }

source
instance Lean.Server.Watchdog.instToJsonCallHierarchyItemData :
ToJson CallHierarchyItemData
Equations

- Lean.Server.Watchdog.instToJsonCallHierarchyItemData = { toJson := Lean.Server.Watchdog.instToJsonCallHierarchyItemData.toJson }

source
def Lean.Server.Watchdog.instToJsonCallHierarchyItemData.toJson :
CallHierarchyItemData → Json
Equations

- Lean.Server.Watchdog.instToJsonCallHierarchyItemData.toJson x✝ = Lean.Json.mkObj [[("module", Lean.toJson x✝.module)], [("name", Lean.toJson x✝.name)]].flatten

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

source
inductive Lean.Server.Watchdog.ServerEvent :
Type

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

Instances For

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

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

Instances For

source
partial def Lean.Server.Watchdog.mainLoop (clientTask : ServerTask ServerEvent) :
ServerM Unit
source
def Lean.Server.Watchdog.mkLeanServerCapabilities :
Lsp.ServerCapabilities
Equations

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

Instances For

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

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

Instances For

source
def Lean.Server.Watchdog.findWorkerPath :
IO System.FilePath
Equations

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For