merge dirs

leanprover-community · Nov 15, 2023 · 3ff46ae · 3ff46ae
1 parent 3d79c4e
commit 3ff46ae
Show file tree

Hide file tree

Showing 11 changed files with 21 additions and 79 deletions.
diff --git a/server/reverse-ffi/lib/RFFI.lean → server/WasmServer.lean b/server/reverse-ffi/lib/RFFI.lean → server/WasmServer.lean
diff --git a/server/lakefile.lean b/server/lakefile.lean
@@ -10,3 +10,8 @@ lean_exe gameserver {
   root := `Main
   supportInterpreter := true
 }
+
+
+@[default_target]
+lean_lib WasmServer where
+  defaultFacets := #[LeanLib.staticFacet]
diff --git a/server/reverse-ffi/main.c → server/main.c b/server/reverse-ffi/main.c → server/main.c
@@ -7,7 +7,7 @@ extern lean_object* game_send_message(lean_object*, lean_object*);
 extern void lean_initialize_runtime_module();
 extern void lean_initialize();
 extern void lean_io_mark_end_initialization();
-extern lean_object * initialize_RFFI(uint8_t builtin, lean_object *);
+extern lean_object * initialize_WasmServer(uint8_t builtin, lean_object *);
 
 int main() {
   lean_initialize();
@@ -16,7 +16,7 @@ int main() {
   // use same default as for Lean executables
   uint8_t builtin = 1;
   lean_object * io_world = lean_io_mk_world();
-  res = initialize_RFFI(builtin, io_world);
+  res = initialize_WasmServer(builtin, io_world);
   if (lean_io_result_is_ok(res)) {
       lean_dec_ref(res);
   } else {

diff --git a/server/reverse-ffi/.gitignore b/server/reverse-ffi/.gitignore
diff --git a/server/reverse-ffi/Makefile b/server/reverse-ffi/Makefile
diff --git a/server/reverse-ffi/README.md b/server/reverse-ffi/README.md
diff --git a/server/reverse-ffi/clean.sh b/server/reverse-ffi/clean.sh
diff --git a/server/reverse-ffi/lib/.gitignore b/server/reverse-ffi/lib/.gitignore
diff --git a/server/reverse-ffi/lib/lakefile.lean b/server/reverse-ffi/lib/lakefile.lean
diff --git a/server/reverse-ffi/test.sh b/server/reverse-ffi/test.sh
diff --git a/wasm.sh b/wasm.sh
@@ -0,0 +1,14 @@
+#!/bin/bash
+
+
+cd server
+
+lake build
+
+
+OUT_DIR=../client/public
+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/WasmServer.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