From d636b34c1c667b0b96bfda9933440caaf6f9cc54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 May 2015 11:48:07 -0700 Subject: [PATCH] fix(tests/lean): make sure tests do not fail when compiling Lean with cmake option "-DIGNORE_SORRY=ON" --- tests/lean/531.hlean.expected.out | 6 ------ tests/lean/quot_bug.lean.expected.out | 1 - tests/lean/test_single.sh | 2 +- 3 files changed, 1 insertion(+), 8 deletions(-) diff --git a/tests/lean/531.hlean.expected.out b/tests/lean/531.hlean.expected.out index 59c5ad3cd..c70917a50 100644 --- a/tests/lean/531.hlean.expected.out +++ b/tests/lean/531.hlean.expected.out @@ -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 diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out index 13e60ba80..d925317ac 100644 --- a/tests/lean/quot_bug.lean.expected.out +++ b/tests/lean/quot_bug.lean.expected.out @@ -1,2 +1 @@ λ (x : A), f x -quot_bug.lean:8:59: warning: using 'sorry' diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh index 91e7c0322..8bac28fed 100755 --- a/tests/lean/test_single.sh +++ b/tests/lean/test_single.sh @@ -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