From 85efdb159a1ac7d16186cdd0d8554be9cce265bd Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 8 Oct 2021 15:20:23 -0400
Subject: [PATCH] test: expand `examples/ffi` to use `getLeanIncludeDir`

---
 examples/ffi-dep/Main.lean              |  2 +-
 examples/ffi/c/add.cpp                  |  5 -----
 examples/ffi/c/ffi.cpp                  |  9 +++++++++
 examples/ffi/lakefile.lean              | 18 +++++++++---------
 examples/ffi/lib/{Add.lean => Ffi.lean} |  3 +++
 examples/ffi/lib/Main.lean              |  2 +-
 examples/ffi/test.sh                    |  2 +-
 7 files changed, 24 insertions(+), 17 deletions(-)
 delete mode 100644 examples/ffi/c/add.cpp
 create mode 100644 examples/ffi/c/ffi.cpp
 rename examples/ffi/lib/{Add.lean => Ffi.lean} (54%)

diff --git a/examples/ffi-dep/Main.lean b/examples/ffi-dep/Main.lean
index ff0f0acc4b..865c82a2ed 100644
--- a/examples/ffi-dep/Main.lean
+++ b/examples/ffi-dep/Main.lean
@@ -1,4 +1,4 @@
-import Add
+import Ffi
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2
diff --git a/examples/ffi/c/add.cpp b/examples/ffi/c/add.cpp
deleted file mode 100644
index 8dcbb71334..0000000000
--- a/examples/ffi/c/add.cpp
+++ /dev/null
@@ -1,5 +0,0 @@
-#include <stdint.h>
-
-extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
-    return a + b;
-}
diff --git a/examples/ffi/c/ffi.cpp b/examples/ffi/c/ffi.cpp
new file mode 100644
index 0000000000..bd9e26e0c6
--- /dev/null
+++ 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));
+}
diff --git a/examples/ffi/lakefile.lean b/examples/ffi/lakefile.lean
index 5ed04c2c0a..f1f8a174b4 100644
--- a/examples/ffi/lakefile.lean
+++ b/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]
 }
diff --git a/examples/ffi/lib/Add.lean b/examples/ffi/lib/Ffi.lean
similarity index 54%
rename from examples/ffi/lib/Add.lean
rename to examples/ffi/lib/Ffi.lean
index 4cf61cece8..9ba99565ca 100644
--- a/examples/ffi/lib/Add.lean
+++ b/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
diff --git a/examples/ffi/lib/Main.lean b/examples/ffi/lib/Main.lean
index ff0f0acc4b..865c82a2ed 100644
--- a/examples/ffi/lib/Main.lean
+++ b/examples/ffi/lib/Main.lean
@@ -1,4 +1,4 @@
-import Add
+import Ffi
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2
diff --git a/examples/ffi/test.sh b/examples/ffi/test.sh
index af25029718..c921904800 100755
--- a/examples/ffi/test.sh
+++ b/examples/ffi/test.sh
@@ -2,4 +2,4 @@ set -e
 
 ./clean.sh
 ./package.sh
-./build/bin/add
+./build/bin/ffi