test: add test for leanprover/lake#174

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
 

test/174/.gitignore

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

test/174/Test/1.lean

@@ -0,0 +1 @@
+#check (2 : Nat)

test/174/clean.sh

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

test/174/lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+
+open Lake DSL
+
+package test
+
+@[default_target]
+lean_lib Test {
+  globs := #[.submodules "Test"]
+}

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