error: Tried to spawn a new thread, but

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

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)
+  def mkHeaderTask (m : DocumentMeta) (hOut : FS.Stream) (paths : List System.FilePath)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
+      (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
+  partial def mainLoop1 (msg : JsonRpc.Message): GameWorkerM Bool := do
-    let ctx ← read
     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

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 α :=
+def mkWorkerContext (state : WasmServerState) (headerTask : Task (Except Error (Snapshots.Snapshot × SearchPath))) :
-  let j := toJson params?
+    IO FileWorker.WorkerContext := do
-  match fromJson? j with
+  let i ← IO.getStdin
-  | Except.ok v => pure v
+  let o ← IO.getStdout
-  | Except.error inner => throw $ userError s!"Unexpected param '{j.compress}' \n{inner}"
+  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? =>
+    | Message.request id "initialize" (some params) =>
-      let p : InitializeParams ← readParams 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
-        | _ =>
+        | Message.notification method (some params) =>
-          e.putStrLn s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
+            let handle := (fun α [FromJson α] (handler : α → WasmServerState → IO WasmServerState)
-          return state
+              => 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

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 \