test: add simple extension example

examples/ext/.gitignore

@@ -0,0 +1 @@
+/build

examples/ext/README.md

@@ -0,0 +1,2 @@
+This example was adapted from Xubai Wong's [`simpleAdd`](https://github.com/xubaiw/lean-lake-build-script-demo/tree/758373277cb8615f9b9cb43025fa7d59d6b0badb/simpleAdd) Lake demo.
+Done with [permission](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/leanpkg.2B.2B.20idea.20.5BRFC.5D/near/246711345) from the author.

examples/ext/clean.sh

@@ -0,0 +1 @@
+rm -rf build

examples/ext/ext/add.cpp

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

examples/ext/lib/Add.lean

@@ -0,0 +1,5 @@
+@[extern "my_add"]
+constant myAdd : UInt32 → UInt32 → UInt32
+
+def main : IO Unit :=
+  IO.println <| myAdd 1 2

examples/ext/package.lean

@@ -0,0 +1,33 @@
+import Lake.Build
+import Lake.Package
+open Lake System
+
+def extDir : FilePath := "ext"
+def addSrc := extDir / "add.cpp"
+
+def buildDir := defaultBuildDir
+def addO := buildDir / extDir / "add.o"
+def extLib := buildDir / extDir / "libext.a"
+
+def fetchAddOTarget : IO FileTarget := do
+  skipIfNewer addO (← getMTime addSrc) <|
+    BuildTask.spawn <| compileO addO addSrc (cmd := "c++")
+
+def fetchExtLibTarget : IO FileTarget := do
+  let oTarget ← fetchAddOTarget
+  skipIfNewer extLib oTarget.mtime <|
+    oTarget >> compileStaticLib extLib #[addO]
+
+def package : PackageConfig := {
+  name := "ext"
+  version := "0.1"
+  -- customize layout
+  srcDir := "lib"
+  moduleRoot := `Add
+  binName := "add"
+  -- specify path to the lib for linker
+  linkArgs := #[extLib.toString]
+  -- specify the lib target as an additional dependency
+  buildMoreDepsTarget := fetchExtLibTarget.map fun target =>
+    LeanTarget.fromMTimeTarget <| target.discardArtifact
+}

examples/ext/package.sh

@@ -0,0 +1 @@
+../../build/bin/Lake build-bin

examples/ext/test.sh

@@ -0,0 +1,3 @@
+./clean.sh
+./package.sh
+./build/bin/add