game info

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

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

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 := `Init : Import },
-          -- { module := `GameServer : 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 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 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}"

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

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"@/lib/Lean \
-  # --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
-  # --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
+  --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
-  # --preload-file "../server32bit/build/lib"@/gamelib
+  --preload-file "../server32bit/build/lib"@/gamelib