From 3183a106c51b0feb861284c4e2e483096fbe1a85 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Fri, 25 Oct 2024 16:47:35 +0900
Subject: [PATCH] ffi example (from official lake repository
 (leanprover/lean4))

---
 FfiTest/Basic.lean |  7 ++++++-
 Main.lean          |  4 ++++
 c/.clangd          |  2 ++
 c/ffi.cpp          |  8 ++++++++
 lake-manifest.json |  5 +++++
 lakefile.lean      | 17 ++++++++++++++++-
 6 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 Main.lean
 create mode 100644 c/.clangd
 create mode 100644 c/ffi.cpp
 create mode 100644 lake-manifest.json

diff --git a/FfiTest/Basic.lean b/FfiTest/Basic.lean
index e99d3a6..e9bc4b0 100644
--- a/FfiTest/Basic.lean
+++ b/FfiTest/Basic.lean
@@ -1 +1,6 @@
-def hello := "world"
\ No newline at end of file
+@[extern "my_add"]
+opaque myAdd : UInt32 → UInt32 → UInt32
+
+def hello := "world"
+
+-- #eval myAdd 1 2
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..c4738b3
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import FfiTest
+
+def main : IO Unit := do
+  IO.println s!"{myAdd 2 3}"
diff --git a/c/.clangd b/c/.clangd
new file mode 100644
index 0000000..470521c
--- /dev/null
+++ b/c/.clangd
@@ -0,0 +1,2 @@
+CompileFlags:
+  Add: [-I/home/qwjyh/.elan/toolchains/stable/include/]
diff --git a/c/ffi.cpp b/c/ffi.cpp
new file mode 100644
index 0000000..579ad8f
--- /dev/null
+++ b/c/ffi.cpp
@@ -0,0 +1,8 @@
+#include <cstdint>
+#include <lean/lean.h>
+#include <curl/curl.h>
+
+extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
+    return a + b;
+}
+
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..7973206
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "ffi_test",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 6b29568..345edb7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,21 @@ open Lake DSL
 package "ffi_test" where
   version := v!"0.1.0"
 
-@[default_target]
 lean_lib «FfiTest» where
   -- add library configuration options here
+
+@[default_target]
+lean_exe test where
+  root := `Main
+
+target ffi.o pkg : FilePath := do
+  let oFile := pkg.buildDir / "c" / "ffi.o"
+  let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp"
+  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
+  buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
+
+extern_lib libleanffi pkg := do
+  let ffiO ← ffi.o.fetch
+  let name := nameToStaticLib "leanffi"
+  IO.println s!"{repr name}"
+  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]