From 8faafb7ef68189faff3179629a06414cf1bdf46c Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 14 Jun 2022 18:33:01 -0400 Subject: [PATCH] test: reorg + regression tests --- .github/workflows/ci.yml | 14 ++-- Makefile | 130 +++++++++++++++++++++++++++++++++++++ build.sh | 7 +- examples/Makefile | 80 ----------------------- test/49/test.sh | 11 ++++ test/50/foo/.gitignore | 1 + test/50/foo/foo.lean | 2 + test/50/foo/lakefile.lean | 9 +++ test/50/foo/lean-toolchain | 1 + test/50/test.sh | 8 +++ test/62/.gitignore | 1 + test/62/clean.sh | 1 + test/62/test.sh | 7 ++ 13 files changed, 184 insertions(+), 88 deletions(-) create mode 100644 Makefile delete mode 100644 examples/Makefile create mode 100644 test/49/test.sh create mode 100644 test/50/foo/.gitignore create mode 100644 test/50/foo/foo.lean create mode 100644 test/50/foo/lakefile.lean create mode 100644 test/50/foo/lean-toolchain create mode 100644 test/50/test.sh create mode 100644 test/62/.gitignore create mode 100644 test/62/clean.sh create mode 100644 test/62/test.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6ee120aa1d..7216a3fd32 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Makefile b/Makefile new file mode 100644 index 0000000000..2fed57592b --- /dev/null +++ b/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 diff --git a/build.sh b/build.sh index ffde950680..4f949786b1 100755 --- a/build.sh +++ b/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 "$@" diff --git a/examples/Makefile b/examples/Makefile deleted file mode 100644 index 849f2c14df..0000000000 --- a/examples/Makefile +++ /dev/null @@ -1,80 +0,0 @@ -LAKE ?= ../build/bin/lake - -all: check-lake test time-bootstrap check-bootstrap test-bootstrapped - -test: test-init test-hello test-io test-deps\ - test-git test-ffi test-targets test-scripts - -clean: clean-init clean-hello clean-io clean-deps\ - clean-git clean-ffi clean-targets clean-bootstrap - -check-lake: - $(LAKE) self-check - -test-init: - cd init && ./test.sh - -clean-init: - cd init && ./clean.sh - -test-hello: - cd hello && ./test.sh - -clean-hello: - cd hello && ./clean.sh - -test-io: - cd io && ./test.sh - -clean-io: - cd io && ./clean.sh - -test-deps: - cd deps && ./test.sh - -clean-deps: - cd deps && ./clean.sh - -test-git: - cd git && ./test.sh - -clean-git: - cd git && ./clean.sh - -test-ffi: - cd ffi && ./test.sh - -clean-ffi: - cd ffi && ./clean.sh - -test-targets: - cd targets && ./test.sh - -clean-targets: - cd targets && ./clean.sh - -test-scripts: - cd scripts && ./test.sh - -test-bootstrap: - cd bootstrap && ./test.sh - -package-bootstrap: - cd bootstrap && ./package.sh - -clean-bootstrap: - cd bootstrap && ./clean.sh - -time-bootstrap: - cd bootstrap && ./time.sh - -check-bootstrap: - cd bootstrap && ./check.sh - -test-bootstrapped: test-boostrapped-hello - -test-boostrapped-hello: - cd hello && ./bootstrapped-test.sh - -.PHONY: all check-lake test clean\ - test-bootstrap time-bootstrap check-bootstrap test-bootstrapped diff --git a/test/49/test.sh b/test/49/test.sh new file mode 100644 index 0000000000..606f5da2b2 --- /dev/null +++ b/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 diff --git a/test/50/foo/.gitignore b/test/50/foo/.gitignore new file mode 100644 index 0000000000..796b96d1c4 --- /dev/null +++ b/test/50/foo/.gitignore @@ -0,0 +1 @@ +/build diff --git a/test/50/foo/foo.lean b/test/50/foo/foo.lean new file mode 100644 index 0000000000..dccecb1f5c --- /dev/null +++ b/test/50/foo/foo.lean @@ -0,0 +1,2 @@ +def main : IO Unit := + IO.println s!"Hello, world!" diff --git a/test/50/foo/lakefile.lean b/test/50/foo/lakefile.lean new file mode 100644 index 0000000000..2e6565d457 --- /dev/null +++ b/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 diff --git a/test/50/foo/lean-toolchain b/test/50/foo/lean-toolchain new file mode 100644 index 0000000000..03095f8168 --- /dev/null +++ b/test/50/foo/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2022-06-14 diff --git a/test/50/test.sh b/test/50/test.sh new file mode 100644 index 0000000000..875c761fbf --- /dev/null +++ b/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 diff --git a/test/62/.gitignore b/test/62/.gitignore new file mode 100644 index 0000000000..0661686d61 --- /dev/null +++ b/test/62/.gitignore @@ -0,0 +1 @@ +/foo diff --git a/test/62/clean.sh b/test/62/clean.sh new file mode 100644 index 0000000000..1cfb9dabe4 --- /dev/null +++ b/test/62/clean.sh @@ -0,0 +1 @@ +rm -rf foo diff --git a/test/62/test.sh b/test/62/test.sh new file mode 100644 index 0000000000..4c27e8cbed --- /dev/null +++ b/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