test: reverse FFI from C with Lake

src/lake/examples/reverse-ffi/.gitignore

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

src/lake/examples/reverse-ffi/Makefile

@@ -0,0 +1,48 @@
+.PHONY: all run run-local lake
+
+all: run run-local
+
+# Link C binary against Lake package dynamic library
+
+lake:
+	lake --dir=lib build
+
+ifneq ($(OS),Windows_NT)
+# Add shared library paths to loader path (no Windows equivalent)
+  LINK_FLAGS=-Wl,-rpath,`lean --print-prefix`/lib/lean -Wl,-rpath,$(PWD)/lib/build/lib
+endif
+
+main: main.c lake
+# Add library paths for Lake package and for Lean itself
+	cc -o $@ $< -I `lean --print-prefix`/include -L `lean --print-libdir` -L lib/build/lib -lRFFI -lleanshared $(LINK_FLAGS)
+
+run: main
+ifeq ($(OS),Windows_NT)
+# Add shared library path to loader path dynamically (`lean`'s directory is already in `PATH`)
+	PATH=lib/build/lib:$(PATH) ./main
+else
+	./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_EXT=dll
+else
+  # 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
+endif
+
+main-local: main.c lake
+	cp -f `lean --print-libdir`/libleanshared.$(SHLIB_EXT) lib/build/lib/libRFFI.$(SHLIB_EXT) .
+	cc -o $@ $< -I `lean --print-prefix`/include -L . -lRFFI -lleanshared $(LINK_FLAGS_LOCAL)
+
+run-local: main-local
+	./main-local

src/lake/examples/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`).

src/lake/examples/reverse-ffi/clean.sh

@@ -0,0 +1,2 @@
+rm -rf lib/build
+rm -f main

src/lake/examples/reverse-ffi/lib/.gitignore

@@ -0,0 +1 @@
+/build

src/lake/examples/reverse-ffi/lib/RFFI.lean

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

src/lake/examples/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]

src/lake/examples/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);
+}

src/lake/examples/reverse-ffi/test.sh

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