From 9d1e312c12503ed0da70d7724e52cd3a3ee261d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 20:10:53 -0800
Subject: [PATCH] test(tests/lean/extra): add extra tests for 'print' command

---
 src/shell/CMakeLists.txt          |  3 +++
 tests/lean/extra/print_tests.lean |  7 +++++++
 tests/lean/extra/test_single.sh   | 16 ++++++++++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 tests/lean/extra/print_tests.lean
 create mode 100755 tests/lean/extra/test_single.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 0f401e7c2b..7e87e0903c 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -37,6 +37,9 @@ add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LE
 add_test(NAME "lean_eqn_macro"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./test_eqn_macro.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "lean_print_notation"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_tests.lean")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/extra/print_tests.lean b/tests/lean/extra/print_tests.lean
new file mode 100644
index 0000000000..354e1cf511
--- /dev/null
+++ b/tests/lean/extra/print_tests.lean
@@ -0,0 +1,7 @@
+print notation
+
+print notation ∧ ∨
+
+print notation if
+
+print notation mod
diff --git a/tests/lean/extra/test_single.sh b/tests/lean/extra/test_single.sh
new file mode 100755
index 0000000000..1339f11d60
--- /dev/null
+++ b/tests/lean/extra/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 $f; then
+   echo "-- checked"
+else
+   echo "failed $f"
+   exit 1
+fi