Lean.Server.Watchdog

Lean.Server.Watchdog.FileWorker.errorPendingRequests fw hError code msg = do let pendingRequests ← ST.Ref.modifyGet fw.pendingRequestsRef fun pendingRequests => (pendingRequests, Std.RBMap.empty) let r ← forIn pendingRequests PUnit.unit fun x r => match x with | (id, x) => do IO.FS.Stream.writeLspResponseError hError { id := id, code := code, message := msg, data? := none } pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

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

IO (Task Lean.Server.Watchdog.WorkerEvent)

Equations

Lean.Server.Watchdog.FileWorker.runEditsSignalTask fw = (fun loopAction => do let t ← liftM (IO.asTask loopAction Task.Priority.default) pure (Task.map (fun x => match x with | Except.ok ev => ev | Except.error e => Lean.Server.Watchdog.WorkerEvent.ioError e) t)) (Lean.Server.Watchdog.FileWorker.runEditsSignalTask.loopAction fw)

source

partial def Lean.Server.Watchdog.FileWorker.runEditsSignalTask.loopAction (fw : Lean.Server.Watchdog.FileWorker) :

IO Lean.Server.Watchdog.WorkerEvent

source

@[inline]

abbrev Lean.Server.Watchdog.FileWorkerMap :

Type

Equations

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

source

structure Lean.Server.Watchdog.ServerContext :

Type

hIn : IO.FS.Stream
hOut : IO.FS.Stream
hLog : IO.FS.Stream
args : List String
fileWorkersRef : IO.Ref Lean.Server.Watchdog.FileWorkerMap
initParams : Lean.Lsp.InitializeParams
editDelay : Nat
workerPath : System.FilePath
srcSearchPath : System.SearchPath
references : IO.Ref Lean.Server.References

source

@[inline]

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

Type

Equations

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

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.updateFileWorkers val = do let a ← read ST.Ref.modify a.fileWorkersRef fun fileWorkers => Std.RBMap.insert fileWorkers val.doc.meta.uri val

source

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

Lean.Server.Watchdog.ServerM (Option Lean.Server.Watchdog.FileWorker)

Equations

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

source

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

Lean.Server.Watchdog.ServerM Lean.Server.Watchdog.FileWorker

Equations

