michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-01 21:25:52 -08:00
parent 36cfb7fac0
commit 10357f3f53
4 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/nonexhaustive.lean.expected.out
View file

@ -1,4 +1,3 @@
nonexhaustive.lean:2:0: warning: imported file uses 'sorry'
nonexhaustive.lean:6:11: error: invalid non-exhaustive set of recursive equations, left-hand-side(s) after elaboration:
@foo 0 (@nil A)

4
tests/lean/test.sh
View file

@ -15,7 +15,9 @@ fi
NUM_ERRORS=0
for f in *.lean; do
echo "-- testing $f"
$LEAN -t config.lean $f &> $f.produced.out
$LEAN -t config.lean $f &> $f.produced.out.1
sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
rm -f $f.produced.out.1
if test -f $f.expected.out; then
if diff -I "executing external script" $f.produced.out $f.expected.out; then
echo "-- checked"

4
tests/lean/test_single.sh
View file

@ -13,7 +13,9 @@ else
fi
f=$2
echo "-- testing $f"
$LEAN config.lean $f &> $f.produced.out
$LEAN config.lean $f &> $f.produced.out.1
sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
rm -f $f.produced.out.1
if test -f $f.expected.out; then
if diff --ignore-all-space -I "executing external script" $f.produced.out $f.expected.out; then
echo "-- checked"

1
tests/lean/unzip_error.lean.expected.out
View file

@ -1,3 +1,2 @@
unzip_error.lean:2:0: warning: imported file uses 'sorry'
unzip_error.lean:9:2: error: invalid recursive equation, left-hand-side contains meta-variable (possible solution: provide implicit parameters occurring in left-hand-side explicitly)
match (@mk (vector A ?M_1) (vector B ?M_1) va vb)