From abdbc39403616d7bd41034c31daeff06c9be7e16 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 21 Jun 2023 18:19:12 -0400
Subject: [PATCH] test: add test for leanprover/lake#174

---
 Makefile               | 12 ++++++++++--
 test/174/.gitignore    |  1 +
 test/174/Test/1.lean   |  1 +
 test/174/clean.sh      |  1 +
 test/174/lakefile.lean | 10 ++++++++++
 test/174/test.sh       |  6 ++++++
 6 files changed, 29 insertions(+), 2 deletions(-)
 create mode 100644 test/174/.gitignore
 create mode 100644 test/174/Test/1.lean
 create mode 100755 test/174/clean.sh
 create mode 100644 test/174/lakefile.lean
 create mode 100755 test/174/test.sh

diff --git a/Makefile b/Makefile
index 550ef4bef7..0fbc4b4ac0 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,8 @@ test: check-lake test-ci test-bootstrap test-bootstrapped
 
 test-ci: test-tests test-examples
 
-test-tests: test-44 test-49 test-50 test-62 test-75 test-102 test-104 test-116\
+test-tests:\
+	test-44 test-49 test-50 test-62 test-75 test-102 test-104 test-116 test-174\
 	test-manifest test-meta
 
 test-examples: test-init test-hello test-deps\
@@ -22,7 +23,8 @@ test-bootstrapped: test-boostrapped-hello
 
 clean: clean-tests clean-examples clean-build
 
-clean-tests: clean-44 clean-62 clean-102 clean-104 clean-116 clean-manifest
+clean-tests:\
+	clean-44 clean-62 clean-102 clean-104 clean-116 clean-174 clean-manifest
 
 clean-examples: clean-init clean-hello clean-deps\
 	clean-git clean-ffi clean-targets clean-precompile clean-bootstrap
@@ -157,6 +159,12 @@ test-116:
 clean-116:
 	cd test/116 && ./clean.sh
 
+test-174:
+	cd test/174 && ./test.sh
+
+clean-174:
+	cd test/174 && ./clean.sh
+
 clean-manifest:
 	cd test/manifest && ./clean.sh
 
diff --git a/test/174/.gitignore b/test/174/.gitignore
new file mode 100644
index 0000000000..796b96d1c4
--- /dev/null
+++ b/test/174/.gitignore
@@ -0,0 +1 @@
+/build
diff --git a/test/174/Test/1.lean b/test/174/Test/1.lean
new file mode 100644
index 0000000000..a4e20a8f36
--- /dev/null
+++ b/test/174/Test/1.lean
@@ -0,0 +1 @@
+#check (2 : Nat)
diff --git a/test/174/clean.sh b/test/174/clean.sh
new file mode 100755
index 0000000000..1582321863
--- /dev/null
+++ b/test/174/clean.sh
@@ -0,0 +1 @@
+rm -rf build
diff --git a/test/174/lakefile.lean b/test/174/lakefile.lean
new file mode 100644
index 0000000000..3b06bb167f
--- /dev/null
+++ b/test/174/lakefile.lean
@@ -0,0 +1,10 @@
+import Lake
+
+open Lake DSL
+
+package test
+
+@[default_target]
+lean_lib Test {
+  globs := #[.submodules "Test"]
+}
diff --git a/test/174/test.sh b/test/174/test.sh
new file mode 100755
index 0000000000..3b369b6019
--- /dev/null
+++ b/test/174/test.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+./clean.sh
+LAKE=${LAKE:-../../build/bin/lake}
+$LAKE build -v