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

fix(tests/lean): make sure tests do not fail when compiling Lean with cmake option "-DIGNORE_SORRY=ON"

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-11 11:48:07 -07:00
parent 396f77aa68
commit d636b34c1c
3 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/531.hlean.expected.out
View file

@ -1,7 +1 @@
531.hlean:49:2: warning: using 'sorry'
531.hlean:55:72: warning: using 'sorry'
531.hlean:55:92: warning: using 'sorry'
531.hlean:57:2: warning: using 'sorry'
531.hlean:133:12: warning: using 'sorry'
531.hlean:148:6: warning: using 'sorry'
531.hlean:151:0: warning: using 'exit' to interrupt Lean

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

@ -1,2 +1 @@
λ (x : A), f x
quot_bug.lean:8:59: warning: using 'sorry'

2
tests/lean/test_single.sh
View file

@ -22,7 +22,7 @@ fi
echo "-- testing $f"
"$LEAN" $CONFIG "$f" &> "$f.produced.out.1"
sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" > "$f.produced.out"
sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" | sed "/warning: using 'sorry'/d" > "$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