test(tests/lean/interactive): add more tests for lean server

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

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

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

tests/lean/interactive/options_cmd.trace

@@ -0,0 +1 @@
+OPTIONS