From f04e462bf3f643996b4c834f6f0cf7dcd90804d5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Jan 2015 16:30:07 -0800
Subject: [PATCH] test(tests/lean/interactive): add more tests for lean server

---
 src/shell/CMakeLists.txt                      |  2 +
 tests/lean/interactive/commands.input         | 22 +++++++++
 .../interactive/commands.input.expected.out   | 45 +++++++++++++++++++
 tests/lean/interactive/options_cmd.trace      |  1 +
 4 files changed, 70 insertions(+)
 create mode 100644 tests/lean/interactive/commands.input
 create mode 100644 tests/lean/interactive/commands.input.expected.out
 create mode 100644 tests/lean/interactive/options_cmd.trace

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index f2fdcd5742..d5ae73f2c2 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -31,6 +31,8 @@ add_test(lean_luahook2 ${CMAKE_CURRENT_BINARY_DIR}/lean -k 100 "${LEAN_SOURCE_DI
 add_test(lean_unknown_option bash ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
 add_test(lean_unknown_file1 bash ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
 add_test(lean_unknown_file2 bash ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua")
+add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/consume_args.input")
+add_test(lean_server_trace ${CMAKE_CURRENT_BINARY_DIR}/lean --server-trace "${LEAN_SOURCE_DIR}/../tests/lean/interactive/options_cmd.trace")
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
diff --git a/tests/lean/interactive/commands.input b/tests/lean/interactive/commands.input
new file mode 100644
index 0000000000..7b6ed446bf
--- /dev/null
+++ b/tests/lean/interactive/commands.input
@@ -0,0 +1,22 @@
+VISIT consume_args.lean
+SYNC 9
+import logic data.nat.basic
+open nat eq.ops
+
+definition a := true
+
+theorem tst (a b c : nat) : a + b + c = a + c + b :=
+calc a + b + c = a + (b + c) : _
+         ...   = a + (c + b) : {!add.comm}
+         ...   = a + c + b   : (!add.assoc)⁻¹
+WAIT
+CLEAR_CACHE
+WAIT 100
+INFO 4
+WAIT
+INFO 4
+FINDG 7 31
++assoc -symm
+WAIT
+SLEEP 20
+SHOW
\ No newline at end of file
diff --git a/tests/lean/interactive/commands.input.expected.out b/tests/lean/interactive/commands.input.expected.out
new file mode 100644
index 0000000000..c871aa7db4
--- /dev/null
+++ b/tests/lean/interactive/commands.input.expected.out
@@ -0,0 +1,45 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- INTERRUPTED
+-- ENDWAIT
+-- BEGININFO NAY
+-- TYPE|4|13
+Type₁
+-- ACK
+-- TYPE|4|16
+Prop
+-- ACK
+-- IDENTIFIER|4|16
+true
+-- ACK
+-- ENDINFO
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|4|13
+Type₁
+-- ACK
+-- TYPE|4|16
+Prop
+-- ACK
+-- IDENTIFIER|4|16
+true
+-- ACK
+-- ENDINFO
+-- BEGINFINDG
+add.assoc|∀ (n m k : ℕ), n + m + k = n + (m + k)
+-- ENDFINDG
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINSHOW
+import logic data.nat.basic
+open nat eq.ops
+
+definition a := true
+
+theorem tst (a b c : nat) : a + b + c = a + c + b :=
+calc a + b + c = a + (b + c) : _
+         ...   = a + (c + b) : {!add.comm}
+         ...   = a + c + b   : (!add.assoc)⁻¹
+-- ENDSHOW
diff --git a/tests/lean/interactive/options_cmd.trace b/tests/lean/interactive/options_cmd.trace
new file mode 100644
index 0000000000..b2ef5b8916
--- /dev/null
+++ b/tests/lean/interactive/options_cmd.trace
@@ -0,0 +1 @@
+OPTIONS