From 34654ad06bf08d6969e09d5167360e970261bbb1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 16:56:20 -0800
Subject: [PATCH] feat(tests/lean/interactive): add interactive mode test
 script

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp                 |  9 ++--
 src/shell/CMakeLists.txt                      | 18 +++++--
 tests/lean/interactive/config.lean            |  3 ++
 .../lean/interactive/config.lean.expected.out |  5 ++
 tests/lean/interactive/t1.lean                | 12 +++++
 tests/lean/interactive/t1.lean.expected.out   | 35 ++++++++++++++
 tests/lean/interactive/test.sh                | 48 +++++++++++++++++++
 tests/lean/interactive/test_single.sh         | 42 ++++++++++++++++
 8 files changed, 164 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/interactive/config.lean
 create mode 100644 tests/lean/interactive/config.lean.expected.out
 create mode 100644 tests/lean/interactive/t1.lean
 create mode 100644 tests/lean/interactive/t1.lean.expected.out
 create mode 100755 tests/lean/interactive/test.sh
 create mode 100755 tests/lean/interactive/test_single.sh

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index bc3e70adc4..ecd4863b2e 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1255,7 +1255,7 @@ class parser::imp {
                 return;
             }
         }
-        throw tactic_cmd_error("no more states to backtrack", p, s);
+        throw tactic_cmd_error("failed to backtrack", p, s);
     }
 
     void tactic_apply(proof_state_seq_stack & stack, proof_state & s) {
@@ -1308,7 +1308,7 @@ class parser::imp {
             }
             return pr;
         } else {
-            throw tactic_cmd_error("failed to synthesize proof object using tactics", p, s);
+            throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s);
         }
     }
 
@@ -1356,11 +1356,12 @@ class parser::imp {
                         } else if (id == g_back) {
                             tactic_backtrack(stack, s);
                         } else if (id == g_done) {
-                            done = true;
                             pr = tactic_done(s);
+                            if (pr)
+                                done = true;
                         } else {
                             next();
-                            throw tactic_cmd_error(sstream() << "invalid tactical proof, unknown command '" << id << "'", p, s);
+                            throw tactic_cmd_error(sstream() << "invalid tactic command '" << id << "'", p, s);
                         }
                         break;
                     default:
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 50ba31242f..aafe5179f2 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -8,7 +8,7 @@ add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../exampl
 add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean")
 add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
 
-# LEANTESTS
+# LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
 FOREACH(T ${LEANTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@@ -17,7 +17,16 @@ FOREACH(T ${LEANTESTS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
 
-# LEANSLOWTESTS
+# LEAN INTERACTIVE TESTS
+file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
+FOREACH(T ${LEANINTERACTIVETESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leaninteractivetest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+ENDFOREACH(T)
+
+# LEAN SLOW TESTS
 file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
 FOREACH(T ${LEANSLOWTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@@ -26,7 +35,7 @@ FOREACH(T ${LEANSLOWTESTS})
            COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
 
-# LEANLUATESTS
+# LEAN LUA TESTS
 file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
 FOREACH(T ${LEANLUATESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@@ -35,7 +44,7 @@ FOREACH(T ${LEANLUATESTS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
 
-# LEANLUADOCS
+# LEAN LUA DOCS
 file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md")
 FOREACH(T ${LEANLUADOCS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@@ -44,6 +53,7 @@ FOREACH(T ${LEANLUADOCS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
 
+# LEAN LUA THREAD TESTS
 if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
   if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${THREAD_SAFE} MATCHES "ON"))
     file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua")
diff --git a/tests/lean/interactive/config.lean b/tests/lean/interactive/config.lean
new file mode 100644
index 0000000000..905e753401
--- /dev/null
+++ b/tests/lean/interactive/config.lean
@@ -0,0 +1,3 @@
+(* Set default configuration for tests *)
+Set pp::colors  false
+Set pp::unicode true
diff --git a/tests/lean/interactive/config.lean.expected.out b/tests/lean/interactive/config.lean.expected.out
new file mode 100644
index 0000000000..0efee9e48a
--- /dev/null
+++ b/tests/lean/interactive/config.lean.expected.out
@@ -0,0 +1,5 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+  Set: pp::colors
+  Set: pp::unicode
diff --git a/tests/lean/interactive/t1.lean b/tests/lean/interactive/t1.lean
new file mode 100644
index 0000000000..941e49b9fd
--- /dev/null
+++ b/tests/lean/interactive/t1.lean
@@ -0,0 +1,12 @@
+Theorem T2 (a b : Bool) : a => b => a /\ b.
+done.
+done.
+apply imp_tactic.
+apply imp_tactic2.
+foo.
+apply imp_tactic.
+apply imp_tactic.
+apply conj_tactic.
+back.
+apply assumption_tactic.
+done.
diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out
new file mode 100644
index 0000000000..bc063c9b2d
--- /dev/null
+++ b/tests/lean/interactive/t1.lean.expected.out
@@ -0,0 +1,35 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+Proof state:
+a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+## Error (line: 5, pos: 0) invalid 'done' command, proof cannot be produced from this state
+Proof state:
+a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+## Error (line: 6, pos: 0) invalid 'done' command, proof cannot be produced from this state
+Proof state:
+a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+## Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Error (line: 8, pos: 0) unknown tactic 'imp_tactic2'
+Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Error (line: 9, pos: 0) invalid tactic command 'foo'
+Proof state:
+H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
+## Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
+## Error (line: 11, pos: 0) tactic failed
+Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
+## Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a
+H::1 : b, H : a, a : Bool, b : Bool ⊢ b
+## Error (line: 13, pos: 0) failed to backtrack
+Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a
+H::1 : b, H : a, a : Bool, b : Bool ⊢ b
+## Proof state:
+no goals
+##   Proved: T2
+# 
\ No newline at end of file
diff --git a/tests/lean/interactive/test.sh b/tests/lean/interactive/test.sh
new file mode 100755
index 0000000000..57fd79098a
--- /dev/null
+++ b/tests/lean/interactive/test.sh
@@ -0,0 +1,48 @@
+#!/bin/bash
+if [ $# -ne 2 -a $# -ne 1 ]; then
+    echo "Usage: test.sh [lean-executable-path] [yes/no]?"
+    exit 1
+fi
+ulimit -s unlimited
+LEAN=$1
+if [ $# -ne 2 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$2
+fi
+NUM_ERRORS=0
+for f in `ls *.lean`; do
+    echo "-- testing $f"
+    cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
+    if test -f $f.expected.out; then
+        if diff $f.produced.out $f.expected.out; then
+            echo "-- checked"
+        else
+            echo "ERROR: file $f.produced.out does not match $f.expected.out"
+            NUM_ERRORS=$(($NUM_ERRORS+1))
+            if [ $INTERACTIVE == "yes" ]; then
+                meld $f.produced.out $f.expected.out
+                if diff $f.produced.out $f.expected.out; then
+                    echo "-- mismath was fixed"
+                fi
+            fi
+        fi
+    else
+        echo "ERROR: file $f.expected.out does not exist"
+        NUM_ERRORS=$(($NUM_ERRORS+1))
+        if [ $INTERACTIVE == "yes" ]; then
+            read -p "copy $f.produced.out (y/n)? "
+            if [ $REPLY == "y" ]; then
+                cp $f.produced.out $f.expected.out
+                echo "-- copied $f.produced.out --> $f.expected.out"
+            fi
+        fi
+    fi
+done
+if [ $NUM_ERRORS -gt 0 ]; then
+    echo "-- Number of errors: $NUM_ERRORS"
+    exit 1
+else
+    echo "-- Passed"
+    exit 0
+fi
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
new file mode 100755
index 0000000000..edd524dc65
--- /dev/null
+++ b/tests/lean/interactive/test_single.sh
@@ -0,0 +1,42 @@
+#!/bin/bash
+if [ $# -ne 3 -a $# -ne 2 ]; then
+    echo "Usage: test.sh [lean-executable-path] [file] [yes/no]?"
+    exit 1
+fi
+ulimit -s unlimited
+LEAN=$1
+if [ $# -ne 3 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$3
+fi
+f=$2
+echo "-- testing $f"
+cat config.lean $f | $LEAN --lean | tail -n +2 > $f.produced.out
+if test -f $f.expected.out; then
+    if diff $f.produced.out $f.expected.out; then
+        echo "-- checked"
+        exit 0
+    else
+        echo "ERROR: file $f.produced.out does not match $f.expected.out"
+        if [ $INTERACTIVE == "yes" ]; then
+            meld $f.produced.out $f.expected.out
+            if diff $f.produced.out $f.expected.out; then
+                echo "-- mismath was fixed"
+            fi
+        else
+            diff $f.produced.out $f.expected.out
+        fi
+        exit 1
+    fi
+else
+    echo "ERROR: file $f.expected.out does not exist"
+    if [ $INTERACTIVE == "yes" ]; then
+        read -p "copy $f.produced.out (y/n)? "
+        if [ $REPLY == "y" ]; then
+            cp $f.produced.out $f.expected.out
+            echo "-- copied $f.produced.out --> $f.expected.out"
+        fi
+    fi
+    exit 1
+fi