From 91d3df58cd01ac481008a8f52a77053fd32f6e31 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 28 Jul 2021 09:10:14 -0400
Subject: [PATCH] test: add git example

---
 examples/git/.gitignore    |  2 ++
 examples/git/GitHello.lean |  1 +
 examples/git/clean.sh      |  2 ++
 examples/git/package.lean  | 18 ++++++++++++++++++
 examples/git/package.sh    |  1 +
 examples/git/test.sh       |  3 +++
 examples/test.sh           |  5 +++++
 7 files changed, 32 insertions(+)
 create mode 100644 examples/git/.gitignore
 create mode 100644 examples/git/GitHello.lean
 create mode 100644 examples/git/clean.sh
 create mode 100644 examples/git/package.lean
 create mode 100644 examples/git/package.sh
 create mode 100644 examples/git/test.sh

diff --git a/examples/git/.gitignore b/examples/git/.gitignore
new file mode 100644
index 0000000000..29035da63c
--- /dev/null
+++ b/examples/git/.gitignore
@@ -0,0 +1,2 @@
+/build
+/lean_packages
diff --git a/examples/git/GitHello.lean b/examples/git/GitHello.lean
new file mode 100644
index 0000000000..ccbbf4cfd0
--- /dev/null
+++ b/examples/git/GitHello.lean
@@ -0,0 +1 @@
+import Hello
diff --git a/examples/git/clean.sh b/examples/git/clean.sh
new file mode 100644
index 0000000000..ab33e94a34
--- /dev/null
+++ b/examples/git/clean.sh
@@ -0,0 +1,2 @@
+rm -rf build
+rm -rf lean_packages
diff --git a/examples/git/package.lean b/examples/git/package.lean
new file mode 100644
index 0000000000..e4b312815c
--- /dev/null
+++ b/examples/git/package.lean
@@ -0,0 +1,18 @@
+import Lake.Package
+
+open Lake System
+
+def package : PackageConfig := {
+  name := "gitHello"
+  version := "1.0"
+  dependencies := [
+    {
+      name := "hello",
+      src := Source.git
+        "https://github.com/tydeu/lean4-lake.git"
+        "71defa066dd845a31d19547f1a3e01f79c5fc8d9"
+        (branch := none)
+      dir := FilePath.mk "examples" / "hello"
+    }
+  ]
+}
diff --git a/examples/git/package.sh b/examples/git/package.sh
new file mode 100644
index 0000000000..b6449c2dd0
--- /dev/null
+++ b/examples/git/package.sh
@@ -0,0 +1 @@
+../../build/bin/Lake build-bin
diff --git a/examples/git/test.sh b/examples/git/test.sh
new file mode 100644
index 0000000000..17a6aca2f8
--- /dev/null
+++ b/examples/git/test.sh
@@ -0,0 +1,3 @@
+./clean.sh
+./package.sh
+./build/bin/gitHello
diff --git a/examples/test.sh b/examples/test.sh
index 84fa211f1f..1201d6ea1a 100644
--- a/examples/test.sh
+++ b/examples/test.sh
@@ -18,6 +18,11 @@ cd deps
 ./test.sh
 cd ..
 
+echo 'testing git'
+cd git
+./test.sh
+cd ..
+
 echo 'testing ext'
 cd ext
 ./test.sh