From 382d0474c4ccae6ff113caa630bdabaaea578969 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 13 Oct 2020 18:13:05 +0200 Subject: [PATCH] chore: remove dead code and fix some minor styling details --- src/Lean/Data/Json/FromToJson.lean | 3 + src/Lean/Server/FileWorker.lean | 113 +++++++++--------- src/Lean/Server/Utils.lean | 6 +- src/Lean/Server/Watchdog.lean | 180 +++++++++++++++-------------- 4 files changed, 155 insertions(+), 147 deletions(-) diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index dadce64c4d..fffc0706ba 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -57,6 +57,9 @@ instance : ToJson Structured := ⟨fun s => | Structured.arr a => arr a | Structured.obj o => obj o⟩ +def toStructured? {α : Type} [ToJson α] (v : α) : Option Structured := + fromJson? (toJson v) + def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Option α := (j.getObjVal? k).bind fromJson? diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index d369063394..3628da87df 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -42,13 +42,14 @@ open Lsp open IO open Snapshots -private def sendDiagnosticsCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) (text : FileMap) (log : MessageLog) +private def sendDiagnostics (h : FS.Stream) (uri : DocumentUri) (version : Nat) (text : FileMap) (log : MessageLog) : IO Unit := do diagnostics ← log.msgs.mapM (msgToDiagnostic text); Lsp.writeLspNotification h "textDocument/publishDiagnostics" - { uri := uri, - version? := version, - diagnostics := diagnostics.toArray : PublishDiagnosticsParams } + { uri := uri, + version? := version, + diagnostics := diagnostics.toArray + : PublishDiagnosticsParams } private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit := IO.eprintln $ "`" ++ text.source.extract s.beginPos (s.endPos-1) ++ "`" @@ -59,18 +60,19 @@ inductive TaskError | ioError (e : IO.Error) inductive ElabTask --- TODO(MH): Sebastian said something about wrapping next in Thunk but i did not have time to look into it yet | mk (snap : Snapshot) (next : Task (Except TaskError ElabTask)) : ElabTask namespace ElabTask private def runTask (act : IO (Except TaskError ElabTask)) : IO (Task (Except TaskError ElabTask)) := do t ← asTask act; -pure $ t.map $ fun error => match error with -| Except.ok e => e -| Except.error ioError => Except.error (TaskError.ioError ioError) +pure $ t.map $ fun error => + match error with + | Except.ok e => e + | Except.error ioError => Except.error (TaskError.ioError ioError) -private partial def runCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) : Snapshot → IO (Except TaskError ElabTask) +private partial def runCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) + : Snapshot → IO (Except TaskError ElabTask) | parent => do result ← compileNextCmd contents.source parent; match result with @@ -89,7 +91,7 @@ private partial def runCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) -- the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, -- because we cannot guarantee that no further diagnostics are emitted after clearing -- them. - sendDiagnosticsCore h uri version contents snap.msgLog; + sendDiagnostics h uri version contents snap.msgLog; t ← runTask (runCore snap); pure (Except.ok ⟨snap, t⟩) | Sum.inr msgLog => do @@ -97,14 +99,16 @@ private partial def runCore (h : FS.Stream) (uri : DocumentUri) (version : Nat) if canceled then pure (Except.error TaskError.aborted) else do - sendDiagnosticsCore h uri version contents msgLog; + sendDiagnostics h uri version contents msgLog; pure (Except.error TaskError.eof) -def run (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) (parent : Snapshot) : IO ElabTask := do +def run (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) (parent : Snapshot) + : IO ElabTask := do t ← runTask (runCore h uri version contents parent); pure ⟨parent, t⟩ -partial def branchOffAt (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) : ElabTask → String.Pos → IO ElabTask +partial def branchOffAt (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents : FileMap) + : ElabTask → String.Pos → IO ElabTask | ⟨snap, nextTask⟩, changePos => do finished ← hasFinished nextTask; if finished then @@ -114,25 +118,24 @@ partial def branchOffAt (h : FS.Stream) (uri : DocumentUri) (version : Nat) (con -- (it will never be the header snap because the -- watchdog will never send didChange notifs with -- header changes to the file worker) - if changePos ≤ nextSnap.endPos then do - new ← run h uri version contents snap; - -- we do not need to cancel the old task explicitly since tasks without refs are marked as cancelled by the GC - pure new + if changePos ≤ nextSnap.endPos then + -- we do not need to cancel the old task explicitly since tasks without refs are marked as cancelled + -- by the GC + run h uri version contents snap else do newNext ← branchOffAt next changePos; pure ⟨snap, Task.pure (Except.ok newNext)⟩ - | Except.error e => match e with + | Except.error e => + match e with -- this case should not be possible. only the main task aborts tasks and ensures that aborted tasks -- do not show up in `snapshots` of EditableDocument below. - | TaskError.aborted => throw (userError "reached case that should not be possible during server file worker task branching") - | TaskError.eof => do - new ← run h uri version contents snap; - pure new + | TaskError.aborted => throwServerError + "Internal server error: reached case that should not be possible during server file worker task branching" + | TaskError.eof => run h uri version contents snap | TaskError.ioError ioError => throw ioError - else do - new ← run h uri version contents snap; + else -- we do not need to cancel the old task explicitly since tasks without refs are marked as cancelled by the GC - pure new + run h uri version contents snap end ElabTask @@ -153,12 +156,12 @@ open Elab def compileDocument (h : FS.Stream) (uri : DocumentUri) (version : Nat) (text : FileMap) : IO EditableDocument := do headerSnap ← Snapshots.compileHeader text.source; task ← ElabTask.run h uri version text headerSnap; -let docOut : EditableDocument := ⟨version, text, task⟩; -pure docOut +pure ⟨version, text, task⟩ /-- Given `changePos`, the UTF-8 offset of a change into the pre-change source, and the new document, updates editable doc state. -/ -def updateDocument (h : FS.Stream) (uri : DocumentUri) (doc : EditableDocument) (changePos : String.Pos) (newVersion : Nat) (newText : FileMap) : IO EditableDocument := +def updateDocument (h : FS.Stream) (uri : DocumentUri) (doc : EditableDocument) (changePos : String.Pos) + (newVersion : Nat) (newText : FileMap) : IO EditableDocument := -- The watchdog only restarts the file worker when the syntax tree of the header changes. -- If e.g. a newline is deleted, it will not restart this file worker, but we still -- need to reparse the header so the offsets are correct. @@ -194,44 +197,27 @@ fun st => st.docRef.get def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : ServerM Unit := fun st => st.pendingRequestsRef.modify map -/-- Clears diagnostics for the document version 'version'. -/ --- TODO(WN): how to clear all diagnostics? Sending version 'none' doesn't seem to work -def clearDiagnostics (uri : DocumentUri) (version : Nat) : ServerM Unit := -fun st => -writeLspNotification st.hOut "textDocument/publishDiagnostics" - { uri := uri, - version? := version, - diagnostics := #[] : PublishDiagnosticsParams } - -def sendDiagnostics (uri : DocumentUri) (doc : EditableDocument) (log : MessageLog) - : ServerM Unit := do -fun st => monadLift $ sendDiagnosticsCore st.hOut uri doc.version doc.text log - -def openDocument (h : FS.Stream) (p : DidOpenTextDocumentParams) : IO EditableDocument := do +def openDocument (h : FS.Stream) (p : DidOpenTextDocumentParams) : IO EditableDocument := let doc := p.textDocument; -- NOTE(WN): `toFileMap` marks line beginnings as immediately following -- "\n", which should be enough to handle both LF and CRLF correctly. -- This is because LSP always refers to characters by (line, column), -- so if we get the line number correct it shouldn't matter that there -- is a CR there. -let text := doc.text.toFileMap; -newDoc ← compileDocument h doc.uri doc.version text; -pure newDoc +compileDocument h doc.uri doc.version doc.text.toFileMap def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do let docId := p.textDocument; let changes := p.contentChanges; oldDoc ← getDocument; -some newVersion ← pure docId.version? | throw (userError "expected version number"); -if newVersion <= oldDoc.version then do - throw (userError "got outdated version number") -else if not changes.isEmpty then do +some newVersion ← pure docId.version? | throwServerError "Expected version number"; +if newVersion <= oldDoc.version then throwServerError "Got outdated version number" +else when (not changes.isEmpty) $ do let (newDocText, minStartOff) := foldDocumentChanges changes oldDoc.text; st ← read; newDoc ← monadLift $ updateDocument st.hOut docId.uri oldDoc minStartOff newVersion newDocText; setDocument newDoc -else pure () def handleCancelRequest (p : CancelParams) : ServerM Unit := do updatePendingRequests (fun pendingRequests => pendingRequests.erase p.id) @@ -249,17 +235,18 @@ def handleHover (p : HoverParams) (e : EditableDocument) : IO Unit := pure ⟨ def parseParams (paramType : Type*) [HasFromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with | some parsed => pure parsed -| none => throw (userError "got param with wrong structure") +| none => throwServerError $ "Got param with wrong structure: " ++ params.compress def handleNotification (method : String) (params : Json) : ServerM Unit := do let h := (fun paramType [HasFromJson paramType] (handler : paramType → ServerM Unit) => parseParams paramType params >>= handler); match method with | "textDocument/didChange" => h DidChangeTextDocumentParams handleDidChange -| "$/cancelRequest" => pure () -- TODO when we're async -| _ => throw (userError ("got unsupported notification method: " ++ method)) +| "$/cancelRequest" => pure () -- TODO(MH) +| _ => throwServerError $ "Got unsupported notification method: " ++ method -def queueRequest {α : Type*} (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α) : ServerM Unit := do +def queueRequest {α : Type*} (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α) + : ServerM Unit := do doc ← getDocument; requestTask ← monadLift $ asTask (handler params doc); updatePendingRequests (fun pendingRequests => pendingRequests.insert id requestTask) @@ -271,8 +258,8 @@ let h := (fun paramType [HasFromJson paramType] parseParams paramType params >>= queueRequest id handler); match method with | "textDocument/hover" => h HoverParams handleHover -| _ => throw (userError $ "got unsupported request: " ++ method ++ - "; params: " ++ toString params) +| _ => throwServerError $ "Got unsupported request: " ++ method ++ + "; params: " ++ toString params partial def mainLoop : Unit → ServerM Unit | () => do @@ -300,13 +287,12 @@ partial def mainLoop : Unit → ServerM Unit | Message.notification method (some params) => do handleNotification method (toJson params); mainLoop () - | _ => throw (userError "got invalid JSON-RPC message") + | _ => throwServerError "Got invalid JSON-RPC message" def initAndRunWorker (i o e : FS.Stream) : IO Unit := do i ← maybeTee "fwIn.txt" false i; o ← maybeTee "fwOut.txt" true o; e ← maybeTee "fwErr.txt" true e; - -- TODO(WN): act in accordance with InitializeParams _ ← Lsp.readLspRequestAs i "initialize" InitializeParams; param ← Lsp.readLspNotificationAs i "textDocument/didOpen" DidOpenTextDocumentParams; @@ -314,7 +300,12 @@ _ ← IO.setStderr e; -- TODO(WN): use a stream var in WorkerM instead of global doc ← openDocument o param; docRef ← IO.mkRef doc; pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap); -runReader (mainLoop ()) (⟨i, o, docRef, pendingRequestsRef⟩ : ServerContext) +runReader (mainLoop ()) + { hIn := i, + hOut := o, + docRef := docRef, + pendingRequestsRef := pendingRequestsRef + : ServerContext } namespace Test @@ -325,7 +316,7 @@ FS.withFile fn FS.Mode.read (fun hFile => do Lean.initSearchPath searchPath; catch (Lean.Server.initAndRunWorker (FS.Stream.ofHandle hFile) o e) - (fun err => e.putStrLn $ toString err)) + (fun err => e.putStrLn (toString err))) end Test end Server @@ -338,5 +329,5 @@ e ← IO.getStderr; Lean.initSearchPath; catch (Lean.Server.initAndRunWorker i o e) - (fun err => e.putStrLn $ toString err); + (fun err => e.putStrLn (toString err)); pure 0 diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean index 746adbeb52..5c62855aa2 100644 --- a/src/Lean/Server/Utils.lean +++ b/src/Lean/Server/Utils.lean @@ -2,6 +2,10 @@ import Lean.Data.Position import Lean.Data.Lsp namespace IO + +def throwServerError {α : Type} {m : Type → Type} [MonadIO m] (err : String) : m α := +liftIO $ throw (userError err) + namespace FS namespace Stream @@ -67,7 +71,7 @@ match logDir with | some logDir => do hTee ← FS.Handle.mk (System.mkFilePath [logDir, fName]) FS.Mode.write true; let hTee := FS.Stream.ofHandle hTee; - pure $ if isOut then + pure $ if isOut then hTee.chainLeft h true else h.chainRight hTee true diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 465ec8ed85..c28fbde4c7 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -19,8 +19,8 @@ For general server architecture, see `README.md`. This module implements the wat ## 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 +Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted +workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes to the header and thus restart the corresponding worker, freeing its imports. TODO(WN): @@ -35,8 +35,8 @@ The watchdog process and its file worker processes communicate via LSP. If the n 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/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. If the header was mutated, signal a shutdown to the file worker by closing the I/O channels. Then restart the file worker. Otherwise, forward the `didChange` notification. @@ -44,18 +44,18 @@ are forwarded to the corresponding file worker process, with the exception of th 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. +- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with its server + capabilities. Consequently, the watchdog will not send an `initialized` notification to the worker. +- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full current state of + the file. No additional `didOpen` notifications will be forwarded to the worker process. - `$/cancelRequest` notifications are forwarded to all file workers. - File workers are always terminated with an `exit` notification, without previously receiving a `shutdown` request. Similarly, they never receive a `didClose` notification. ## Watchdog <-> client communication -The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add non-standard -extensions in case they're needed, for example to communicate tactic state. +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. -/ namespace Lean @@ -72,7 +72,10 @@ structure OpenDocument := (text : FileMap) (headerAst : Syntax) -def workerCfg : Process.StdioConfig := ⟨Process.Stdio.piped, Process.Stdio.piped, Process.Stdio.piped⟩ +def workerCfg : Process.StdioConfig := +{ stdin := Process.Stdio.piped, + stdout := Process.Stdio.piped, + stderr := Process.Stdio.piped } -- Events that a forwarding task of a worker signals to the main task inductive WorkerEvent @@ -80,11 +83,13 @@ inductive WorkerEvent | crashed (e : IO.Error) inductive WorkerState --- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker and when reading a request reply. --- In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. Then, in both cases, the --- file worker has its state set to `crashed` and requests that are in-flight are errored. --- Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded to it. --- If the crash was detected while writing a packet, we queue that packet until the next packet for the file worker arrives. +-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker +-- and when reading a request reply. +-- In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. +-- Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. +-- Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded +-- to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file +-- worker arrives. | crashed (queuedMsgs : Array JsonRpc.Message) | running @@ -125,10 +130,11 @@ writeLspMessage fw.stdin msg def writeNotification {α : Type*} [HasToJson α] (fw : FileWorker) (method : String) (param : α) : m Unit := writeLspNotification fw.stdin method param -def writeRequest {α : Type*} [HasToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α) : m Unit := do +def writeRequest {α : Type*} [HasToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α) + : m Unit := do writeLspRequest fw.stdin id method param; liftIO $ fw.pendingRequestsRef.modify $ fun pendingRequests => - pendingRequests.insert id (Message.request id method (fromJson? (toJson param))) + pendingRequests.insert id (Message.request id method (Json.toStructured? param)) def errorPendingRequests (fw : FileWorker) (hOut : FS.Stream) (code : ErrorCode) (msg : String) : m Unit := do pendingRequests ← liftIO $ fw.pendingRequestsRef.modifyGet (fun pendingRequests => (pendingRequests, RBMap.empty)); @@ -153,10 +159,10 @@ fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert uri va def findFileWorker (uri : DocumentUri) : ServerM FileWorker := fun st => do -fileWorkers ← st.fileWorkersRef.get; -match fileWorkers.find? uri with -| some fw => pure fw -| none => throw (userError $ "Got unknown document URI (" ++ uri ++ ")") + fileWorkers ← st.fileWorkersRef.get; + match fileWorkers.find? uri with + | some fw => pure fw + | none => throwServerError $ "Got unknown document URI (" ++ uri ++ ")" def eraseFileWorker (uri : DocumentUri) : ServerM Unit := fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri) @@ -164,7 +170,6 @@ fun st => st.fileWorkersRef.modify (fun fileWorkers => fileWorkers.erase uri) def log (msg : String) : ServerM Unit := fun st => do st.hLog.putStrLn msg; st.hLog.flush --- TODO: this creates a long-running Task, which should be okay with upcoming API changes. partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerEvent | ⟨⟩ => catch (do @@ -173,7 +178,7 @@ partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerE writeLspMessage hOut msg; fwdMsgAux ()) (fun err => do - -- NOTE: if writeLspMessage errors we will block here, but the main task will + -- NOTE: if writeLspMessage from above errors we will block here, but the main task will -- quit eventually anyways if that happens exitCode ← fw.proc.wait; if exitCode = 0 then do @@ -182,35 +187,48 @@ partial def fwdMsgAux (fw : FileWorker) (hOut : FS.Stream) : Unit → IO WorkerE pure WorkerEvent.terminated else do -- worker crashed - fw.errorPendingRequests hOut ErrorCode.internalError "Server process of file crashed, likely due to a stack overflow in user code"; + fw.errorPendingRequests hOut ErrorCode.internalError + "Server process of file crashed, likely due to a stack overflow in user code"; pure (WorkerEvent.crashed err)) /-- A Task which forwards a worker's messages into the output stream until an event which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/ def fwdMsgTask (fw : FileWorker) : ServerM (Task WorkerEvent) := fun st => - (Task.map (fun either => match either with + (Task.map (fun either => + match either with | Except.ok ev => ev - | Except.error e => WorkerEvent.crashed e)) <$> (IO.asTask (fwdMsgAux fw st.hOut ()) Task.Priority.dedicated) + | Except.error e => WorkerEvent.crashed e)) + <$> (IO.asTask (fwdMsgAux fw st.hOut ()) Task.Priority.dedicated) private def parseHeaderAst (input : String) : IO Syntax := do emptyEnv ← mkEmptyEnvironment; -let inputCtx := Parser.mkInputContext input ""; +let inputCtx := Parser.mkInputContext input ""; let (stx, _, _) := Parser.parseHeader emptyEnv inputCtx; pure stx def startFileWorker (uri : DocumentUri) (version : Nat) (text : FileMap) : ServerM Unit := do st ← read; headerAst ← monadLift $ parseHeaderAst text.source; -let doc : OpenDocument := ⟨version, text, headerAst⟩; workerProc ← monadLift $ Process.spawn { workerCfg with cmd := st.workerPath }; pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap); -- the task will never access itself, so this is fine -let commTaskFw : FileWorker := ⟨doc, workerProc, Task.pure WorkerEvent.terminated, WorkerState.running, pendingRequestsRef⟩; +let commTaskFw : FileWorker := + { doc := ⟨version, text, headerAst⟩, + proc := workerProc, + commTask := Task.pure WorkerEvent.terminated, + state := WorkerState.running, + pendingRequestsRef := pendingRequestsRef }; commTask ← fwdMsgTask commTaskFw; -let fw : FileWorker := {commTaskFw with commTask := commTask}; +let fw : FileWorker := { commTaskFw with commTask := commTask }; writeLspRequest fw.stdin (0 : Nat) "initialize" st.initParams; -fw.writeNotification "textDocument/didOpen" (DidOpenTextDocumentParams.mk ⟨uri, "lean", version, text.source⟩); +fw.writeNotification "textDocument/didOpen" + { textDocument := + { uri := uri, + languageId := "lean", + version := version, + text := text.source } + : DidOpenTextDocumentParams }; updateFileWorkers uri fw def terminateFileWorker (uri : DocumentUri) : ServerM Unit := do @@ -227,13 +245,14 @@ eraseFileWorker uri def parseParams (paramType : Type*) [HasFromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with | some parsed => pure parsed -| none => throw (userError "Got param with wrong structure") +| none => throwServerError $ "Got param with wrong structure: " ++ params.compress def handleCrash (uri : DocumentUri) (queuedMsgs : Array JsonRpc.Message) : ServerM Unit := do fw ← findFileWorker uri; -updateFileWorkers uri {fw with state := WorkerState.crashed queuedMsgs} +updateFileWorkers uri { fw with state := WorkerState.crashed queuedMsgs } -def restartCrashedFileWorker (uri : DocumentUri) (fw : FileWorker) (queuedMsgs : Array JsonRpc.Message) : ServerM Unit := do +def restartCrashedFileWorker (uri : DocumentUri) (fw : FileWorker) (queuedMsgs : Array JsonRpc.Message) + : ServerM Unit := do eraseFileWorker uri; startFileWorker uri fw.doc.version fw.doc.text; newFw ← findFileWorker uri; @@ -244,10 +263,8 @@ let tryDischargeQueuedMsgs : Array JsonRpc.Message → JsonRpc.Message → Serve pure crashedMsgs) (fun err => pure (crashedMsgs.push m)); crashedMsgs ← queuedMsgs.foldlM tryDischargeQueuedMsgs #[]; -if ¬ crashedMsgs.isEmpty then do - handleCrash uri crashedMsgs -else - pure () +when (¬ crashedMsgs.isEmpty) (handleCrash uri crashedMsgs) + def handleDidOpen (p : DidOpenTextDocumentParams) : ServerM Unit := let doc := p.textDocument; @@ -263,10 +280,9 @@ let doc := p.textDocument; let changes := p.contentChanges; fw ← findFileWorker doc.uri; let oldDoc := fw.doc; -some newVersion ← pure doc.version? | throw (userError "Expected version number"); -if newVersion <= oldDoc.version then do - throw (userError "Got outdated version number") -else if not changes.isEmpty then do +some newVersion ← pure doc.version? | throwServerError "Expected version number"; +if newVersion <= oldDoc.version then throwServerError "Got outdated version number" +else when (not changes.isEmpty) $ do let (newDocText, _) := foldDocumentChanges changes oldDoc.text; newHeaderAst ← liftIO $ parseHeaderAst newDocText.source; if newHeaderAst != oldDoc.headerAst then do @@ -277,16 +293,14 @@ else if not changes.isEmpty then do startFileWorker doc.uri newVersion newDocText else do let newDoc : OpenDocument := ⟨newVersion, newDocText, oldDoc.headerAst⟩; - let newFw : FileWorker := {fw with doc := newDoc}; + let newFw : FileWorker := { fw with doc := newDoc }; updateFileWorkers doc.uri newFw; - let msg := Message.notification "textDocument/didChange" (fromJson? (toJson p)); + let msg := Message.notification "textDocument/didChange" (Json.toStructured? p); match fw.state with | WorkerState.crashed queuedMsgs => restartCrashedFileWorker doc.uri newFw (queuedMsgs.push msg) | WorkerState.running => - -- looks like it crashed now! catch (fw.writeNotification "textDocument/didChange" p) (fun err => handleCrash doc.uri #[msg]) -else pure () def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit := terminateFileWorker p.textDocument.uri @@ -294,7 +308,8 @@ terminateFileWorker p.textDocument.uri def handleCancelRequest (p : CancelParams) : ServerM Unit := do st ← read; fileWorkers ← st.fileWorkersRef.get; -fileWorkers.forM $ fun uri fw => match fw.state with +fileWorkers.forM $ fun uri fw => + match fw.state with | WorkerState.crashed queuedMsgs => restartCrashedFileWorker uri fw queuedMsgs | WorkerState.running => catch (fw.writeNotification "$/cancelRequest" p) @@ -302,20 +317,19 @@ fileWorkers.forM $ fun uri fw => match fw.state with def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do let h := (fun α [HasFromJson α] [HasToJson α] [HasFileSource α] => do - parsedParams ← parseParams α params; - let uri := fileSource parsedParams; - fw ← findFileWorker uri; - let msg := Message.request id method (fromJson? params); - match fw.state with - | WorkerState.crashed queuedMsgs => restartCrashedFileWorker uri fw (queuedMsgs.push msg) - | WorkerState.running => do - -- if this errors, the file worker crashed - catch (fw.writeRequest id method parsedParams) - (fun err => handleCrash uri #[msg])); + parsedParams ← parseParams α params; + let uri := fileSource parsedParams; + fw ← findFileWorker uri; + let msg := Message.request id method (fromJson? params); + match fw.state with + | WorkerState.crashed queuedMsgs => restartCrashedFileWorker uri fw (queuedMsgs.push msg) + | WorkerState.running => + catch (fw.writeRequest id method parsedParams) + (fun err => handleCrash uri #[msg])); match method with | "textDocument/hover" => h HoverParams -| _ => throw (userError $ "Got unsupported request: " ++ method ++ - "; params: " ++ toString params) +| _ => throwServerError $ "Got unsupported request: " ++ method ++ + "; params: " ++ toString params def handleNotification (method : String) (params : Json) : ServerM Unit := let handle := (fun α [HasFromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler); @@ -324,7 +338,7 @@ match method with | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange | "textDocument/didClose" => handle DidCloseTextDocumentParams handleDidClose | "$/cancelRequest" => handle CancelParams handleCancelRequest -| _ => throw (userError "Got unsupported notification method") +| _ => throwServerError "Got unsupported notification method" def shutdown : ServerM Unit := do st ← read; @@ -340,24 +354,22 @@ inductive ServerEvent def runClientTask : ServerM (Task ServerEvent) := do st ← read; clientTask ← liftIO $ IO.asTask $ ServerEvent.ClientMsg <$> readLspMessage st.hIn; -let clientTask := clientTask.map - (fun either => match either with +let clientTask := clientTask.map $ fun either => + match either with | Except.ok ev => ev - | Except.error e => ServerEvent.ClientError e); + | Except.error e => ServerEvent.ClientError e; pure clientTask partial def mainLoop : Task ServerEvent → ServerM Unit | clientTask => do st ← read; workers ← st.fileWorkersRef.get; - let workerTasks := workers.fold (fun acc uri fw => match fw.state with | WorkerState.running => fw.commTask.map (ServerEvent.WorkerEvent uri fw) :: acc | _ => acc) ([] : List (Task ServerEvent)); - ev ← liftIO $ IO.waitAny $ clientTask :: workerTasks; match ev with | ServerEvent.ClientMsg msg => @@ -373,19 +385,15 @@ partial def mainLoop : Task ServerEvent → ServerM Unit handleNotification method (toJson params); newClientTask ← runClientTask; mainLoop newClientTask - | _ => throw (userError "Got invalid JSON-RPC message") - - | ServerEvent.ClientError e => - shutdown - - /- Restart an exited worker. -/ + | _ => throwServerError "Got invalid JSON-RPC message" + | ServerEvent.ClientError e => throw e | ServerEvent.WorkerEvent uri fw err => match err with | WorkerEvent.crashed e => do handleCrash uri #[]; mainLoop clientTask - -- TODO: this internal error does occur - | WorkerEvent.terminated => throw (userError "Internal server error: got termination event for worker that should have been removed") + | WorkerEvent.terminated => throwServerError + "Internal server error: got termination event for worker that should have been removed" def mkLeanServerCapabilities : ServerCapabilities := { textDocumentSync? := some @@ -404,10 +412,8 @@ catch clientTask ← runClientTask; mainLoop clientTask; Message.notification "exit" none ← readLspMessage st.hIn - | throw (userError "Expected an exit notification"); + | throwServerError "Expected an exit notification"; pure ()) - -- something crashed, try to terminate all the file workers and all the forwarding tasks - -- so that we can die in peace (fun err => do shutdown; throw err) def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do @@ -417,20 +423,24 @@ let workerPath := match workerPath with | none => appDir ++ pathSeparator.toString ++ "FileWorker" ++ exeSuffix | some p => p; fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap); - i ← maybeTee "wdIn.txt" false i; o ← maybeTee "wdOut.txt" true o; e ← maybeTee "wdErr.txt" true e; - initRequest ← readLspRequestAs i "initialize" InitializeParams; writeLspResponse o initRequest.id { capabilities := mkLeanServerCapabilities, - serverInfo? := some { name := "Lean 4 server", - version? := "0.0.1" } : InitializeResult }; - + serverInfo? := some { name := "Lean 4 server", + version? := "0.0.1" } + : InitializeResult }; runReader initAndRunWatchdogAux - (⟨i, o, e, fileWorkersRef, initRequest.param, workerPath⟩ : ServerContext) + { hIn := i, + hOut := o, + hLog := e, + fileWorkersRef := fileWorkersRef, + initParams := initRequest.param, + workerPath := workerPath + : ServerContext } namespace Test @@ -441,7 +451,7 @@ FS.withFile fn FS.Mode.read (fun hFile => do Lean.initSearchPath searchPath; catch (Lean.Server.initAndRunWatchdog (FS.Stream.ofHandle hFile) o e) - (fun err => e.putStrLn $ toString err)) + (fun err => e.putStrLn (toString err))) end Test end Server @@ -456,5 +466,5 @@ e ← IO.getStderr; Lean.initSearchPath; catch (Lean.Server.initAndRunWatchdog i o e) - (fun err => e.putStrLn $ toString err); + (fun err => e.putStrLn (toString err)); pure 0