From f19f329b4c41967c76d2c6f8618fb38f91fa09c9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 2 Aug 2023 16:18:40 +0200 Subject: [PATCH] test: reverse FFI from C with Lake --- src/lake/examples/reverse-ffi/.gitignore | 1 + src/lake/examples/reverse-ffi/Makefile | 48 +++++++++++++++++++ src/lake/examples/reverse-ffi/README.md | 3 ++ src/lake/examples/reverse-ffi/clean.sh | 2 + src/lake/examples/reverse-ffi/lib/.gitignore | 1 + src/lake/examples/reverse-ffi/lib/RFFI.lean | 3 ++ .../examples/reverse-ffi/lib/lakefile.lean | 8 ++++ src/lake/examples/reverse-ffi/main.c | 32 +++++++++++++ src/lake/examples/reverse-ffi/test.sh | 4 ++ 9 files changed, 102 insertions(+) create mode 100644 src/lake/examples/reverse-ffi/.gitignore create mode 100644 src/lake/examples/reverse-ffi/Makefile create mode 100644 src/lake/examples/reverse-ffi/README.md create mode 100755 src/lake/examples/reverse-ffi/clean.sh create mode 100644 src/lake/examples/reverse-ffi/lib/.gitignore create mode 100644 src/lake/examples/reverse-ffi/lib/RFFI.lean create mode 100644 src/lake/examples/reverse-ffi/lib/lakefile.lean create mode 100644 src/lake/examples/reverse-ffi/main.c create mode 100755 src/lake/examples/reverse-ffi/test.sh diff --git a/src/lake/examples/reverse-ffi/.gitignore b/src/lake/examples/reverse-ffi/.gitignore new file mode 100644 index 0000000000..95811e0016 --- /dev/null +++ b/src/lake/examples/reverse-ffi/.gitignore @@ -0,0 +1 @@ +/main diff --git a/src/lake/examples/reverse-ffi/Makefile b/src/lake/examples/reverse-ffi/Makefile new file mode 100644 index 0000000000..bd902ef78d --- /dev/null +++ b/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 diff --git a/src/lake/examples/reverse-ffi/README.md b/src/lake/examples/reverse-ffi/README.md new file mode 100644 index 0000000000..8771d2aa30 --- /dev/null +++ b/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`). diff --git a/src/lake/examples/reverse-ffi/clean.sh b/src/lake/examples/reverse-ffi/clean.sh new file mode 100755 index 0000000000..11c3a52b9f --- /dev/null +++ b/src/lake/examples/reverse-ffi/clean.sh @@ -0,0 +1,2 @@ +rm -rf lib/build +rm -f main diff --git a/src/lake/examples/reverse-ffi/lib/.gitignore b/src/lake/examples/reverse-ffi/lib/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/src/lake/examples/reverse-ffi/lib/.gitignore @@ -0,0 +1 @@ +/build diff --git a/src/lake/examples/reverse-ffi/lib/RFFI.lean b/src/lake/examples/reverse-ffi/lib/RFFI.lean new file mode 100644 index 0000000000..b04ce923a4 --- /dev/null +++ b/src/lake/examples/reverse-ffi/lib/RFFI.lean @@ -0,0 +1,3 @@ +@[export my_length] +def myLength (s : String) : UInt64 := + s.length.toUInt64 diff --git a/src/lake/examples/reverse-ffi/lib/lakefile.lean b/src/lake/examples/reverse-ffi/lib/lakefile.lean new file mode 100644 index 0000000000..8c56421b93 --- /dev/null +++ b/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] diff --git a/src/lake/examples/reverse-ffi/main.c b/src/lake/examples/reverse-ffi/main.c new file mode 100644 index 0000000000..24b19b6ebf --- /dev/null +++ b/src/lake/examples/reverse-ffi/main.c @@ -0,0 +1,32 @@ +#include +#include + +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); +} diff --git a/src/lake/examples/reverse-ffi/test.sh b/src/lake/examples/reverse-ffi/test.sh new file mode 100755 index 0000000000..98afcdcab9 --- /dev/null +++ b/src/lake/examples/reverse-ffi/test.sh @@ -0,0 +1,4 @@ +set -ex + +./clean.sh +make run