test(tests/lean/extra): add extra tests for 'print' command

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")

tests/lean/extra/print_tests.lean

@@ -0,0 +1,7 @@
+print notation
+
+print notation ∧ ∨
+
+print notation if
+
+print notation mod

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