diff --git a/examples/ext/.gitignore b/examples/ext/.gitignore
new file mode 100644
index 0000000000..796b96d1c4
--- /dev/null
+++ b/examples/ext/.gitignore
@@ -0,0 +1 @@
+/build
diff --git a/examples/ext/README.md b/examples/ext/README.md
new file mode 100644
index 0000000000..4ebb12c759
--- /dev/null
+++ b/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.
diff --git a/examples/ext/clean.sh b/examples/ext/clean.sh
new file mode 100644
index 0000000000..1582321863
--- /dev/null
+++ b/examples/ext/clean.sh
@@ -0,0 +1 @@
+rm -rf build
diff --git a/examples/ext/ext/add.cpp b/examples/ext/ext/add.cpp
new file mode 100644
index 0000000000..8dcbb71334
--- /dev/null
+++ b/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;
+}
diff --git a/examples/ext/lib/Add.lean b/examples/ext/lib/Add.lean
new file mode 100644
index 0000000000..57be87d8f5
--- /dev/null
+++ 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
diff --git a/examples/ext/package.lean b/examples/ext/package.lean
new file mode 100644
index 0000000000..dc2a865249
--- /dev/null
+++ b/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
+}
diff --git a/examples/ext/package.sh b/examples/ext/package.sh
new file mode 100644
index 0000000000..b6449c2dd0
--- /dev/null
+++ b/examples/ext/package.sh
@@ -0,0 +1 @@
+../../build/bin/Lake build-bin
diff --git a/examples/ext/test.sh b/examples/ext/test.sh
new file mode 100644
index 0000000000..88dc66472f
--- /dev/null
+++ b/examples/ext/test.sh
@@ -0,0 +1,3 @@
+./clean.sh
+./package.sh
+./build/bin/add