game module import (not quite)

.gitignore

@@ -2,5 +2,6 @@ node_modules
 client/dist
 server/build
 server/lakefile.olean
+server32bit
 **/lake-packages/
 **/.DS_Store

client/public/worker.js

@@ -75,7 +75,7 @@ onmessage = (ev) => {
 
 setInterval(() => {
   if (stderrBuffer !== "") {
-    console.error(stderrBuffer);
+    console.log(stderrBuffer);
     stderrBuffer = ""
   }
 }, 1000)

server/GameServer.lean

@@ -0,0 +1,6 @@
+import GameServer.Commands
+
+Game "TestGame"
+Title "Hello Test"
+
+MakeGame

server/GameServer/WasmServer.lean

@@ -10,15 +10,38 @@ open Lsp
 open JsonRpc
 open System.Uri
 
-def counter := IO.mkRef 0
+def ServerState := GameServerState
 
+@[export game_make_state]
+def makeState : IO (Ref ServerState) := do
+  let e ← IO.getStderr
+  try
+    searchPathRef.set ["/lib", "/gamelib"]
+    let state : GameServerState := {
+      env := ← importModules #[
+          { module := `Init : Import }
+          -- { module := `GameServer : Import }
+        ] {} 0 --← createEnv gameDir module,
+      game := "TEST",
+      gameDir := "test",
+      inventory := #[]
+      difficulty := 0
+    }
+    return ← IO.mkRef state
+  catch err =>
+    e.putStrLn s!"Import error: {err}"
+    throw err
 
-def readLspRequestAs (s : String) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
+def readMessage (s : String) : IO JsonRpc.Message := do
   let j ← ofExcept (Json.parse s)
   let m  ← match fromJson? j with
   | Except.ok (m : JsonRpc.Message) => pure m
   | Except.error inner => throw $ userError s!"JSON '{j.compress}' did not have the format of a JSON-RPC message.\n{inner}"
-  let initRequest ← match m with
+  return m
+
+def readLspRequestAs (s : String) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do
+  let m ← readMessage s
+  match m with
   | Message.request id method params? =>
     if method = expectedMethod then
       let j := toJson params?
@@ -29,39 +52,10 @@ def readLspRequestAs (s : String) (expectedMethod : String) (α : Type) [FromJso
       throw $ userError s!"Expected method '{expectedMethod}', got method '{method}'"
   | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
 
-
+def initializeServer (id : RequestID) : IO Unit := do
-@[export game_send_message]
-def sendMessage (s : String) : IO Unit := do
-  -- IO.println s!"received {s}"
-  -- if args.length < 2 then
-  --   throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
-  --     game directory, the name of the main module (optional), and the name of the game (optional)."
-  -- let gameDir := args[1]!
-  -- let module := if args.length < 3 then defaultGameModule else args[2]!
-  -- let gameName := if args.length < 4 then defaultGameName else args[3]!
-  -- let workerPath := "./gameserver"
-  -- -- TODO: Do the following commands slow us down?
-  -- 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 state : GameServerState := {
-  --   env := ← importModules #[] {} 0 --← createEnv gameDir module,
-  --   game := "TEST",
-  --   gameDir := "test",
-  --   inventory := #[]
-  --   difficulty := 0
-  --   }
-  let initRequest ← readLspRequestAs s "initialize" InitializeParams
-
-  -- We misuse the `rootUri` field to the gameName
-  let rootUri? := "TEST"
-  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
   let o ← IO.getStdout
   o.writeLspResponse {
-    id     := initRequest.id
+    id     := id
     result := {
       capabilities := mkLeanServerCapabilities
       serverInfo?  := some {
@@ -71,17 +65,27 @@ def sendMessage (s : String) : IO Unit := do
       : InitializeResult
     }
   }
-  -- let context : ServerContext := {
+  return ()
-  --   hIn            := i
+
-  --   hOut           := o
+@[export game_send_message]
-  --   hLog           := e
+def sendMessage (s : String) (state : Ref ServerState) : IO Unit := do
-  --   args           := args
+  let o ← IO.getStdout
-  --   fileWorkersRef := fileWorkersRef
+  let e ← IO.getStderr
-  --   initParams     := initRequest.param
+  try
-  --   workerPath
+    let m ← readMessage s
-  --   srcSearchPath
+    match m with
-  --   references
+    | Message.request id "initialize" params? =>
-  -- }
+      initializeServer id
-  -- discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
+    | Message.request id "info" _ =>
+      let some game := (gameExt.getState (← state.get).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)])
+      o.writeLspResponse ⟨id, gameJson⟩
+    | _ => throw $ userError s!"Expected JSON-RPC request, got: '{(toJson m).compress}'"
 
+  catch err =>
+    e.putStrLn s!"Server error: {err}"
     return ()

server/lakefile.lean

@@ -3,6 +3,7 @@ open Lake DSL
 
 package GameServer
 
+@[default_target]
 lean_lib GameServer
 
 @[default_target]

server/main.c

@@ -1,7 +1,8 @@
 #include <stdio.h>
 #include <lean/lean.h>
 
-extern lean_object* game_send_message(lean_object*, lean_object*);
+extern lean_object* game_send_message(lean_object*, lean_object*, lean_object*);
+extern lean_object* game_make_state(lean_object*);
 
 // see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization
 extern void lean_initialize_runtime_module();
@@ -9,13 +10,16 @@ extern void lean_initialize();
 extern void lean_io_mark_end_initialization();
 extern lean_object * initialize_GameServer_WasmServer(uint8_t builtin, lean_object *);
 
+lean_object * state;
+lean_object * io_world;
+
 int main() {
   lean_initialize();
   lean_initialize_runtime_module();
   lean_object * res;
   // use same default as for Lean executables
   uint8_t builtin = 1;
-  lean_object * io_world = lean_io_mk_world();
+  io_world = lean_io_mk_world();
   res = initialize_GameServer_WasmServer(builtin, io_world);
   if (lean_io_result_is_ok(res)) {
       lean_dec_ref(res);
@@ -25,9 +29,10 @@ int main() {
       return 1;  // do not access Lean declarations if initialization failed
   }
   lean_io_mark_end_initialization();
+  state = lean_io_result_get_value(game_make_state(io_world));
 }
 
 void send_message(char* msg){
   lean_object * s = lean_mk_string(msg);
-  game_send_message(s, lean_io_mk_world());
+  game_send_message(s, state, io_world);
 }

wasm.sh

@@ -1,7 +1,13 @@
 #!/bin/bash
 
+rm -rf server32bit
+cp -r server server32bit
 
-cd server
+cd server32bit
+/home/alex/Projects/lean4/build/test/stage1/bin/lake update -R
+/home/alex/Projects/lean4/build/test/stage1/bin/lake build
+
+cd ../server
 
 lake build
 
@@ -11,4 +17,11 @@ LEAN_SYSROOT=/home/alex/Projects/lean4/build/release/stage1
 LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
 
 emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR 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
+  -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 \
+  --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