Lean.Server.Watchdog.findFileWorker! uri = do let discr ← Lean.Server.Watchdog.findFileWorker? uri match discr with | some fw => pure fw | x => liftM (IO.throwServerError (toString "cannot find open document '" ++ toString uri ++ toString "'"))

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.eraseFileWorker uri = do let s ← read ST.Ref.modify s.fileWorkersRef fun fileWorkers => Std.RBMap.erase fileWorkers uri match Lean.Lsp.DocumentUri.toPath? uri with | some path => do let a ← liftM (Lean.searchModuleNameOfFileName path s.srcSearchPath) match a with | some module => ST.Ref.modify s.references fun refs => Lean.Server.References.removeWorkerRefs refs module | x => pure PUnit.unit | x => pure PUnit.unit

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

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

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleIleanInfoUpdate fw params = do let s ← read match Lean.Lsp.DocumentUri.toPath? fw.doc.meta.uri with | some path => do let a ← liftM (Lean.searchModuleNameOfFileName path s.srcSearchPath) match a with | some module => ST.Ref.modify s.references fun refs => Lean.Server.References.updateWorkerRefs refs module params.version params.references | x => pure PUnit.unit | x => pure PUnit.unit

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleIleanInfoFinal fw params = do let s ← read match Lean.Lsp.DocumentUri.toPath? fw.doc.meta.uri with | some path => do let a ← liftM (Lean.searchModuleNameOfFileName path s.srcSearchPath) match a with | some module => ST.Ref.modify s.references fun refs => Lean.Server.References.finalizeWorkerRefs refs module params.version params.references | x => pure PUnit.unit | x => pure PUnit.unit

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.startFileWorker m = do let a ← read liftM (Lean.Server.publishProgressAtPos m 0 a.hOut Lean.Lsp.LeanFileProgressKind.processing) let st ← read let headerAst ← liftM (Lean.Server.Watchdog.parseHeaderAst m.text.source) let workerProc ← liftM (IO.Process.spawn { toStdioConfig := Lean.Server.Watchdog.workerCfg, cmd := st.workerPath.toString, args := #["--worker"] ++ List.toArray st.args ++ #[m.uri], cwd := none, env := #[] }) let pendingRequestsRef ← liftM (IO.mkRef Std.RBMap.empty) let a ← liftM (IO.mkRef none) let fw : Lean.Server.Watchdog.FileWorker := { doc := { meta := m, headerAst := headerAst }, proc := workerProc, commTask := { get := Lean.Server.Watchdog.WorkerEvent.terminated }, state := Lean.Server.Watchdog.WorkerState.running, pendingRequestsRef := pendingRequestsRef, groupedEditsRef := a } let commTask ← Lean.Server.Watchdog.forwardMessages fw let fw : Lean.Server.Watchdog.FileWorker := { doc := fw.doc, proc := fw.proc, commTask := commTask, state := fw.state, pendingRequestsRef := fw.pendingRequestsRef, groupedEditsRef := fw.groupedEditsRef } liftM (IO.FS.Stream.writeLspRequest (Lean.Server.Watchdog.FileWorker.stdin fw) { id := 0, method := "initialize", param := st.initParams }) liftM (IO.FS.Stream.writeLspNotification (Lean.Server.Watchdog.FileWorker.stdin fw) { method := "textDocument/didOpen", param := { textDocument := { uri := m.uri, languageId := "lean", version := m.version, text := m.text.source } } }) Lean.Server.Watchdog.updateFileWorkers fw

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.terminateFileWorker uri = do let fw ← Lean.Server.Watchdog.findFileWorker! uri let r ← tryCatch (do let y ← liftM (IO.FS.Stream.writeLspMessage (Lean.Server.Watchdog.FileWorker.stdin fw) (Lean.JsonRpc.Message.notification "exit" none)) pure (DoResultPR.pure y PUnit.unit)) fun x => pure (DoResultPR.return PUnit.unit PUnit.unit) let _do_jp : Unit → Lean.Server.Watchdog.ServerM Unit := fun y => Lean.Server.Watchdog.eraseFileWorker uri match r with | DoResultPR.pure a u => let x := u; do let y ← pure a _do_jp y | DoResultPR.return b u => let x := u; pure b

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleCrash uri queuedMsgs = do let a ← Lean.Server.Watchdog.findFileWorker! uri Lean.Server.Watchdog.updateFileWorkers { doc := a.doc, proc := a.proc, commTask := a.commTask, state := Lean.Server.Watchdog.WorkerState.crashed queuedMsgs, pendingRequestsRef := a.pendingRequestsRef, groupedEditsRef := a.groupedEditsRef }

source

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

Equations

Lean.Server.Watchdog.tryWriteMessage uri msg queueFailedMessage restartCrashedWorker = do let discr ← Lean.Server.Watchdog.findFileWorker? uri match discr with | some fw => do let pendingEdit ← ST.Ref.modifyGet fw.groupedEditsRef fun x => match x with | some ge => (true, some { applyTime := ge.applyTime, params := ge.params, signalTask := ge.signalTask, queuedMsgs := Array.push ge.queuedMsgs msg }) | none => (false, none) let _do_jp : PUnit → Lean.Server.Watchdog.ServerM Unit := fun y => match fw.state with | Lean.Server.Watchdog.WorkerState.crashed queuedMsgs => let queuedMsgs := queuedMsgs; let _do_jp := fun queuedMsgs y => let _do_jp := fun y => do Lean.Server.Watchdog.eraseFileWorker uri Lean.Server.Watchdog.startFileWorker fw.doc.meta let newFw ← Lean.Server.Watchdog.findFileWorker! uri let crashedMsgs : Array Lean.JsonRpc.Message := #[] let r ← forIn queuedMsgs crashedMsgs fun msg r => let crashedMsgs := r; do let r ← tryCatch (do let y ← liftM (IO.FS.Stream.writeLspMessage (Lean.Server.Watchdog.FileWorker.stdin newFw) msg) pure { fst := y, snd := crashedMsgs }) fun x => let crashedMsgs := Array.push crashedMsgs msg; do let y ← pure PUnit.unit pure { fst := y, snd := crashedMsgs } let x : Array Lean.JsonRpc.Message := r.snd let crashedMsgs : Array Lean.JsonRpc.Message := x pure r.fst pure (ForInStep.yield crashedMsgs) let x : Array Lean.JsonRpc.Message := r let crashedMsgs : Array Lean.JsonRpc.Message := x if ¬Array.isEmpty crashedMsgs = true then Lean.Server.Watchdog.handleCrash uri crashedMsgs else pure PUnit.unit; if (!restartCrashedWorker) = true then pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y; if queueFailedMessage = true then let queuedMsgs := Array.push queuedMsgs msg; do let y ← pure PUnit.unit _do_jp queuedMsgs y else do let y ← pure PUnit.unit _do_jp queuedMsgs y | Lean.Server.Watchdog.WorkerState.running => let initialQueuedMsgs := if queueFailedMessage = true then #[msg] else #[]; tryCatch (liftM (IO.FS.Stream.writeLspMessage (Lean.Server.Watchdog.FileWorker.stdin fw) msg)) fun x => Lean.Server.Watchdog.handleCrash uri initialQueuedMsgs if pendingEdit = true then pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y | x => do let a ← read liftM (IO.FS.Stream.putStrLn a.hLog (toString "Cannot send message to unknown document '" ++ toString uri ++ toString "':\n" ++ toString (Lean.Json.compress (Lean.toJson msg)) ++ toString "")) pure PUnit.unit

source

def Lean.Server.Watchdog.findDefinition? (p : Lean.Lsp.TextDocumentPositionParams) :

Lean.Server.Watchdog.ServerM (Option Lean.Lsp.Location)

Equations

Lean.Server.Watchdog.findDefinition? p = let _do_jp := fun y => pure none; match Lean.Lsp.DocumentUri.toPath? p.textDocument.uri with | some path => do let a ← read let srcSearchPath : System.SearchPath := a.srcSearchPath let a ← liftM (Lean.searchModuleNameOfFileName path srcSearchPath) match a with | some module => do let a ← read let references ← ST.Ref.get a.references match Lean.Server.References.findAt? references module p.position with | some ident => do let a ← liftM (Lean.Server.References.definitionOf? references ident srcSearchPath) pure a | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y

source

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

Lean.Server.Watchdog.ServerM (Array Lean.Lsp.Location)

Equations

Lean.Server.Watchdog.handleReference p = let _do_jp := fun y => pure #[]; match Lean.Lsp.DocumentUri.toPath? p.toTextDocumentPositionParams.textDocument.uri with | some path => do let a ← read let srcSearchPath : System.SearchPath := a.srcSearchPath let a ← liftM (Lean.searchModuleNameOfFileName path srcSearchPath) match a with | some module => do let a ← read let references ← ST.Ref.get a.references match Lean.Server.References.findAt? references module p.toTextDocumentPositionParams.position with | some ident => do let a ← liftM (Lean.Server.References.referringTo references ident srcSearchPath p.context.includeDeclaration) pure a | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y

source

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

Lean.Server.Watchdog.ServerM (Array Lean.Lsp.SymbolInformation)

Equations

Lean.Server.Watchdog.handleWorkspaceSymbol p = (fun containsInOrder => do let a ← read let references ← ST.Ref.get a.references let a ← read let srcSearchPath : System.SearchPath := a.srcSearchPath let symbols ← liftM (Lean.Server.References.definitionsMatching references srcSearchPath (fun name => let name := Option.getD (Lean.privateToUserName? name) name; if containsCaseInsensitive p.query (Lean.Name.toString name) = true then some (Lean.Name.toString name) else none) (some 100)) pure (Array.map (fun x => match x with | (name, location) => { name := name, kind := Lean.Lsp.SymbolKind.constant, tags := #[], location := location, containerName? := none }) symbols)) Lean.Server.Watchdog.handleWorkspaceSymbol.containsCaseInsensitive Lean.Server.Watchdog.handleWorkspaceSymbol.containsInOrder

source

def Lean.Server.Watchdog.handleWorkspaceSymbol.containsCaseInsensitive (value : String) :

String → Bool

Equations

Lean.Server.Watchdog.handleWorkspaceSymbol.containsCaseInsensitive value = if (String.any value fun a => Char.isUpper a) = true then Lean.Server.Watchdog.handleWorkspaceSymbol.containsInOrder value else let value := String.toLower value; fun target => Lean.Server.Watchdog.handleWorkspaceSymbol.containsInOrder value (String.toLower target)

source

def Lean.Server.Watchdog.handleWorkspaceSymbol.containsInOrder (value : String) (target : String) :

Bool

Equations

Lean.Server.Watchdog.handleWorkspaceSymbol.containsInOrder value target = Id.run (let _do_jp := fun y => let valueIt := String.mkIterator value; let targetIt := String.mkIterator target; do let r ← let col := { start := 0, stop := String.bsize target, step := 1 }; forIn col { fst := none, snd := { fst := targetIt, snd := valueIt } } fun x r => let r := r.snd; let targetIt := r.fst; let valueIt := r.snd; let _do_jp := fun targetIt valueIt y => let targetIt := String.Iterator.next targetIt; do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := { fst := targetIt, snd := valueIt } }); if (String.Iterator.curr valueIt == String.Iterator.curr targetIt) = true then let valueIt := String.Iterator.next valueIt; if (!String.Iterator.hasNext valueIt) = true then pure (ForInStep.done { fst := some true, snd := { fst := targetIt, snd := valueIt } }) else do let y ← pure PUnit.unit _do_jp targetIt valueIt y else do let y ← pure PUnit.unit _do_jp targetIt valueIt y let x : MProd String.Iterator String.Iterator := r.snd match x with | { fst := targetIt, snd := valueIt } => let _do_jp := fun y => pure false; match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a; if (String.length value == 0) = true then pure true else do let y ← pure PUnit.unit _do_jp y)

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleDidOpen p = let doc := p.textDocument; Lean.Server.Watchdog.startFileWorker { uri := doc.uri, version := doc.version, text := String.toFileMap doc.text }

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleEdits fw = do let discr ← ST.Ref.modifyGet fw.groupedEditsRef fun a => (a, none) match discr with | some ge => let doc := ge.params.textDocument; let changes := ge.params.contentChanges; let oldDoc := fw.doc; do let discr ← pure doc.version? match discr with | some newVersion => let _do_jp := fun y => let _do_jp := fun y => let newDocText := Lean.Server.foldDocumentChanges changes oldDoc.meta.text; let newMeta := { uri := doc.uri, version := newVersion, text := newDocText }; do let newHeaderAst ← liftM (Lean.Server.Watchdog.parseHeaderAst newDocText.source) if (newHeaderAst != oldDoc.headerAst) = true then do Lean.Server.Watchdog.terminateFileWorker doc.uri Lean.Server.Watchdog.startFileWorker newMeta else let newDoc := { meta := newMeta, headerAst := oldDoc.headerAst }; do Lean.Server.Watchdog.updateFileWorkers { doc := newDoc, proc := fw.proc, commTask := fw.commTask, state := fw.state, pendingRequestsRef := fw.pendingRequestsRef, groupedEditsRef := fw.groupedEditsRef } Lean.Server.Watchdog.tryWriteMessage doc.uri (Lean.JsonRpc.Message.notification { method := "textDocument/didChange", param := ge.params }.method (Except.toOption (Lean.Json.toStructured? { method := "textDocument/didChange", param := ge.params }.param))) true true let r ← let col := ge.queuedMsgs; forIn col PUnit.unit fun msg r => do Lean.Server.Watchdog.tryWriteMessage doc.uri msg true false pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit; if Array.isEmpty changes = true then pure PUnit.unit else do let y ← pure PUnit.unit _do_jp y; if newVersion ≤ oldDoc.meta.version then do let y ← liftM (IO.throwServerError "Got outdated version number") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => liftM (IO.throwServerError "Expected version number") | x => liftM (IO.throwServerError "Internal error: empty grouped edits reference")

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

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

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleDidChangeWatchedFiles p = do let a ← read let references : IO.Ref Lean.Server.References := a.references let oleanSearchPath ← ST.Ref.get Lean.searchPathRef let ileans ← liftM (Lean.SearchPath.findAllWithExt oleanSearchPath "ilean") let r ← let col := p.changes; forIn col PUnit.unit fun change r => match Lean.Lsp.DocumentUri.toPath? change.uri with | some path => match change.type with | Lean.Lsp.FileChangeType.Deleted => do ST.Ref.modify references fun r => Lean.Server.References.removeIlean r path pure (ForInStep.yield PUnit.unit) | x => if Array.contains ileans path = true then do let ilean ← liftM (Lean.Server.Ilean.load path) match change.type with | Lean.Lsp.FileChangeType.Changed => do ST.Ref.modify references fun r => Lean.Server.References.addIlean (Lean.Server.References.removeIlean r path) path ilean pure (ForInStep.yield PUnit.unit) | x => do ST.Ref.modify references fun r => Lean.Server.References.addIlean r path ilean pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) | x => do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleCancelRequest p = do let a ← read let fileWorkers ← ST.Ref.get a.fileWorkersRef let r ← forIn fileWorkers PUnit.unit fun x r => match x with | (uri, fw) => do let a ← ST.Ref.get fw.pendingRequestsRef if Std.RBMap.contains a p.id = true then do Lean.Server.Watchdog.tryWriteMessage uri (Lean.JsonRpc.Message.notification { method := "$/cancelRequest", param := p }.method (Except.toOption (Lean.Json.toStructured? { method := "$/cancelRequest", param := p }.param))) false false pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.forwardNotification method params = Lean.Server.Watchdog.tryWriteMessage (Lean.Lsp.fileSource params) (Lean.JsonRpc.Message.notification { method := method, param := params }.method (Except.toOption (Lean.Json.toStructured? { method := method, param := params }.param))) true false

source

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

Lean.Server.Watchdog.ServerM paramType

Equations

Lean.Server.Watchdog.parseParams paramType params = match Lean.fromJson? params with | Except.ok parsed => pure parsed | Except.error inner => liftM (IO.throwServerError (toString "Got param with wrong structure: " ++ toString (Lean.Json.compress params) ++ toString "\n" ++ toString inner ++ toString ""))

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.forwardRequestToWorker id method params = let _do_jp := fun uri => do let discr ← Lean.Server.Watchdog.findFileWorker? uri match discr with | some fw => let r := { id := id, method := method, param := params }; do ST.Ref.modify fw.pendingRequestsRef fun a => Std.RBMap.insert a id (Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param))) Lean.Server.Watchdog.tryWriteMessage uri (Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param))) true false | x => do let a ← read liftM (IO.FS.Stream.writeLspResponseError a.hOut { id := id, code := Lean.JsonRpc.ErrorCode.contentModified, message := toString "Cannot process request to closed file '" ++ toString uri ++ toString "'", data? := none }) pure PUnit.unit; if (method == "$/lean/rpc/connect") = true then do let ps ← Lean.Server.Watchdog.parseParams Lean.Lsp.RpcConnectParams params let y ← pure (Lean.Lsp.fileSource ps) _do_jp y else do let a ← liftM (Lean.Server.routeLspRequest method params) match a with | Except.error e => do let a ← read liftM (IO.FS.Stream.writeLspResponseError a.hOut (Lean.Server.RequestError.toLspResponseError id e)) pure PUnit.unit | Except.ok uri => do let y ← pure uri _do_jp y

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleRequest id method params = let handle := fun α β [Lean.FromJson α] [Lean.ToJson β] handler => do let a ← read let hOut : IO.FS.Stream := a.hOut tryCatch (do let params ← Lean.Server.Watchdog.parseParams α params let result ← handler params liftM (IO.FS.Stream.writeLspResponse hOut { id := id, result := result })) fun ex => let e := ex; liftM (IO.FS.Stream.writeLspResponseError hOut { id := id, code := Lean.JsonRpc.ErrorCode.internalError, message := toString "Failed to process request " ++ toString id ++ toString ": " ++ toString e ++ toString "", data? := none }); let _do_jp := fun y => match method with | "textDocument/references" => handle Lean.Lsp.ReferenceParams (Array Lean.Lsp.Location) Lean.Server.Watchdog.handleReference | "workspace/symbol" => handle Lean.Lsp.WorkspaceSymbolParams (Array Lean.Lsp.SymbolInformation) Lean.Server.Watchdog.handleWorkspaceSymbol | x => Lean.Server.Watchdog.forwardRequestToWorker id method params; if (method == "textDocument/definition" || method == "textDocument/declaration") = true then do let params ← Lean.Server.Watchdog.parseParams Lean.Lsp.TextDocumentPositionParams params let a ← Lean.Server.Watchdog.findDefinition? params match a with | some definition => do let a ← read liftM (IO.FS.Stream.writeLspResponse a.hOut { id := id, result := #[definition] }) pure PUnit.unit | x => do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

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

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.handleNotification method params = let handle := fun α [Lean.FromJson α] handler => Lean.Server.Watchdog.parseParams α params >>= handler; match method with | "textDocument/didOpen" => handle Lean.Lsp.DidOpenTextDocumentParams Lean.Server.Watchdog.handleDidOpen | "textDocument/didClose" => handle Lean.Lsp.DidCloseTextDocumentParams Lean.Server.Watchdog.handleDidClose | "workspace/didChangeWatchedFiles" => handle Lean.Lsp.DidChangeWatchedFilesParams Lean.Server.Watchdog.handleDidChangeWatchedFiles | "$/cancelRequest" => handle Lean.Lsp.CancelParams Lean.Server.Watchdog.handleCancelRequest | "$/lean/rpc/connect" => handle Lean.Lsp.RpcConnectParams (Lean.Server.Watchdog.forwardNotification method) | "$/lean/rpc/release" => handle Lean.Lsp.RpcReleaseParams (Lean.Server.Watchdog.forwardNotification method) | "$/lean/rpc/keepAlive" => handle Lean.Lsp.RpcKeepAliveParams (Lean.Server.Watchdog.forwardNotification method) | x => if (!String.isPrefixOf "$/" method) = true then do let a ← read liftM (IO.FS.Stream.putStrLn a.hLog (toString "Got unsupported notification: " ++ toString method ++ toString "")) else pure PUnit.unit

source

def Lean.Server.Watchdog.shutdown :

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.shutdown = do let a ← read let fileWorkers ← ST.Ref.get a.fileWorkersRef let r ← forIn fileWorkers PUnit.unit fun x r => match x with | (uri, x) => do Lean.Server.Watchdog.terminateFileWorker uri pure (ForInStep.yield PUnit.unit) let x : PUnit := r let r ← forIn fileWorkers PUnit.unit fun x r => match x with | (x, fw) => do discard (liftM (IO.wait fw.commTask)) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

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

source

def Lean.Server.Watchdog.runClientTask :

Lean.Server.Watchdog.ServerM (Task Lean.Server.Watchdog.ServerEvent)

Equations

Lean.Server.Watchdog.runClientTask = do let st ← read let readMsgAction : IO Lean.Server.Watchdog.ServerEvent := do let msg ← IO.FS.Stream.readLspMessage st.hIn pure (Lean.Server.Watchdog.ServerEvent.clientMsg msg) let a ← liftM (IO.asTask readMsgAction Task.Priority.default) let clientTask : Task Lean.Server.Watchdog.ServerEvent := Task.map (fun x => match x with | Except.ok ev => ev | Except.error e => Lean.Server.Watchdog.ServerEvent.clientError e) a pure clientTask

source

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

Lean.Server.Watchdog.ServerM Unit

source

def Lean.Server.Watchdog.mkLeanServerCapabilities :

Lean.Lsp.ServerCapabilities

Equations

Lean.Server.Watchdog.mkLeanServerCapabilities = { textDocumentSync? := some { openClose := true, change := Lean.Lsp.TextDocumentSyncKind.incremental, willSave := false, willSaveWaitUntil := false, save? := none }, completionProvider? := some { triggerCharacters? := some #["."], allCommitCharacters? := none, resolveProvider := false }, hoverProvider := true, documentHighlightProvider := true, documentSymbolProvider := true, definitionProvider := true, declarationProvider := true, typeDefinitionProvider := true, referencesProvider := true, workspaceSymbolProvider := true, semanticTokensProvider? := some { legend := { tokenTypes := Lean.Lsp.SemanticTokenType.names, tokenModifiers := #[] }, range := true, full := true } }

source

def Lean.Server.Watchdog.initAndRunWatchdogAux :

Lean.Server.Watchdog.ServerM Unit

Equations

Lean.Server.Watchdog.initAndRunWatchdogAux = do let st ← read tryCatch (do discard (liftM (IO.FS.Stream.readLspNotificationAs st.hIn "initialized" Lean.Lsp.InitializedParams)) let clientTask ← Lean.Server.Watchdog.runClientTask Lean.Server.Watchdog.mainLoop clientTask) fun err => do Lean.Server.Watchdog.shutdown throw err let _do_jp : Lean.JsonRpc.Message → Lean.Server.Watchdog.ServerM Unit := fun discr => match discr with | Lean.JsonRpc.Message.notification "exit" none => pure PUnit.unit | x => liftM (IO.throwServerError "Got `shutdown` request, expected an `exit` notification") let y ← tryCatch (liftM (IO.FS.Stream.readLspMessage st.hIn)) fun x => pure (Lean.JsonRpc.Message.notification "exit" none) _do_jp y

source

def Lean.Server.Watchdog.findWorkerPath :

IO System.FilePath

Equations

Lean.Server.Watchdog.findWorkerPath = do let workerPath ← IO.appPath let a ← liftM (IO.getEnv "LEAN_SYSROOT") let _do_jp : System.FilePath → PUnit → IO System.FilePath := fun workerPath y => do let a ← liftM (IO.getEnv "LEAN_WORKER_PATH") let _do_jp : System.FilePath → PUnit → IO System.FilePath := fun workerPath y => pure workerPath match a with | some path => let workerPath := { toString := path }; do let y ← pure PUnit.unit _do_jp workerPath y | x => do let y ← pure PUnit.unit _do_jp workerPath y match a with | some path => let workerPath := System.FilePath.withExtension ({ toString := path } / { toString := "bin" } / { toString := "lean" }) System.FilePath.exeExtension; do let y ← pure PUnit.unit _do_jp workerPath y | x => do let y ← pure PUnit.unit _do_jp workerPath y

source

def Lean.Server.Watchdog.loadReferences :

IO Lean.Server.References

Equations

Lean.Server.Watchdog.loadReferences = do let oleanSearchPath ← ST.Ref.get Lean.searchPathRef let refs : Lean.Server.References := Lean.Server.References.empty let a ← Lean.SearchPath.findAllWithExt oleanSearchPath "ilean" let r ← forIn a refs fun path r => let refs := r; do let r ← tryCatch (do let a ← Lean.Server.Ilean.load path let refs : Lean.Server.References := Lean.Server.References.addIlean refs path a let y ← pure PUnit.unit pure { fst := y, snd := refs }) fun x => do let y ← pure () pure { fst := y, snd := refs } let x : Lean.Server.References := r.snd let refs : Lean.Server.References := x pure r.fst pure (ForInStep.yield refs) let x : Lean.Server.References := r let refs : Lean.Server.References := x pure refs

source

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

IO Unit

Equations

Lean.Server.Watchdog.initAndRunWatchdog args i o e = do let workerPath ← Lean.Server.Watchdog.findWorkerPath let a ← Lean.getBuildDir let srcSearchPath ← Lean.initSrcSearchPath a ∅ let a ← Lean.Server.Watchdog.loadReferences let references ← liftM (IO.mkRef a) let fileWorkersRef ← liftM (IO.mkRef Std.RBMap.empty) let i ← Lean.Server.maybeTee "wdIn.txt" false i let o ← Lean.Server.maybeTee "wdOut.txt" true o let e ← Lean.Server.maybeTee "wdErr.txt" true e let initRequest ← IO.FS.Stream.readLspRequestAs i "initialize" Lean.Lsp.InitializeParams IO.FS.Stream.writeLspResponse o { id := initRequest.id, result := { capabilities := Lean.Server.Watchdog.mkLeanServerCapabilities, serverInfo? := some { name := "Lean 4 Server", version? := some "0.1.1" } } } IO.FS.Stream.writeLspRequest o { id := Lean.JsonRpc.RequestID.str "register_ilean_watcher", method := "client/registerCapability", param := some { registrations := #[{ id := "ilean_watcher", method := "workspace/didChangeWatchedFiles", registerOptions := some (Lean.toJson { watchers := #[{ globPattern := "**/*.ilean", kind := none }] }) }] } } ReaderT.run Lean.Server.Watchdog.initAndRunWatchdogAux { hIn := i, hOut := o, hLog := e, args := args, fileWorkersRef := fileWorkersRef, initParams := initRequest.param, editDelay := Option.getD (Option.bind initRequest.param.initializationOptions? Lean.Lsp.InitializationOptions.editDelay?) 200, workerPath := workerPath, srcSearchPath := srcSearchPath, references := references }

source

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

IO UInt32

Equations

Lean.Server.Watchdog.watchdogMain args = do let i ← liftM IO.getStdin let o ← liftM IO.getStdout let e ← liftM IO.getStderr let r ← tryCatch (do Lean.Server.Watchdog.initAndRunWatchdog args i o e pure 0) fun err => do IO.FS.Stream.putStrLn e (toString "Watchdog error: " ++ toString err ++ toString "") pure 1 pure r