ffi example (from official lake repository (leanprover/lean4))

FfiTest/Basic.lean

@@ -1 +1,6 @@
+@[extern "my_add"]
+opaque myAdd : UInt32 → UInt32 → UInt32
+
 def hello := "world"
+
+-- #eval myAdd 1 2

Main.lean

@@ -0,0 +1,4 @@
+import FfiTest
+
+def main : IO Unit := do
+  IO.println s!"{myAdd 2 3}"

c/.clangd

@@ -0,0 +1,2 @@
+CompileFlags:
+  Add: [-I/home/qwjyh/.elan/toolchains/stable/include/]

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;
+}
+

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "ffi_test",
+ "lakeDir": ".lake"}

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]