From 9a86adb17e43470c908633baaef5e9edb27f5a7d Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 17 Nov 2022 16:38:26 +0100 Subject: [PATCH] rudimentary info request --- client/src/App.tsx | 3 + client/src/components/Welcome.tsx | 20 +- server/index.mjs | 17 +- server/leanserver/GameServer/FileWorker.lean | 443 ++++++++++++++++++ server/leanserver/GameServer/Game.lean | 23 + server/leanserver/GameServer/Watchdog.lean | 154 +++++++ server/leanserver/Main.lean | 446 +------------------ 7 files changed, 651 insertions(+), 455 deletions(-) create mode 100644 server/leanserver/GameServer/FileWorker.lean create mode 100644 server/leanserver/GameServer/Game.lean create mode 100644 server/leanserver/GameServer/Watchdog.lean diff --git a/client/src/App.tsx b/client/src/App.tsx index 868c099..b6087ce 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -33,6 +33,9 @@ function App() { let rpcConnection = rpc.createWebSocketConnection(socket, logger) setRpcConnection(rpcConnection); rpcConnection.listen(); + }, + onMessage: (msg) => { + console.log(msg) } }) diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 4c21806..2efa1aa 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -24,7 +24,9 @@ type infoResultType = { conclusion: string } -const infoRequestType = new rpc.RequestType0("info") +const initializeRequestType = new rpc.RequestType0("initialize") +const initializedNotificationType = new rpc.NotificationType0("initialized") +const infoRequestType = new rpc.RequestType1("info") function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { @@ -32,12 +34,16 @@ function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusio useEffect(() => { if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established - rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{ - setLeanData(res) - setNbLevels(res.nb_levels) - setTitle(res.title) - document.title = res.title - setConclusion(res.conclusion) + rpcConnection.sendRequest(initializeRequestType).then((res: any) => { + rpcConnection.onRequest("client/registerCapability", () => {}) + rpcConnection.sendNotification(initializedNotificationType) + rpcConnection.sendRequest(infoRequestType, "hello").then((res: infoResultType) =>{ + setLeanData(res) + setNbLevels(res.nb_levels) + setTitle(res.title) + document.title = res.title + setConclusion(res.conclusion) + }); }); } }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion]) diff --git a/server/index.mjs b/server/index.mjs index 92848eb..7b03739 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -34,16 +34,23 @@ if (isDevelopment) { wss.addListener("connection", function(ws) { const socket = { - onMessage: (cb) => {ws.on("message", cb)}, - onError: (cb) => {ws.on("error", cb)}, - onClose: (cb) => {ws.on("onclose", cb)}, - send: ws.send + onMessage: (cb) => { ws.on("message", cb) }, + onError: (cb) => { ws.on("error", cb) }, + onClose: (cb) => { ws.on("onclose", cb) }, + send: (data, cb) => { ws.send(data,cb) } } const reader = new rpc.WebSocketMessageReader(socket); const writer = new rpc.WebSocketMessageWriter(socket); const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close()) const serverConnection = jsonrpcserver.createServerProcess('Lean Server', cmd, cmdArgs); - jsonrpcserver.forward(socketConnection, serverConnection, message => { + socketConnection.forward(serverConnection, message => { + console.log(`CLIENT: ${JSON.stringify(message)}`) return message; }); + serverConnection.forward(socketConnection, message => { + console.log(`SERVER: ${JSON.stringify(message)}`) + return message; + }); + socketConnection.onClose(() => serverConnection.dispose()); + serverConnection.onClose(() => socketConnection.dispose()); }) diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean new file mode 100644 index 0000000..1ad00e9 --- /dev/null +++ b/server/leanserver/GameServer/FileWorker.lean @@ -0,0 +1,443 @@ +/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/ + +import Lean + +namespace MyModule +open Lean +open Elab +open Parser + +private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message := + let pos := c.fileMap.toPosition pos + { fileName := c.fileName, pos := pos, data := errorMsg } + +open Parser in +private def mkEOI (pos : String.Pos) : Syntax := + let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) "" + mkNode `Lean.Parser.Module.eoi #[atom] + +partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) : Syntax × ModuleParserState × MessageLog := Id.run do + let mut pos := mps.pos + let mut recovering := mps.recovering + let mut messages := messages + let mut stx := Syntax.missing -- will always be assigned below + if inputCtx.input.atEnd pos ∧ couldBeEndSnap then + stx := mkEOI pos + return (stx, { pos, recovering }, messages) + let c := mkParserContext inputCtx pmctx + let s := { cache := initCacheForInput c.input, pos := pos : ParserState } + let s := whitespace c s + let s := (Tactic.sepByIndentSemicolon tacticParser).fn c s + pos := s.pos + match s.errorMsg with + | none => + stx := s.stxStack.back + recovering := false + | some errorMsg => + messages := messages.add <| mkErrorMessage c s.pos (toString errorMsg) + recovering := true + stx := s.stxStack.back + if ¬ c.input.atEnd s.pos then + messages := messages.add <| mkErrorMessage c s.pos "end of input" + return (stx, { pos := c.input.endPos, recovering }, messages) + +end MyModule + +namespace MyServer.FileWorker +open Lean +open Lean.Server +open Lean.Server.FileWorker +open Lsp +open IO +open Snapshots +open JsonRpc + +section Elab + +open Elab Meta Expr in +def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do + let cmdState := snap.cmdState + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let (tacticStx, cmdParserState, msgLog) := + MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap + let cmdPos := tacticStx.getPos?.get! + if Parser.isEOI tacticStx then + let endSnap : Snapshot := { + beginPos := cmdPos + stx := tacticStx + mpState := cmdParserState + cmdState := snap.cmdState + interactiveDiags := ← withNewInteractiveDiags msgLog + tacticCache := snap.tacticCache + } + return endSnap + else + let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog } + /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive + access to the cache, we create a fresh reference here. Before this change, the + following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/ + let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get) + let cmdCtx : Elab.Command.Context := { + cmdPos := snap.endPos + fileName := inputCtx.fileName + fileMap := inputCtx.fileMap + tacticCache? := some tacticCacheNew + } + let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do + Elab.Command.catchExceptions + (getResetInfoTrees *> do + let level := `level1 + let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[] + let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩) + let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*) + let cmdStx ← `(command| example : $(mkIdent level) := by {unfold $(mkIdent level); $(⟨tacticStx⟩)} ) + Elab.Command.elabCommandTopLevel cmdStx) + cmdCtx cmdStateRef + let postNew := (← tacticCacheNew.get).post + snap.tacticCache.modify fun _ => { pre := postNew, post := {} } + let mut postCmdState ← cmdStateRef.get + if !output.isEmpty then + postCmdState := { + postCmdState with + messages := postCmdState.messages.add { + fileName := inputCtx.fileName + severity := MessageSeverity.information + pos := inputCtx.fileMap.toPosition snap.endPos + data := output + } + } + let postCmdSnap : Snapshot := { + beginPos := cmdPos + stx := tacticStx + mpState := cmdParserState + cmdState := postCmdState + interactiveDiags := ← withNewInteractiveDiags postCmdState.messages + tacticCache := (← IO.mkRef {}) + } + return postCmdSnap + +where + /-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent + snapshot. We need to do this because unlike the `MessageLog` itself, interactive diags are not + part of the command state. -/ + withNewInteractiveDiags (msgLog : MessageLog) : IO (PersistentArray Widget.InteractiveDiagnostic) := do + let newMsgCount := msgLog.msgs.size - snap.msgLog.msgs.size + let mut ret := snap.interactiveDiags + for i in List.iota newMsgCount do + let newMsg := msgLog.msgs.get! (msgLog.msgs.size - i) + ret := ret.push (← Widget.msgToInteractiveDiagnostic inputCtx.fileMap newMsg hasWidgets) + return ret + + private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream) + (snaps : Array Snapshot) : IO Unit := do + let trees := snaps.map fun snap => snap.infoTree + let references := findModuleRefs m.text trees (localVars := true) + let param := { version := m.version, references : LeanIleanInfoParams } + hOut.writeLspNotification { method, param } + + private def publishIleanInfoUpdate : DocumentMeta → FS.Stream → Array Snapshot → IO Unit := + publishIleanInfo "$/lean/ileanInfoUpdate" + + private def publishIleanInfoFinal : DocumentMeta → FS.Stream → Array Snapshot → IO Unit := + publishIleanInfo "$/lean/ileanInfoFinal" + + /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/ + private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) + : AsyncElabM (Option Snapshot) := do + cancelTk.check + let s ← get + let lastSnap := s.snaps.back + if lastSnap.isAtEnd then + publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut + publishProgressDone m ctx.hOut + -- This will overwrite existing ilean info for the file, in case something + -- went wrong during the incremental updates. + publishIleanInfoFinal m ctx.hOut s.snaps + return none + publishProgressAtPos m lastSnap.endPos ctx.hOut + -- Make sure that there is at least one snap after the head snap, so that + -- we can see the current goal even on an empty document + let couldBeEndSnap := s.snaps.size > 1 + let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap + set { s with snaps := s.snaps.push snap } + -- TODO(MH): check for interrupt with increased precision + cancelTk.check + /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones + while prefering newer versions over old ones. The former is necessary because we do + not explicitly clear older diagnostics, while the latter is necessary because we do + not guarantee that diagnostics are emitted in order. Specifically, it may happen that + we interrupted this elaboration task right at this point and a newer elaboration task + emits diagnostics, after which we emit old diagnostics because we did not yet detect + the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, + because we cannot guarantee that no further diagnostics are emitted after clearing + them. -/ + -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot + -- because empty diagnostics clear existing error/information squiggles. Therefore we always + -- want to publish in case there was previously a message at this position. + publishDiagnostics m snap.diagnostics.toArray ctx.hOut + publishIleanInfoUpdate m ctx.hOut #[snap] + return some snap + + /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/ + def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) + : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do + let ctx ← read + let headerSnap := snaps[0]! + if headerSnap.msgLog.hasErrors then + -- Treat header processing errors as fatal so users aren't swamped with + -- followup errors + publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError) + publishIleanInfoFinal m ctx.hOut #[headerSnap] + return AsyncList.ofList [headerSnap] + else + -- This will overwrite existing ilean info for the file since this has a + -- higher version number. + publishIleanInfoUpdate m ctx.hOut snaps + return AsyncList.ofList snaps.toList ++ (← AsyncList.unfoldAsync (nextSnap ctx m cancelTk) { snaps }) + +end Elab + +section Updates + + def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do + let ctx ← read + let oldDoc := (←get).doc + -- The watchdog only restarts the file worker when the semantic content 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 that the offsets are correct. + let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext + let cancelTk ← CancelToken.new + -- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths` + let headSnapTask := oldDoc.cmdSnaps.waitHead? + let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do + let headSnap? ← MonadExcept.ofExcept headSnap?? + -- There is always at least one snapshot absent exceptions + let headSnap := headSnap?.get! + let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState } + oldDoc.cancelTk.set + let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source + -- Ignore exceptions, we are only interested in the successful snapshots + let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix + -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only + -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. + let mut validSnaps := cmdSnaps.takeWhile (fun s => s.endPos < changePos) + if validSnaps.length ≤ 1 then + validSnaps := [newHeaderSnap] + else + /- When at least one valid non-header snap exists, it may happen that a change does not fall + within the syntactic range of that last snap but still modifies it by appending tokens. + We check for this here. We do not currently handle crazy grammars in which an appended + token can merge two or more previous commands into one. To do so would require reparsing + the entire file. -/ + let mut lastSnap := validSnaps.getLast! + let preLastSnap := if validSnaps.length ≥ 2 + then validSnaps.get! (validSnaps.length - 2) + else newHeaderSnap + let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap + if newLastStx != lastSnap.stx then + validSnaps := validSnaps.dropLast + unfoldSnaps newMeta validSnaps.toArray cancelTk ctx + modify fun st => { st with doc := ⟨newMeta, AsyncList.delayed newSnaps, cancelTk⟩ } + +end Updates + +section Initialization + + + def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where + input := "" -- No header! + fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString + fileMap := default + + def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) + : IO (Snapshot × SearchPath) := do + let (headerStx, headerParserState, msgLog) ← Parser.parseHeader m.mkInputContext + let mut srcSearchPath ← initSrcSearchPath (← getBuildDir) + searchPathRef.set [(← Lean.findSysroot) / "lib" / "lean", (← getBuildDir) / "lib"] + let lakePath ← match (← IO.getEnv "LAKE") with + | some path => pure <| System.FilePath.mk path + | none => + let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with + | some path => pure <| System.FilePath.mk path / "bin" / "lake" + | _ => pure <| (← appDir) / "lake" + pure <| lakePath.withExtension System.FilePath.exeExtension + let (headerEnv, msgLog) ← try + if let some path := System.Uri.fileUriToPath? m.uri then + -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps + -- NOTE: lake does not exist in stage 0 (yet?) + if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then + let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut + srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath + let env ← importModules [{module := `Init}, {module := `Lib}] opts 0 + pure (env, msgLog) + catch e => -- should be from `lake print-paths` + let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString } + pure (← mkEmptyEnvironment, msgs) + let mut headerEnv := headerEnv + try + if let some path := System.Uri.fileUriToPath? m.uri then + headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none) + catch _ => pure () + let cmdState := Elab.Command.mkState headerEnv msgLog opts + let cmdState := { cmdState with infoState := { + enabled := true + trees := #[Elab.InfoTree.context ({ + env := headerEnv + fileMap := m.text + ngen := { namePrefix := `_worker } + }) (Elab.InfoTree.node + (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx }) + (headerStx[1].getArgs.toList.map (fun importStx => + Elab.InfoTree.node (Elab.Info.ofCommandInfo { + elaborator := `import + stx := importStx + }) #[].toPArray' + )).toPArray' + )].toPArray' + }} + let headerSnap := { + beginPos := 0 + stx := headerStx + mpState := headerParserState + cmdState := cmdState + interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets) + tacticCache := (← IO.mkRef {}) + } + publishDiagnostics m headerSnap.diagnostics.toArray hOut + return (headerSnap, srcSearchPath) + + + def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) + : IO (WorkerContext × WorkerState) := do + let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false + let headerTask ← EIO.asTask $ compileHeader meta o opts (hasWidgets := clientHasWidgets) + let cancelTk ← CancelToken.new + let ctx := + { hIn := i + hOut := o + hLog := e + headerTask + initParams + clientHasWidgets + } + let snaps ← EIO.mapTask (t := headerTask) (match · with + | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk ctx + | Except.error e => throw (e : ElabTaskError)) + let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩ + return (ctx, + { doc := doc + pendingRequests := RBMap.empty + rpcSessions := RBMap.empty + }) + +end Initialization + +section NotificationHandling + + def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do + let docId := p.textDocument + let changes := p.contentChanges + let oldDoc := (←get).doc + let some newVersion ← pure docId.version? + | throwServerError "Expected version number" + if newVersion ≤ oldDoc.meta.version then + -- TODO(WN): This happens on restart sometimes. + IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" + else if ¬ changes.isEmpty then + let newDocText := foldDocumentChanges changes oldDoc.meta.text + updateDocument ⟨docId.uri, newVersion, newDocText⟩ + +end NotificationHandling + +section MessageHandling + + def handleNotification (method : String) (params : Json) : WorkerM Unit := do + let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) => + parseParams paramType params >>= handler + match method with + | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange + | "$/cancelRequest" => handle CancelParams handleCancelRequest + | "$/lean/rpc/release" => handle RpcReleaseParams handleRpcRelease + | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams handleRpcKeepAlive + | _ => throwServerError s!"Got unsupported notification method: {method}" + +end MessageHandling + +section MainLoop + partial def mainLoop : WorkerM Unit := do + let ctx ← read + let mut st ← get + let msg ← ctx.hIn.readLspMessage + let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit)) + : IO PendingRequestMap := do + if (← hasFinished task) then + /- Handler tasks are constructed so that the only possible errors here + are failures of writing a response into the stream. -/ + if let Except.error e := task.get then + throwServerError s!"Failed responding to request {id}: {e}" + pure <| acc.erase id + else pure acc + let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests + st := { st with pendingRequests } + + -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired. + for (id, seshRef) in st.rpcSessions do + let sesh ← seshRef.get + if (← sesh.hasExpired) then + st := { st with rpcSessions := st.rpcSessions.erase id } + + set st + match msg with + | Message.request id method (some params) => + handleRequest id method (toJson params) + mainLoop + | Message.notification "exit" none => + let doc := st.doc + doc.cancelTk.set + return () + | Message.notification method (some params) => + handleNotification method (toJson params) + mainLoop + | _ => throwServerError "Got invalid JSON-RPC message" +end MainLoop + +def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do + let i ← maybeTee "fwIn.txt" false i + let o ← maybeTee "fwOut.txt" true o + let initParams ← i.readLspRequestAs "initialize" InitializeParams + let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams + let doc := param.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 meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩ + let e := e.withPrefix s!"[{param.textDocument.uri}] " + let _ ← IO.setStderr e + try + let (ctx, st) ← initializeWorker meta i o e initParams.param opts + let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) mainLoop + return (0 : UInt32) + catch e => + IO.eprintln e + publishDiagnostics meta #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.error, message := e.toString }] o + return (1 : UInt32) + +def workerMain (opts : Options) : IO UInt32 := do + let i ← IO.getStdin + let o ← IO.getStdout + let e ← IO.getStderr + try + let exitCode ← initAndRunWorker i o e opts + -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't + -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code + o.flush + e.flush + IO.Process.exit exitCode.toUInt8 + catch err => + e.putStrLn s!"worker initialization error: {err}" + return (1 : UInt32) + +end MyServer.FileWorker diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean new file mode 100644 index 0000000..7ec82ce --- /dev/null +++ b/server/leanserver/GameServer/Game.lean @@ -0,0 +1,23 @@ +import Lean + +namespace Game +open Lean +open Server +open Watchdog +open Lsp +open JsonRpc + +partial def handleServerEvent (ev : ServerEvent) : ServerM Bool := do + match ev with + | ServerEvent.clientMsg msg => + match msg with + | Message.request id "info" _ => + (← read).hOut.writeLspResponse { + id := id + result := "Hello" + } + return true + | _ => return false + | _ => return false + +end Game diff --git a/server/leanserver/GameServer/Watchdog.lean b/server/leanserver/GameServer/Watchdog.lean new file mode 100644 index 0000000..8ac4eec --- /dev/null +++ b/server/leanserver/GameServer/Watchdog.lean @@ -0,0 +1,154 @@ +/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/ +import Lean +import GameServer.Game + +namespace MyServer.Watchdog +open Lean +open Server +open Watchdog +open IO +open Lsp +open JsonRpc +open System.Uri + + partial def mainLoop (clientTask : Task ServerEvent) : ServerM Unit := do + let st ← read + let workers ← st.fileWorkersRef.get + let mut workerTasks := #[] + for (_, fw) in workers do + if let WorkerState.running := fw.state then + workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw) + if let some ge ← fw.groupedEditsRef.get then + workerTasks := workerTasks.push <| ge.signalTask.map (ServerEvent.workerEvent fw) + + let ev ← IO.waitAny (clientTask :: workerTasks.toList) + + if ← Game.handleServerEvent ev then + mainLoop (←runClientTask) + else + match ev with + | ServerEvent.clientMsg msg => + match msg with + | Message.request id "shutdown" _ => + shutdown + st.hOut.writeLspResponse ⟨id, Json.null⟩ + | Message.request id method (some params) => + handleRequest id method (toJson params) + mainLoop (←runClientTask) + | Message.notification "textDocument/didChange" (some params) => + let p ← parseParams DidChangeTextDocumentParams (toJson params) + let fw ← findFileWorker! p.textDocument.uri + let now ← monoMsNow + /- We wait `editDelay`ms since last edit before applying the changes. -/ + let applyTime := now + st.editDelay + let queuedMsgs? ← fw.groupedEditsRef.modifyGet fun + | some ge => (some ge.queuedMsgs, some { ge with + applyTime := applyTime + params.textDocument := p.textDocument + params.contentChanges := ge.params.contentChanges ++ p.contentChanges + -- drain now-outdated messages and respond with `contentModified` below + queuedMsgs := #[] }) + | none => (none, some { + applyTime := applyTime + params := p + /- This is overwritten just below. -/ + signalTask := Task.pure WorkerEvent.processGroupedEdits + queuedMsgs := #[] }) + match queuedMsgs? with + | some queuedMsgs => + for msg in queuedMsgs do + match msg with + | JsonRpc.Message.request id _ _ => + fw.erasePendingRequest id + (← read).hOut.writeLspResponseError { + id := id + code := ErrorCode.contentModified + message := "File changed." + } + | _ => pure () -- notifications do not need to be cancelled + | _ => + let t ← fw.runEditsSignalTask + fw.groupedEditsRef.modify (Option.map fun ge => { ge with signalTask := t } ) + mainLoop (←runClientTask) + | Message.notification method (some params) => + handleNotification method (toJson params) + mainLoop (←runClientTask) + | Message.response "register_ilean_watcher" _ => + mainLoop (←runClientTask) + | _ => throwServerError "Got invalid JSON-RPC message" + | ServerEvent.clientError e => throw e + | ServerEvent.workerEvent fw ev => + match ev with + | WorkerEvent.processGroupedEdits => + handleEdits fw + mainLoop clientTask + | WorkerEvent.ioError e => + throwServerError s!"IO error while processing events for {fw.doc.meta.uri}: {e}" + | WorkerEvent.crashed _ => + handleCrash fw.doc.meta.uri #[] + mainLoop clientTask + | WorkerEvent.terminated => + throwServerError "Internal server error: got termination event for worker that should have been removed" + +def initAndRunWatchdogAux : ServerM Unit := do + let st ← read + try + discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams + let clientTask ← runClientTask + mainLoop clientTask + catch err => + shutdown + throw err + /- NOTE(WN): It looks like instead of sending the `exit` notification, + VSCode just closes the stream. In that case, pretend we got an `exit`. -/ + let Message.notification "exit" none ← + try st.hIn.readLspMessage + catch _ => pure (Message.notification "exit" none) + | throwServerError "Got `shutdown` request, expected an `exit` notification" + +def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do + let workerPath ← findWorkerPath + let srcSearchPath ← initSrcSearchPath (← getBuildDir) + let references ← IO.mkRef (← loadReferences) + let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) + let i ← maybeTee "wdIn.txt" false i + let o ← maybeTee "wdOut.txt" true o + let e ← maybeTee "wdErr.txt" true e + let initRequest ← i.readLspRequestAs "initialize" InitializeParams + o.writeLspResponse { + id := initRequest.id + result := { + capabilities := mkLeanServerCapabilities + serverInfo? := some { + name := "Lean 4 Game Server" + version? := "0.1.1" + } + : InitializeResult + } + } + ReaderT.run initAndRunWatchdogAux { + hIn := i + hOut := o + hLog := e + args := args + fileWorkersRef := fileWorkersRef + initParams := initRequest.param + editDelay := initRequest.param.initializationOptions? |>.bind InitializationOptions.editDelay? |>.getD 200 + workerPath + srcSearchPath + references + : ServerContext + } + +def watchdogMain (args : List String) : IO UInt32 := do + let i ← IO.getStdin + let o ← IO.getStdout + let e ← IO.getStderr + try + initAndRunWatchdog args i o e + return 0 + catch err => + e.putStrLn s!"Watchdog error: {err}" + return 1 + +end MyServer.Watchdog diff --git a/server/leanserver/Main.lean b/server/leanserver/Main.lean index 17ad1ab..38b1258 100644 --- a/server/leanserver/Main.lean +++ b/server/leanserver/Main.lean @@ -1,451 +1,11 @@ -import GameServer.Server -import Lean +import GameServer.Watchdog +import GameServer.FileWorker -namespace MyModule -open Lean -open Elab -open Parser - -private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message := - let pos := c.fileMap.toPosition pos - { fileName := c.fileName, pos := pos, data := errorMsg } - -open Parser in -private def mkEOI (pos : String.Pos) : Syntax := - let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) "" - mkNode `Lean.Parser.Module.eoi #[atom] - -partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) : Syntax × ModuleParserState × MessageLog := Id.run do - let mut pos := mps.pos - let mut recovering := mps.recovering - let mut messages := messages - let mut stx := Syntax.missing -- will always be assigned below - if inputCtx.input.atEnd pos ∧ couldBeEndSnap then - stx := mkEOI pos - return (stx, { pos, recovering }, messages) - let c := mkParserContext inputCtx pmctx - let s := { cache := initCacheForInput c.input, pos := pos : ParserState } - let s := whitespace c s - let s := (Tactic.sepByIndentSemicolon tacticParser).fn c s - pos := s.pos - match s.errorMsg with - | none => - stx := s.stxStack.back - recovering := false - | some errorMsg => - messages := messages.add <| mkErrorMessage c s.pos (toString errorMsg) - recovering := true - stx := s.stxStack.back - if ¬ c.input.atEnd s.pos then - messages := messages.add <| mkErrorMessage c s.pos "end of input" - return (stx, { pos := c.input.endPos, recovering }, messages) - -end MyModule - -namespace MyServer.FileWorker -open Lean -open Lean.Server -open Lean.Server.FileWorker -open Lsp -open IO -open Snapshots -open JsonRpc - -section Elab - -open Elab Meta Expr in -def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do - let cmdState := snap.cmdState - let scope := cmdState.scopes.head! - let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } - let (tacticStx, cmdParserState, msgLog) := - MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap - let cmdPos := tacticStx.getPos?.get! - if Parser.isEOI tacticStx then - let endSnap : Snapshot := { - beginPos := cmdPos - stx := tacticStx - mpState := cmdParserState - cmdState := snap.cmdState - interactiveDiags := ← withNewInteractiveDiags msgLog - tacticCache := snap.tacticCache - } - return endSnap - else - let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog } - /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive - access to the cache, we create a fresh reference here. Before this change, the - following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/ - let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get) - let cmdCtx : Elab.Command.Context := { - cmdPos := snap.endPos - fileName := inputCtx.fileName - fileMap := inputCtx.fileMap - tacticCache? := some tacticCacheNew - } - let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get scope.opts) <| liftM (m := BaseIO) do - Elab.Command.catchExceptions - (getResetInfoTrees *> do - let level := `level1 - let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[] - let tacticStx := (tacticStx.getArgs.push done).map (⟨.⟩) - let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*) - let cmdStx ← `(command| example : $(mkIdent level) := by {unfold $(mkIdent level); $(⟨tacticStx⟩)} ) - Elab.Command.elabCommandTopLevel cmdStx) - cmdCtx cmdStateRef - let postNew := (← tacticCacheNew.get).post - snap.tacticCache.modify fun _ => { pre := postNew, post := {} } - let mut postCmdState ← cmdStateRef.get - if !output.isEmpty then - postCmdState := { - postCmdState with - messages := postCmdState.messages.add { - fileName := inputCtx.fileName - severity := MessageSeverity.information - pos := inputCtx.fileMap.toPosition snap.endPos - data := output - } - } - let postCmdSnap : Snapshot := { - beginPos := cmdPos - stx := tacticStx - mpState := cmdParserState - cmdState := postCmdState - interactiveDiags := ← withNewInteractiveDiags postCmdState.messages - tacticCache := (← IO.mkRef {}) - } - return postCmdSnap - -where - /-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent - snapshot. We need to do this because unlike the `MessageLog` itself, interactive diags are not - part of the command state. -/ - withNewInteractiveDiags (msgLog : MessageLog) : IO (PersistentArray Widget.InteractiveDiagnostic) := do - let newMsgCount := msgLog.msgs.size - snap.msgLog.msgs.size - let mut ret := snap.interactiveDiags - for i in List.iota newMsgCount do - let newMsg := msgLog.msgs.get! (msgLog.msgs.size - i) - ret := ret.push (← Widget.msgToInteractiveDiagnostic inputCtx.fileMap newMsg hasWidgets) - return ret - - private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream) - (snaps : Array Snapshot) : IO Unit := do - let trees := snaps.map fun snap => snap.infoTree - let references := findModuleRefs m.text trees (localVars := true) - let param := { version := m.version, references : LeanIleanInfoParams } - hOut.writeLspNotification { method, param } - - private def publishIleanInfoUpdate : DocumentMeta → FS.Stream → Array Snapshot → IO Unit := - publishIleanInfo "$/lean/ileanInfoUpdate" - - private def publishIleanInfoFinal : DocumentMeta → FS.Stream → Array Snapshot → IO Unit := - publishIleanInfo "$/lean/ileanInfoFinal" - - /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/ - private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) - : AsyncElabM (Option Snapshot) := do - cancelTk.check - let s ← get - let lastSnap := s.snaps.back - if lastSnap.isAtEnd then - publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut - publishProgressDone m ctx.hOut - -- This will overwrite existing ilean info for the file, in case something - -- went wrong during the incremental updates. - publishIleanInfoFinal m ctx.hOut s.snaps - return none - publishProgressAtPos m lastSnap.endPos ctx.hOut - -- Make sure that there is at least one snap after the head snap, so that - -- we can see the current goal even on an empty document - let couldBeEndSnap := s.snaps.size > 1 - let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap - set { s with snaps := s.snaps.push snap } - -- TODO(MH): check for interrupt with increased precision - cancelTk.check - /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones - while prefering newer versions over old ones. The former is necessary because we do - not explicitly clear older diagnostics, while the latter is necessary because we do - not guarantee that diagnostics are emitted in order. Specifically, it may happen that - we interrupted this elaboration task right at this point and a newer elaboration task - emits diagnostics, after which we emit old diagnostics because we did not yet detect - the interrupt. Explicitly clearing diagnostics is difficult for a similar reason, - because we cannot guarantee that no further diagnostics are emitted after clearing - them. -/ - -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot - -- because empty diagnostics clear existing error/information squiggles. Therefore we always - -- want to publish in case there was previously a message at this position. - publishDiagnostics m snap.diagnostics.toArray ctx.hOut - publishIleanInfoUpdate m ctx.hOut #[snap] - return some snap - - /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/ - def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) - : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do - let ctx ← read - let headerSnap := snaps[0]! - if headerSnap.msgLog.hasErrors then - -- Treat header processing errors as fatal so users aren't swamped with - -- followup errors - publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError) - publishIleanInfoFinal m ctx.hOut #[headerSnap] - return AsyncList.ofList [headerSnap] - else - -- This will overwrite existing ilean info for the file since this has a - -- higher version number. - publishIleanInfoUpdate m ctx.hOut snaps - return AsyncList.ofList snaps.toList ++ (← AsyncList.unfoldAsync (nextSnap ctx m cancelTk) { snaps }) - -end Elab - -section Updates - - def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do - let ctx ← read - let oldDoc := (←get).doc - -- The watchdog only restarts the file worker when the semantic content 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 that the offsets are correct. - let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext - let cancelTk ← CancelToken.new - -- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths` - let headSnapTask := oldDoc.cmdSnaps.waitHead? - let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do - let headSnap? ← MonadExcept.ofExcept headSnap?? - -- There is always at least one snapshot absent exceptions - let headSnap := headSnap?.get! - let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState } - oldDoc.cancelTk.set - let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source - -- Ignore exceptions, we are only interested in the successful snapshots - let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix - -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only - -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. - let mut validSnaps := cmdSnaps.takeWhile (fun s => s.endPos < changePos) - if validSnaps.length ≤ 1 then - validSnaps := [newHeaderSnap] - else - /- When at least one valid non-header snap exists, it may happen that a change does not fall - within the syntactic range of that last snap but still modifies it by appending tokens. - We check for this here. We do not currently handle crazy grammars in which an appended - token can merge two or more previous commands into one. To do so would require reparsing - the entire file. -/ - let mut lastSnap := validSnaps.getLast! - let preLastSnap := if validSnaps.length ≥ 2 - then validSnaps.get! (validSnaps.length - 2) - else newHeaderSnap - let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap - if newLastStx != lastSnap.stx then - validSnaps := validSnaps.dropLast - unfoldSnaps newMeta validSnaps.toArray cancelTk ctx - modify fun st => { st with doc := ⟨newMeta, AsyncList.delayed newSnaps, cancelTk⟩ } - -end Updates - -section Initialization - - - def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where - input := "" -- No header! - fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString - fileMap := default - - def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) - : IO (Snapshot × SearchPath) := do - let (headerStx, headerParserState, msgLog) ← Parser.parseHeader m.mkInputContext - let mut srcSearchPath ← initSrcSearchPath (← getBuildDir) - searchPathRef.set [(← Lean.findSysroot) / "lib" / "lean", (← getBuildDir) / "lib"] - let lakePath ← match (← IO.getEnv "LAKE") with - | some path => pure <| System.FilePath.mk path - | none => - let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with - | some path => pure <| System.FilePath.mk path / "bin" / "lake" - | _ => pure <| (← appDir) / "lake" - pure <| lakePath.withExtension System.FilePath.exeExtension - let (headerEnv, msgLog) ← try - if let some path := System.Uri.fileUriToPath? m.uri then - -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps - -- NOTE: lake does not exist in stage 0 (yet?) - if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then - let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut - srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath - let env ← importModules [{module := `Init}, {module := `Lib}] opts 0 - pure (env, msgLog) - catch e => -- should be from `lake print-paths` - let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString } - pure (← mkEmptyEnvironment, msgs) - let mut headerEnv := headerEnv - try - if let some path := System.Uri.fileUriToPath? m.uri then - headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none) - catch _ => pure () - let cmdState := Elab.Command.mkState headerEnv msgLog opts - let cmdState := { cmdState with infoState := { - enabled := true - trees := #[Elab.InfoTree.context ({ - env := headerEnv - fileMap := m.text - ngen := { namePrefix := `_worker } - }) (Elab.InfoTree.node - (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx }) - (headerStx[1].getArgs.toList.map (fun importStx => - Elab.InfoTree.node (Elab.Info.ofCommandInfo { - elaborator := `import - stx := importStx - }) #[].toPArray' - )).toPArray' - )].toPArray' - }} - let headerSnap := { - beginPos := 0 - stx := headerStx - mpState := headerParserState - cmdState := cmdState - interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets) - tacticCache := (← IO.mkRef {}) - } - publishDiagnostics m headerSnap.diagnostics.toArray hOut - return (headerSnap, srcSearchPath) - - - def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) - : IO (WorkerContext × WorkerState) := do - let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false - let headerTask ← EIO.asTask $ compileHeader meta o opts (hasWidgets := clientHasWidgets) - let cancelTk ← CancelToken.new - let ctx := - { hIn := i - hOut := o - hLog := e - headerTask - initParams - clientHasWidgets - } - let snaps ← EIO.mapTask (t := headerTask) (match · with - | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk ctx - | Except.error e => throw (e : ElabTaskError)) - let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩ - return (ctx, - { doc := doc - pendingRequests := RBMap.empty - rpcSessions := RBMap.empty - }) - -end Initialization - -section NotificationHandling - - def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do - let docId := p.textDocument - let changes := p.contentChanges - let oldDoc := (←get).doc - let some newVersion ← pure docId.version? - | throwServerError "Expected version number" - if newVersion ≤ oldDoc.meta.version then - -- TODO(WN): This happens on restart sometimes. - IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}" - else if ¬ changes.isEmpty then - let newDocText := foldDocumentChanges changes oldDoc.meta.text - updateDocument ⟨docId.uri, newVersion, newDocText⟩ - -end NotificationHandling - -section MessageHandling - - def handleNotification (method : String) (params : Json) : WorkerM Unit := do - let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) => - parseParams paramType params >>= handler - match method with - | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange - | "$/cancelRequest" => handle CancelParams handleCancelRequest - | "$/lean/rpc/release" => handle RpcReleaseParams handleRpcRelease - | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams handleRpcKeepAlive - | _ => throwServerError s!"Got unsupported notification method: {method}" - -end MessageHandling - -section MainLoop - partial def mainLoop : WorkerM Unit := do - let ctx ← read - let mut st ← get - let msg ← ctx.hIn.readLspMessage - let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit)) - : IO PendingRequestMap := do - if (← hasFinished task) then - /- Handler tasks are constructed so that the only possible errors here - are failures of writing a response into the stream. -/ - if let Except.error e := task.get then - throwServerError s!"Failed responding to request {id}: {e}" - pure <| acc.erase id - else pure acc - let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests - st := { st with pendingRequests } - - -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired. - for (id, seshRef) in st.rpcSessions do - let sesh ← seshRef.get - if (← sesh.hasExpired) then - st := { st with rpcSessions := st.rpcSessions.erase id } - - set st - match msg with - | Message.request id method (some params) => - handleRequest id method (toJson params) - mainLoop - | Message.notification "exit" none => - let doc := st.doc - doc.cancelTk.set - return () - | Message.notification method (some params) => - handleNotification method (toJson params) - mainLoop - | _ => throwServerError "Got invalid JSON-RPC message" -end MainLoop - -def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do - let i ← maybeTee "fwIn.txt" false i - let o ← maybeTee "fwOut.txt" true o - let initParams ← i.readLspRequestAs "initialize" InitializeParams - let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams - let doc := param.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 meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩ - let e := e.withPrefix s!"[{param.textDocument.uri}] " - let _ ← IO.setStderr e - try - let (ctx, st) ← initializeWorker meta i o e initParams.param opts - let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) mainLoop - return (0 : UInt32) - catch e => - IO.eprintln e - publishDiagnostics meta #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.error, message := e.toString }] o - return (1 : UInt32) - -def workerMain (opts : Options) : IO UInt32 := do - let i ← IO.getStdin - let o ← IO.getStdout - let e ← IO.getStderr - try - let exitCode ← initAndRunWorker i o e opts - -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't - -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code - o.flush - e.flush - IO.Process.exit exitCode.toUInt8 - catch err => - e.putStrLn s!"worker initialization error: {err}" - return (1 : UInt32) - -end MyServer.FileWorker - def main : List String → IO UInt32 := fun args => do let e ← IO.getStderr if args[0]? == some "--server" then - Lean.Server.Watchdog.watchdogMain [] + MyServer.Watchdog.watchdogMain [] else if args[0]? == some "--worker" then MyServer.FileWorker.workerMain {} else