diff --git a/Makefile b/Makefile index 30d276b81..425070b8f 100644 --- a/Makefile +++ b/Makefile @@ -38,7 +38,7 @@ export SCHEME .PHONY: all idris2-exec ${TARGET} support support-clean clean distclean -all: support ${TARGET} libs +all: support ${TARGET} testbin libs idris2-exec: ${TARGET} @@ -64,6 +64,9 @@ contrib: prelude libs : prelude base network contrib +testbin: + @${MAKE} -C tests testbin + test: @${MAKE} -C tests only=$(only) IDRIS2=../../../${TARGET} diff --git a/README.md b/README.md index 855c6db8a..dd4bc5480 100644 --- a/README.md +++ b/README.md @@ -16,8 +16,8 @@ you have Chez Scheme installed, with the executable name `chez`, type: You may need to change `chez` to be the local name of your Chez Scheme. This is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the -version). On a modern desktop machine, this process should take no more than -2 or 3 minutes. +version). On a modern desktop machine, this process (including tests) +should take less than 5 minutes. Idris 2 is mostly backwards compatible with Idris 1, with some minor exceptions. The most notable user visible differences, which might cause Idris diff --git a/bootstrap.sh b/bootstrap.sh index 138aedbee..39c26ed09 100644 --- a/bootstrap.sh +++ b/bootstrap.sh @@ -26,9 +26,13 @@ PREFIX="`dirname $DIR`"/bootstrap echo ${PREFIX} IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network" +NEWPREFIX="`dirname $DIR`" +IDRIS2_NEW_PATH="${NEWPREFIX}/libs/prelude/build/ttc:${NEWPREFIX}/libs/base/build/ttc:${NEWPREFIX}/libs/network/build/ttc" make libs SCHEME=${SCHEME} PREFIX=${PREFIX} make install SCHEME=${SCHEME} PREFIX=${PREFIX} make clean IDRIS2_BOOT=${PREFIX}/bin/idris2 make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH} -make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support + +echo "Testing using libraries in ${IDRIS2_NEW_PATH}" +make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support diff --git a/tests/Makefile b/tests/Makefile index d125edc75..1c4ec763d 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,8 +1,14 @@ INTERACTIVE ?= --interactive -test: clean +.PHONY: testbin test + +test: + ./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only) + +testbin: build/exec/runtests + +build/exec/runtests: ${IDRIS2_BOOT} --build tests.ipkg - @./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only) clean: $(RM) -r build diff --git a/tests/typedd-book/chapter11/ArithCmd.idr b/tests/typedd-book/chapter11/ArithCmd.idr index 500051426..6de57a200 100644 --- a/tests/typedd-book/chapter11/ArithCmd.idr +++ b/tests/typedd-book/chapter11/ArithCmd.idr @@ -2,7 +2,7 @@ import Data.Primitives.Views import Data.Strings import System --- %default total -- put this back when codata works! +%default total data Command : Type -> Type where PutStr : String -> Command ()