From bb8be70bcbb8f002b681355e804e78ad7a20f65e Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 27 Nov 2023 22:12:37 +0100 Subject: [PATCH] error: Tried to spawn a new thread, but --- client/public/worker.js | 7 +- server/GameServer/FileWorker.lean | 64 +++++++----- server/GameServer/WasmServer.lean | 165 +++++++++++++++++++++++++----- wasm.sh | 1 + 4 files changed, 185 insertions(+), 52 deletions(-) diff --git a/client/public/worker.js b/client/public/worker.js index 201124f..74a1381 100644 --- a/client/public/worker.js +++ b/client/public/worker.js @@ -2,6 +2,7 @@ var stderrBuffer = "" var messageBuffer = [] var initialized = false; +var flushing = false; var headerMode = true; var header=""; @@ -12,11 +13,15 @@ var utf8decoder = new TextDecoder(); function flushMessageBuffer(){ - if (initialized) { + if (initialized && !flushing) { while(messageBuffer.length > 0) { + flushing = true; var msg = messageBuffer.shift(); + console.log(`Send message: ${msg}`); Module.ccall('send_message', 'void', ['string'], [msg]); + console.log(`Message done: ${msg}`); } + flushing = false; } } diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 0cca9c1..321f8e5 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -395,26 +395,9 @@ section Initialization fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString fileMap := default - def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) - (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) : + def mkHeaderTask (m : DocumentMeta) (hOut : FS.Stream) (paths : List System.FilePath) + (env : Environment) (opts : Options) (hasWidgets : Bool) : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do - -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. - let out ← IO.Process.output - { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } - if out.exitCode != 0 then - throwServerError s!"Error while running Lake: {out.stderr}" - - -- Make the paths relative to the current directory - let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim - let currentDir ← IO.currentDir - let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p - - -- Set the search path - Lean.searchPathRef.set paths - - let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0 - -- return (env, paths) - -- use empty header let (headerStx, headerParserState, msgLog) ← Parser.parseHeader {m.mkInputContext with @@ -456,11 +439,32 @@ section Initialization publishDiagnostics m headerSnap.diagnostics.toArray hOut return (headerSnap, srcSearchPath) + def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool) + (levelParams : Game.DidOpenLevelParams) : + IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do + -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`. + let out ← IO.Process.output + { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] } + if out.exitCode != 0 then + throwServerError s!"Error while running Lake: {out.stderr}" + + -- Make the paths relative to the current directory + let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim + let currentDir ← IO.currentDir + let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p + + -- Set the search path + Lean.searchPathRef.set paths + + let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0 + -- return (env, paths) + mkHeaderTask m hOut paths env opts hasWidgets + def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options) (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets) - levelParams initParams + levelParams let cancelTk ← CancelToken.new let ctx := { hIn := i @@ -515,10 +519,8 @@ section MessageHandling end MessageHandling section MainLoop - partial def mainLoop : GameWorkerM Unit := do - let ctx ← read + partial def mainLoop1 (msg : JsonRpc.Message): GameWorkerM Bool := do let mut st ← StateT.lift 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 @@ -541,11 +543,11 @@ section MainLoop match msg with | Message.request id method (some params) => handleRequest id method (toJson params) - mainLoop + return false | Message.notification "exit" none => let doc := st.doc doc.cancelTk.set - return () + return true | Message.notification "$/game/setInventory" params => let p := (← parseParams Game.SetInventoryParams (toJson params)) let s ← get @@ -553,11 +555,19 @@ section MainLoop set {s with levelParams := {s.levelParams with inventory := p.inventory, difficulty := p.difficulty}} - mainLoop + return false | Message.notification method (some params) => handleNotification method (toJson params) - mainLoop + return false | _ => throwServerError "Got invalid JSON-RPC message" + + +partial def mainLoop : GameWorkerM Unit := do + let ctx ← read + let msg ← ctx.hIn.readLspMessage + if not (← mainLoop1 msg) then + mainLoop + end MainLoop def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do diff --git a/server/GameServer/WasmServer.lean b/server/GameServer/WasmServer.lean index b13e9f8..0055128 100644 --- a/server/GameServer/WasmServer.lean +++ b/server/GameServer/WasmServer.lean @@ -1,4 +1,5 @@ import Lean.Server.Watchdog +import GameServer.FileWorker import GameServer.EnvExtensions import GameServer.Game @@ -11,16 +12,26 @@ open Lsp open JsonRpc open System.Uri +open MyServer.FileWorker + +structure WasmFileState := + fileWorkerState : FileWorker.WorkerState + gameWorkerState : GameWorkerState + headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath)) + structure WasmServerState := initParams? : Option InitializeParams gameServerState : GameServerState + fileState : HashMap String WasmFileState := {} + +def wasmSearchPath : SearchPath := ["/lib", "/gamelib"] @[export game_make_state] unsafe def makeState : IO WasmServerState := do let e ← IO.getStderr try Lean.enableInitializersExecution - searchPathRef.set ["/lib", "/gamelib"] + searchPathRef.set wasmSearchPath let env ← importModules #[ { module := `GameServer : Import } ] {} 0 @@ -31,7 +42,7 @@ unsafe def makeState : IO WasmServerState := do inventory := #[] difficulty := 0 } - return ⟨none, state⟩ + return ⟨none, state, {}⟩ catch err => e.putStrLn s!"Import error: {err}" throw err @@ -71,7 +82,7 @@ def initializeServer (id : RequestID) : IO Unit := do } return () -def mkContext (state : WasmServerState) : IO ServerContext := do +def mkServerContext (state : WasmServerState) : IO ServerContext := do let i ← IO.getStdin let o ← IO.getStdout let e ← IO.getStderr @@ -96,14 +107,104 @@ def mkContext (state : WasmServerState) : IO ServerContext := do def runGameServerM (state : WasmServerState) (x : GameServerM α) : IO (α × WasmServerState) := do let (res, gameServerState) ← ReaderT.run (StateT.run x state.gameServerState) - (← mkContext state) + (← mkServerContext state) return (res, {state with gameServerState}) -def readParams (params? : Option Json.Structured) [FromJson α] : IO α := - let j := toJson params? - match fromJson? j with - | Except.ok v => pure v - | Except.error inner => throw $ userError s!"Unexpected param '{j.compress}' \n{inner}" +def mkWorkerContext (state : WasmServerState) (headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))) : + IO FileWorker.WorkerContext := do + let i ← IO.getStdin + let o ← IO.getStdout + let e ← IO.getStderr + let some initParams := state.initParams? + | throwServerError "no yet initialized" + let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false + return { + hIn := i + hOut := o + hLog := e + headerTask := headerTask + initParams := initParams + clientHasWidgets + } + +def runGameWorkerM (state : WasmServerState) (fileState : WasmFileState) (x : GameWorkerM α) : + IO (α × WasmFileState) := do + let s := fileState.fileWorkerState + let ctx ← mkWorkerContext state fileState.headerTask + let ((res, gameWorkerState), s) ← StateRefT'.run (s := s) <| ReaderT.run (r := ctx) <| + StateT.run (s := fileState.gameWorkerState) <| x + let fileState := {fileState with gameWorkerState := gameWorkerState, fileWorkerState := s} + return (res, fileState) + +def parseParams {paramType : Type} [FromJson paramType] (params : Json) : IO paramType := + match fromJson? params with + | Except.ok parsed => pure parsed + | Except.error inner => throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}" + +def requestWorkerUri (method : String) (params : Json) : IO (Option DocumentUri) := do + if method == "$/lean/rpc/connect" then + let ps : Lsp.RpcConnectParams ← parseParams params + pure <| fileSource ps + else match (← routeLspRequest method params) with + | Except.error e => + throwServerError e.message + | Except.ok uri => pure uri + +open FileWorker in +def handleDidOpen (params : DidOpenTextDocumentParams) (state : WasmServerState) : IO WasmServerState := do + let some initParams := state.initParams? + | throwServerError "no yet initialized" + let (_, state) ← runGameServerM state do + let some lvl ← GameServer.getLevelByFileName? initParams + ((System.Uri.fileUriToPath? params.textDocument.uri).getD params.textDocument.uri |>.toString) + | throwServerError s!"Level not found: {params.textDocument.uri} | {initParams.rootUri?}" + + let env ← importModules #[ + { module := lvl.module : Import } + ] {} 0 + + (← getStderr).putStr "Import for level completed" + + let doc := params.textDocument + let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩ + let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false + + let (headerStx, headerTask) ← mkHeaderTask meta (← getStdout) wasmSearchPath env {} clientHasWidgets + let cancelTk ← CancelToken.new + + let levelParams := { + uri := meta.uri + gameDir := state.gameServerState.gameDir + levelModule := lvl.module + tactics := lvl.tactics.tiles + lemmas := lvl.lemmas.tiles + definitions := lvl.definitions.tiles + inventory := state.gameServerState.inventory + difficulty := state.gameServerState.difficulty + statementName := lvl.statementName + : Game.DidOpenLevelParams + } + + let ctx ← mkWorkerContext state headerTask + let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with + | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0) + | Except.error e => throw (e : ElabTaskError)) + let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk } + + + let s : WasmFileState := { + fileWorkerState := { + doc := doc + initHeaderStx := headerStx + pendingRequests := RBMap.empty + rpcSessions := RBMap.empty + } + gameWorkerState := { levelParams } + headerTask + } + let fileState := state.fileState.insert params.textDocument.uri s + return {state with fileState} + return state @[export game_send_message] unsafe def sendMessage (s : String) (state : WasmServerState) : IO WasmServerState := do @@ -111,30 +212,46 @@ unsafe def sendMessage (s : String) (state : WasmServerState) : IO WasmServerSta try let m ← readMessage s match m with - | Message.request id "initialize" params? => - let p : InitializeParams ← readParams params? + | Message.request id "initialize" (some params) => + let p : InitializeParams ← parseParams (toJson params) initializeServer id let p := {p with rootUri? := some (toString state.gameServerState.game)} return {state with initParams? := some p} - | Message.notification "textDocument/didOpen" params? => - let some initParams := state.initParams? - | throwServerError "no yet initialized" - let p : LeanDidOpenTextDocumentParams ← readParams params? - let (_, state) ← runGameServerM state do - let some lvl ← GameServer.getLevelByFileName? initParams - ((System.Uri.fileUriToPath? p.textDocument.uri).getD p.textDocument.uri |>.toString) - | throwServerError s!"Level not found: {p.textDocument.uri} | {initParams.rootUri?}" - e.putStrLn s!"{lvl.module}" - return state | _ => let (isGameEv, state) ← runGameServerM state (Game.handleServerEvent (.clientMsg m)) if isGameEv then return state else match m with - | _ => - e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" - return state + | Message.notification method (some params) => + let handle := (fun α [FromJson α] (handler : α → WasmServerState → IO WasmServerState) + => parseParams (toJson params) >>= (handler · state)) + match method with --TODO + | "textDocument/didOpen" => handle DidOpenTextDocumentParams handleDidOpen + -- | "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange + -- | "textDocument/didClose" => handle DidCloseTextDocumentParams handleDidClose + -- | "workspace/didChangeWatchedFiles" => handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles + -- | "$/cancelRequest" => handle CancelParams handleCancelRequest + -- | "$/lean/rpc/connect" => handle RpcConnectParams (forwardNotification method) + -- | "$/lean/rpc/release" => handle RpcReleaseParams (forwardNotification method) + -- | "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (forwardNotification method) + | _ => return state + | Message.request id method (some params) => + let some uri ← requestWorkerUri method (toJson params) + | throwServerError s!"Could not find Uri for request: {method}" + let some fileState := state.fileState.find? uri + | throwServerError s!"File not open: {uri}" + let (_, fileState) ← runGameWorkerM state fileState do + MyServer.FileWorker.mainLoop1 m + let fileState := state.fileState.insert uri fileState + return {state with fileState} + | Message.responseError _ _ e .. => + throwServerError s!"Unhandled response error: {e}" + | _ => throwServerError "Got invalid JSON-RPC message" + -- match m with + -- | _ => + -- e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" + -- return state catch err => e.putStrLn s!"Server error: {err}" return state diff --git a/wasm.sh b/wasm.sh index fa9a306..927b15d 100755 --- a/wasm.sh +++ b/wasm.sh @@ -27,6 +27,7 @@ LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \ -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \ + -sPTHREAD_POOL_SIZE_STRICT=2 \ --preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \ --preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \ --preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \