reverse-ffi test

server/reverse-ffi/.gitignore

@@ -0,0 +1,2 @@
+/main
+/out

server/reverse-ffi/Makefile

@@ -0,0 +1,59 @@
+.PHONY: all run run-local lake
+
+all: run run-local
+
+# Link C binary against Lake package dynamic library
+
+lake:
+	lake --dir=lib build
+
+OUT_DIR = out
+LEAN_SYSROOT ?= /home/alex/Projects/lean4/build/release/stage1
+LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean
+
+$(OUT_DIR):
+	mkdir -p $@
+
+ifneq ($(OS),Windows_NT)
+# Add shared library paths to loader path (no Windows equivalent)
+LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lib/build/lib
+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)
+
+run: $(OUT_DIR)/main
+ifeq ($(OS),Windows_NT)
+# Add shared library paths to loader path dynamically
+	env PATH="lib/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main
+else
+	$(OUT_DIR)/main
+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

server/reverse-ffi/README.md

@@ -0,0 +1,3 @@
+# Reverse FFI
+
+This a simple example of how a Lake library (`lib/`) can be used from a foreign language and build system (`main.c` and `Makefile`).

server/reverse-ffi/clean.sh

@@ -0,0 +1 @@
+rm -rf out lib/build lib/lakefile.olean lib/lake-manifest.json

server/reverse-ffi/lib/.gitignore

@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-manifest.json

server/reverse-ffi/lib/RFFI.lean

@@ -0,0 +1,3 @@
+@[export my_length]
+def myLength (s : String) : UInt64 :=
+  s.length.toUInt64

server/reverse-ffi/lib/lakefile.lean

@@ -0,0 +1,8 @@
+import Lake
+open System Lake DSL
+
+package rffi
+
+@[default_target]
+lean_lib RFFI where
+  defaultFacets := #[LeanLib.sharedFacet]

server/reverse-ffi/main.c

@@ -0,0 +1,32 @@
+#include <stdio.h>
+#include <lean/lean.h>
+
+extern uint64_t my_length(lean_obj_arg);
+
+// see https://leanprover.github.io/lean4/doc/dev/ffi.html#initialization
+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 *);
+
+int main() {
+  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());
+  if (lean_io_result_is_ok(res)) {
+      lean_dec_ref(res);
+  } else {
+      lean_io_result_show_error(res);
+      lean_dec(res);
+      return 1;  // do not access Lean declarations if initialization failed
+  }
+  lean_io_mark_end_initialization();
+
+  // actual program
+
+  lean_object * s = lean_mk_string("hello!");
+  uint64_t l = my_length(s);
+  printf("output: %ld\n", l);
+}

server/reverse-ffi/test.sh

@@ -0,0 +1,6 @@
+set -ex
+
+./clean.sh
+
+make run
+make run-local