test: expand examples/ffi to use getLeanIncludeDir

examples/ffi-dep/Main.lean

@@ -1,4 +1,4 @@
-import Add
+import Ffi
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2

examples/ffi/c/add.cpp

@@ -1,5 +0,0 @@
-#include <stdint.h>
-
-extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
-    return a + b;
-}

examples/ffi/c/ffi.cpp

@@ -0,0 +1,9 @@
+#include <lean/lean.h>
+
+extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
+    return a + b;
+}
+
+extern "C" lean_obj_res my_lean_fun() {
+    return lean_io_result_mk_ok(lean_box(0));
+}

examples/ffi/lakefile.lean

@@ -2,23 +2,23 @@ import Lake
 open System Lake DSL
 
 def cDir : FilePath := "c"
-def addSrc := cDir / "add.cpp"
-
+def ffiSrc := cDir / "ffi.cpp"
 def buildDir := defaultBuildDir
-def addO := buildDir / cDir / "add.o"
-def cLib := buildDir / cDir / "libadd.a"
 
-def addOTarget (pkgDir : FilePath) : FileTarget :=
-  oFileTarget (pkgDir / addO) (pkgDir / addSrc : FilePath)
+def ffiOTarget (pkgDir : FilePath) : FileTarget :=
+  let oFile := pkgDir / buildDir / cDir / "ffi.o"
+  let srcTarget : FileTarget := coe <| pkgDir / ffiSrc
+  fileTargetWithDep oFile srcTarget fun srcFile => do
+    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString]
 
 def cLibTarget (pkgDir : FilePath) : FileTarget :=
-  staticLibTarget (pkgDir / cLib) #[addOTarget pkgDir]
+  let libFile := pkgDir / buildDir / cDir / "libffi.a"
+  staticLibTarget libFile #[ffiOTarget pkgDir]
 
 package ffi (pkgDir) (args) {
   -- customize layout
   srcDir := "lib"
-  libRoots := #[`Add]
-  binName := "add"
+  libRoots := #[`Ffi]
   -- specify the lib as an additional target
   moreLibTargets := #[cLibTarget pkgDir]
 }

examples/ffi/lib/Ffi.lean

@@ -1,2 +1,5 @@
 @[extern "my_add"]
 constant myAdd : UInt32 → UInt32 → UInt32
+
+@[extern "my_lean_fun"]
+constant myLeanFun : IO PUnit

examples/ffi/lib/Main.lean

@@ -1,4 +1,4 @@
-import Add
+import Ffi
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2

examples/ffi/test.sh

@@ -2,4 +2,4 @@ set -e
 
 ./clean.sh
 ./package.sh
-./build/bin/add
+./build/bin/ffi