reverse-ffi IO

server/reverse-ffi/Makefile

@@ -21,7 +21,8 @@ endif
 
 $(OUT_DIR)/main: main.c lake | $(OUT_DIR)
 # Add library paths for Lake package and for Lean itself
-	emcc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) lib/build/ir/RFFI.c -lInit -lLean -lleancpp -lleanrt $(LINK_FLAGS)
+	emcc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) lib/build/ir/RFFI.c -lInit -lLean -lleancpp -lleanrt $(LINK_FLAGS) \
+	  -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto
 
 run: $(OUT_DIR)/main
 ifeq ($(OS),Windows_NT)
@@ -34,26 +35,26 @@ endif
 # Alternatively, we can copy all shared lib dependencies to the current directory
 # in order to avoid path set up and obtain a more portable executable
 
-ifeq ($(OS),Windows_NT)
-SHLIB_PREFIX :=
-SHLIB_EXT := dll
-LEAN_SHLIB := $(LEAN_SYSROOT)/bin/libleanshared.$(SHLIB_EXT)
-else
-SHLIB_PREFIX := lib
-# Add current directory to loader path (default on Windows)
-ifeq ($(shell uname -s),Darwin)
-LINK_FLAGS_LOCAL := -Wl,-rpath,@executable_path
-SHLIB_EXT := dylib
-else
-LINK_FLAGS_LOCAL := -Wl,-rpath,'$${ORIGIN}'
-SHLIB_EXT := so
-endif
-LEAN_SHLIB=$(LEAN_LIBDIR)/libleanshared.$(SHLIB_EXT)
-endif
-
-$(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
-	cp -f $(LEAN_SHLIB) lib/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lleanshared $(LINK_FLAGS_LOCAL)
-
-run-local: $(OUT_DIR)/main-local
-	$(OUT_DIR)/main-local
+# ifeq ($(OS),Windows_NT)
+# SHLIB_PREFIX :=
+# SHLIB_EXT := dll
+# LEAN_SHLIB := $(LEAN_SYSROOT)/bin/libleanshared.$(SHLIB_EXT)
+# else
+# SHLIB_PREFIX := lib
+# # Add current directory to loader path (default on Windows)
+# ifeq ($(shell uname -s),Darwin)
+# LINK_FLAGS_LOCAL := -Wl,-rpath,@executable_path
+# SHLIB_EXT := dylib
+# else
+# LINK_FLAGS_LOCAL := -Wl,-rpath,'$${ORIGIN}'
+# SHLIB_EXT := so
+# endif
+# LEAN_SHLIB=$(LEAN_LIBDIR)/libleanshared.$(SHLIB_EXT)
+# endif
+
+# $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
+# 	cp -f $(LEAN_SHLIB) lib/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
+# 	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lleanshared $(LINK_FLAGS_LOCAL)
+
+# run-local: $(OUT_DIR)/main-local
+# 	$(OUT_DIR)/main-local

server/reverse-ffi/lib/RFFI.lean

@@ -1,3 +1,6 @@
+import Lean
+
 @[export my_length]
-def myLength (s : String) : UInt64 :=
-  s.length.toUInt64
+def myLength (s : String) : IO Unit := do
+  IO.println "hello"
+  return () -- IO.println Lean.origin

server/reverse-ffi/main.c

@@ -1,7 +1,7 @@
 #include <stdio.h>
 #include <lean/lean.h>
 
-extern uint64_t my_length(lean_obj_arg);
+extern lean_object* my_length(lean_object*, lean_object*);
 
 // see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization
 extern void lean_initialize_runtime_module();
@@ -10,11 +10,13 @@ extern void lean_io_mark_end_initialization();
 extern lean_object * initialize_RFFI(uint8_t builtin, lean_object *);
 
 int main() {
+  lean_initialize();
   lean_initialize_runtime_module();
   lean_object * res;
   // use same default as for Lean executables
   uint8_t builtin = 1;
-  res = initialize_RFFI(builtin, lean_io_mk_world());
+  lean_object * io_world = lean_io_mk_world();
+  res = initialize_RFFI(builtin, io_world);
   if (lean_io_result_is_ok(res)) {
       lean_dec_ref(res);
   } else {
@@ -27,6 +29,5 @@ int main() {
   // actual program
 
   lean_object * s = lean_mk_string("hello!");
-  uint64_t l = my_length(s);
-  printf("output: %ld\n", l);
+  my_length(s, lean_io_mk_world());
 }

server/reverse-ffi/test.sh

@@ -3,4 +3,3 @@ set -ex
 ./clean.sh
 
 make run
-make run-local