test: reorg + regression tests
This commit is contained in:
tydeu
parent
4ff44fb050
commit
8faafb7ef6
13 changed files with 184 additions and 88 deletions
14
.github/workflows/ci.yml
vendored
14
.github/workflows/ci.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
130
Makefile
Normal file
130
Makefile
Normal file
|
|
@ -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
|
||||
7
build.sh
7
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 "$@"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
11
test/49/test.sh
Normal file
11
test/49/test.sh
Normal file
|
|
@ -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
|
||||
1
test/50/foo/.gitignore
vendored
Normal file
1
test/50/foo/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
/build
|
||||
2
test/50/foo/foo.lean
Normal file
2
test/50/foo/foo.lean
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
def main : IO Unit :=
|
||||
IO.println s!"Hello, world!"
|
||||
9
test/50/foo/lakefile.lean
Normal file
9
test/50/foo/lakefile.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
package foo where
|
||||
moreLeanArgs := #[(__args__).get! 0]
|
||||
moreLeancArgs := #[(__args__).get! 1]
|
||||
|
||||
@[defaultTarget]
|
||||
lean_exe foo
|
||||
1
test/50/foo/lean-toolchain
Normal file
1
test/50/foo/lean-toolchain
Normal file
|
|
@ -0,0 +1 @@
|
|||
leanprover/lean4:nightly-2022-06-14
|
||||
8
test/50/test.sh
Normal file
8
test/50/test.sh
Normal file
|
|
@ -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
|
||||
1
test/62/.gitignore
vendored
Normal file
1
test/62/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
/foo
|
||||
1
test/62/clean.sh
Normal file
1
test/62/clean.sh
Normal file
|
|
@ -0,0 +1 @@
|
|||
rm -rf foo
|
||||
7
test/62/test.sh
Normal file
7
test/62/test.sh
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue