diff --git a/client/public/worker.js b/client/public/worker.js index 6bcb1f4..822f8a7 100644 --- a/client/public/worker.js +++ b/client/public/worker.js @@ -2,6 +2,7 @@ var stderrBuffer = "" var messageBuffer = [] var initialized = false; +var pointer = null; var headerMode = true; var header=""; @@ -15,7 +16,7 @@ function flushMessageBuffer(){ if (initialized) { while(messageBuffer.length > 0) { var msg = messageBuffer.shift(); - Module.ccall('send_message', 'void', ['string'], [msg]); + Module.ccall('send_message', 'void', ['string', 'pointer'], [msg, pointer]); } } } @@ -57,8 +58,12 @@ var Module = { }], "noInitialRun": true, "onRuntimeInitialized": () => { - Module.ccall('main', 'number', [], []); + pointer = Module.ccall('main', 'pointer', [], []); initialized = true; + if (stderrBuffer !== "") { + console.log(stderrBuffer); + stderrBuffer = "" + } flushMessageBuffer(); } }; diff --git a/server/GameServer.lean b/server/GameServer.lean index 4858662..e329fed 100644 --- a/server/GameServer.lean +++ b/server/GameServer.lean @@ -1,6 +1,12 @@ +import Lean.Server.Watchdog import GameServer.Commands +import GameServer.Game Game "TestGame" Title "Hello Test" MakeGame + +#eval do + let env ← (Lean.getEnv : Lean.MetaM _) + return (gameExt.getState env).size diff --git a/server/GameServer/WasmServer.lean b/server/GameServer/WasmServer.lean index 31d2e25..795c53a 100644 --- a/server/GameServer/WasmServer.lean +++ b/server/GameServer/WasmServer.lean @@ -1,4 +1,5 @@ import Lean.Server.Watchdog +import GameServer.EnvExtensions import GameServer.Game namespace WasmServer.Watchdog @@ -13,21 +14,39 @@ open System.Uri def ServerState := GameServerState @[export game_make_state] -def makeState : IO (Ref ServerState) := do +unsafe def makeState : IO (ServerState) := do let e ← IO.getStderr try + Lean.enableInitializersExecution searchPathRef.set ["/lib", "/gamelib"] + e.putStrLn s!"Importing" let state : GameServerState := { env := ← importModules #[ - { module := `Init : Import } - -- { module := `GameServer : Import } + { module := `Init : Import }, + { module := `GameServer : Import } ] {} 0 --← createEnv gameDir module, game := "TEST", gameDir := "test", inventory := #[] difficulty := 0 } - return ← IO.mkRef state + e.putStrLn s!"Import complete" + let pExtDescrs ← persistentEnvExtensionsRef.get + pExtDescrs.forM fun extDescr => do + e.putStrLn ("extension '" ++ toString extDescr.name ++ "'") + let s := extDescr.toEnvExtension.getState state.env + let fmt := extDescr.statsFn s.state + unless fmt.isNil do IO.println (" " ++ toString (Format.nest 2 (extDescr.statsFn s.state))) + e.putStrLn (" number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0)) + e.putStrLn s!"{(gameExt.getState state.env).size}" + let some game := (gameExt.getState state.env).find? `TestGame + | throwServerError "Game not found" + let gameJson : Json := toJson game + -- Add world sizes to Json object + -- let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) + -- let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) + e.putStrLn s!"{gameJson}" + return state catch err => e.putStrLn s!"Import error: {err}" throw err @@ -67,8 +86,9 @@ def initializeServer (id : RequestID) : IO Unit := do } return () + @[export game_send_message] -def sendMessage (s : String) (state : Ref ServerState) : IO Unit := do +unsafe def sendMessage (s : String) (state : ServerState) : IO Unit := do let o ← IO.getStdout let e ← IO.getStderr try @@ -77,14 +97,16 @@ def sendMessage (s : String) (state : Ref ServerState) : IO Unit := do | Message.request id "initialize" params? => initializeServer id | Message.request id "info" _ => - let some game := (gameExt.getState (← state.get).env).find? `TestGame + + let some game := (gameExt.getState state.env).find? `TestGame | throwServerError "Game not found" let gameJson : Json := toJson game -- Add world sizes to Json object - let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) - let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) + -- let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) + -- let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) + e.putStrLn s!"{gameJson}" o.writeLspResponse ⟨id, gameJson⟩ - | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" + | _ => pure () --throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'" catch err => e.putStrLn s!"Server error: {err}" diff --git a/server/main.c b/server/main.c index 9437804..9f9fedd 100644 --- a/server/main.c +++ b/server/main.c @@ -13,7 +13,8 @@ extern lean_object * initialize_GameServer_WasmServer(uint8_t builtin, lean_obje lean_object * state; lean_object * io_world; -int main() { + +lean_object * main() { lean_initialize(); lean_initialize_runtime_module(); lean_object * res; @@ -26,13 +27,21 @@ int main() { } else { lean_io_result_show_error(res); lean_dec(res); - return 1; // do not access Lean declarations if initialization failed + return 0; // do not access Lean declarations if initialization failed } lean_io_mark_end_initialization(); - state = lean_io_result_get_value(game_make_state(io_world)); + res = game_make_state(io_world); + if (lean_io_result_is_ok(res)) { + state = lean_io_result_get_value(res); + return state; + } else { + lean_io_result_show_error(res); + lean_dec(res); + return 0; // do not access Lean declarations if initialization failed + } } -void send_message(char* msg){ +void send_message(char* msg, lean_object * state){ lean_object * s = lean_mk_string(msg); game_send_message(s, state, io_world); } diff --git a/wasm.sh b/wasm.sh index 4f4aac7..71c7cca 100755 --- a/wasm.sh +++ b/wasm.sh @@ -5,6 +5,7 @@ cp -r server server32bit cd server32bit /home/alex/Projects/lean4/build/test/stage1/bin/lake update -R +/home/alex/Projects/lean4/build/test/stage1/bin/lake clean /home/alex/Projects/lean4/build/test/stage1/bin/lake build cd ../server @@ -21,7 +22,7 @@ emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR build --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 \ - # --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \ - # --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \ - # --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \ - # --preload-file "../server32bit/build/lib"@/gamelib + --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \ + --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \ + --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \ + --preload-file "../server32bit/build/lib"@/gamelib