test: reorg + regression tests

.github/workflows/ci.yml

@@ -57,12 +57,12 @@ jobs:
         name: ${{ matrix.os }}
         path: build
     - name: Check Lake
-      run: make -C examples check-lake
-    - name: Test Examples
-      run: make -C examples test -j4
+      run: make check-lake
+    - name: Test Lake
+      run: make test-ci -j4
     - name: Time Bootstrap
-      run: make -C examples time-bootstrap
+      run: make time-bootstrap
     - name: Check Bootstrap
-      run: make -C examples check-bootstrap
-    - name: Test Bootstrapped Examples
-      run: make -C examples test-bootstrapped -j4
+      run: make check-bootstrap
+    - name: Test Bootstrapped Lake
+      run: make test-bootstrapped -j4

Makefile

@@ -0,0 +1,130 @@
+LAKE ?= ./build/bin/lake
+
+#-------------------------------------------------------------------------------
+# Suite Targets
+#-------------------------------------------------------------------------------
+
+default: build
+
+all: build test-all
+
+test: check-lake test-ci test-bootstrap test-bootstrapped
+
+test-ci: test-tests test-examples
+
+test-tests: test-49 test-50 test-62
+
+test-examples: test-init test-hello test-io test-deps\
+	test-git test-ffi test-targets test-scripts
+
+test-bootstrapped: test-boostrapped-hello
+
+clean: clean-build clean-tests clean-examples
+
+clean-tests: clean-62
+
+clean-examples: clean-init clean-hello clean-io clean-deps\
+	clean-git clean-ffi clean-targets clean-bootstrap
+
+.PHONY: all test test-all test-tests test-examples\
+	clean clean-build clean-tests clean-examples build time-build check-lake\
+	test-bootstrap time-bootstrap check-bootstrap test-bootstrapped
+
+#-------------------------------------------------------------------------------
+# Build Targets
+#-------------------------------------------------------------------------------
+
+build:
+	./build.sh
+
+time-build:
+	./time.sh
+
+clean-build:
+	./clean.sh
+
+check-lake:
+	$(LAKE) self-check
+
+#-------------------------------------------------------------------------------
+# Example Targets
+#-------------------------------------------------------------------------------
+
+test-init:
+	cd examples/init && ./test.sh
+
+clean-init:
+	cd examples/init && ./clean.sh
+
+test-hello:
+	cd examples/hello && ./test.sh
+
+clean-hello:
+	cd examples/hello && ./clean.sh
+
+test-io:
+	cd examples/io && ./test.sh
+
+clean-io:
+	cd examples/io && ./clean.sh
+
+test-deps:
+	cd examples/deps && ./test.sh
+
+clean-deps:
+	cd examples/deps && ./clean.sh
+
+test-git:
+	cd examples/git && ./test.sh
+
+clean-git:
+	cd examples/git && ./clean.sh
+
+test-ffi:
+	cd examples/ffi && ./test.sh
+
+clean-ffi:
+	cd examples/ffi && ./clean.sh
+
+test-targets:
+	cd examples/targets && ./test.sh
+
+clean-targets:
+	cd examples/targets && ./clean.sh
+
+test-scripts:
+	cd examples/scripts && ./test.sh
+
+test-bootstrap:
+	cd examples/bootstrap && ./test.sh
+
+package-bootstrap:
+	cd examples/bootstrap && ./package.sh
+
+clean-bootstrap:
+	cd examples/bootstrap && ./clean.sh
+
+time-bootstrap:
+	cd examples/bootstrap && ./time.sh
+
+check-bootstrap:
+	cd examples/bootstrap && ./check.sh
+
+test-boostrapped-hello:
+	cd examples/hello && ./bootstrapped-test.sh
+
+#-------------------------------------------------------------------------------
+# Test Targets
+#-------------------------------------------------------------------------------
+
+test-49:
+	cd test/49 && ./test.sh
+
+test-50:
+	cd test/50 && ./test.sh
+
+test-62:
+	cd test/62 && ./test.sh
+
+clean-62:
+	cd test/62 && ./clean.sh

build.sh

@@ -1,7 +1,12 @@
 #!/usr/bin/env sh
+
 if [ "$OS" = "Windows_NT" ]; then
   LINK_OPTS=
 else
   LINK_OPTS=-rdynamic
 fi
-leanmake PKG=Lake OLEAN_OUT=build/lib TEMP_OUT=build/ir BIN_NAME=lake LEAN_PATH=./build/lib bin LINK_OPTS=${LINK_OPTS} "$@"
+
+LEAN_SYSROOT=${LEAN_SYSROOT:-`lean --print-prefix`}
+LEAN_MAKEFILE="$LEAN_SYSROOT/share/lean/lean.mk"
+EXTRA_ARGS="PKG=Lake OLEAN_OUT=build/lib TEMP_OUT=build/ir BIN_NAME=lake LEAN_PATH=./build/lib LINK_OPTS=$LINK_OPTS"
+PATH="$LEAN_SYSROOT/bin:$PATH" ${MAKE:-make} -f "$LEAN_MAKEFILE" $EXTRA_ARGS bin "$@"

test/49/test.sh

@@ -0,0 +1,11 @@
+set -euo pipefail
+
+INIT_REQ=$'Content-Length: 46\r\n\r\n{"jsonrpc":"2.0","method":"initialize","id":1}'
+INITD_NOT=$'Content-Length: 40\r\n\r\n{"jsonrpc":"2.0","method":"initialized"}'
+SD_REQ=$'Content-Length: 44\r\n\r\n{"jsonrpc":"2.0","method":"shutdown","id":2}'
+EXIT_NOT=$'Content-Length: 33\r\n\r\n{"jsonrpc":"2.0","method":"exit"}'
+MSGS="$INIT_REQ$INITD_NOT$SD_REQ$EXIT_NOT"
+
+echo "does not compile" > lakefile.lean
+echo -n "$MSGS" | ${LAKE:-../../build/bin/lake} serve >/dev/null
+rm lakefile.lean

test/50/foo/.gitignore

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

test/50/foo/foo.lean

@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println s!"Hello, world!"

test/50/foo/lakefile.lean

@@ -0,0 +1,9 @@
+import Lake
+open Lake DSL
+
+package foo where
+  moreLeanArgs := #[(__args__).get! 0]
+  moreLeancArgs := #[(__args__).get! 1]
+
+@[defaultTarget]
+lean_exe foo

test/50/foo/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2022-06-14

test/50/test.sh

@@ -0,0 +1,8 @@
+set -exo pipefail
+LAKE=${LAKE:-../../../build/bin/lake}
+cd foo
+rm -rf build
+${LAKE} build -- -Dhygiene=true -DBAR | grep -m2 foo.c
+${LAKE} build -- -Dhygiene=false -DBAZ | grep -m2 foo.c
+${LAKE} build -- -Dhygiene=false -DBAR | grep -m1 foo.o
+${LAKE} build -- -Dhygiene=true -DBAR | grep -m1 foo.olean

test/62/.gitignore

@@ -0,0 +1 @@
+/foo

test/62/clean.sh

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

test/62/test.sh

@@ -0,0 +1,7 @@
+set -euxo pipefail
+./clean.sh
+lake +leanprover/lean4:4.0.0-m3 new foo
+cd foo
+lake +leanprover/lean4:4.0.0-m3 build | grep -m1 foo
+cp ../../../lean-toolchain lean-toolchain
+${LAKE:-../../../build/bin/lake} build | grep -m1 foo