max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-22 07:56:06 -08:00
parent a858eeea36
commit 167549de59
6 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/compile.sh
View file

@ -6,7 +6,7 @@ fi
ulimit -s 8192
BIN_DIR=../../bin
LEAN=$BIN_DIR/lean
export LEAN_PATH=Init=../../library/Init:Test=.
export LEAN_PATH=Init=../../src/Init:Test=.
ff=$1
if [[ "$OSTYPE" == "msys" ]]; then

2
tests/compiler/test_single.sh
View file

@ -6,7 +6,7 @@ fi
ulimit -s 8192
LEAN=$1
BIN_DIR=../../bin
export LEAN_PATH=Init=../../library/Init:Test=.
export LEAN_PATH=Init=../../src/Init:Test=.
if [ $# -ne 3 ]; then
INTERACTIVE=no
else

2
tests/lean/fail/test_single.sh
View file

@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
fi
ulimit -s 8192
LEAN=$1
export LEAN_PATH=Init=../../../library/Init:Test=.
export LEAN_PATH=Init=../../../src/Init:Test=.
f=$2
echo "-- testing $f"
"$LEAN" -j 0 "$f"

2
tests/lean/run/test_single.sh
View file

@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
fi
ulimit -s 8192
LEAN=$1
export LEAN_PATH=Init=../../../library/Init:Test=.
export LEAN_PATH=Init=../../../src/Init:Test=.
f=$2
echo "-- testing $f"
"$LEAN" -j 0 "$f"

2
tests/lean/test_single.sh
View file

@ -5,7 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
fi
ulimit -s 8192
LEAN=$1
export LEAN_PATH=Init=../../library/Init:Test=.
export LEAN_PATH=Init=../../src/Init:Test=.
if [ $# -ne 3 ]; then
INTERACTIVE=no
else

2
tests/lean/trust0/test_single.sh
View file

@ -5,7 +5,7 @@ if [ $# -lt 2 ]; then
fi
ulimit -s 8192
LEAN=$1
export LEAN_PATH=Init=../../../library/Init:Test=.
export LEAN_PATH=Init=../../../src/Init:Test=.
f=$2
shift 2
echo "-- testing $f"