From fb2ac90cf4717568b7f404c7e3be8bcb8cb68cfe Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 5 Jan 2017 08:09:00 +0100
Subject: [PATCH] chore(tests/lean/fail): add tests that check for positive
 exit values

---
 src/shell/CMakeLists.txt          | 11 +++++++++++
 tests/lean/fail/failed_lemma.lean |  1 +
 tests/lean/fail/parser_error.lean |  1 +
 tests/lean/fail/test_single.sh    | 16 ++++++++++++++++
 4 files changed, 29 insertions(+)
 create mode 100644 tests/lean/fail/failed_lemma.lean
 create mode 100644 tests/lean/fail/parser_error.lean
 create mode 100644 tests/lean/fail/test_single.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 3b9d7f4657..6d783d39c4 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -125,6 +125,17 @@ FOREACH(T ${LEANRUNTESTS})
   endif()
 ENDFOREACH(T)
 
+# LEAN FAIL TESTS
+file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/fail/*.lean")
+FOREACH(T ${LEANRUNTESTS})
+    if(NOT T MATCHES "\\.#")
+        GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+        add_test(NAME "leanfailtest_${T_NAME}"
+                WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/fail"
+                COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
+    endif()
+ENDFOREACH(T)
+
 # SMT2 RUN TESTS
 # file(GLOB SMT2RUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/smt2/run/*.smt2")
 # FOREACH(T ${SMT2RUNTESTS})
diff --git a/tests/lean/fail/failed_lemma.lean b/tests/lean/fail/failed_lemma.lean
new file mode 100644
index 0000000000..d4135a6e4b
--- /dev/null
+++ b/tests/lean/fail/failed_lemma.lean
@@ -0,0 +1 @@
+lemma wrong : false := by tactic.failed
diff --git a/tests/lean/fail/parser_error.lean b/tests/lean/fail/parser_error.lean
new file mode 100644
index 0000000000..d1f45b399c
--- /dev/null
+++ b/tests/lean/fail/parser_error.lean
@@ -0,0 +1 @@
+lemma
diff --git a/tests/lean/fail/test_single.sh b/tests/lean/fail/test_single.sh
new file mode 100644
index 0000000000..fcac9a78ae
--- /dev/null
+++ b/tests/lean/fail/test_single.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+if [ $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file]"
+    exit 1
+fi
+ulimit -s 8192
+LEAN=$1
+export LEAN_PATH=../../../library:.
+f=$2
+echo "-- testing $f"
+if "$LEAN" -j 0 "$f"; then
+   echo "failed $f"
+   exit 1
+else
+   echo "-- checked"
+fi