test(tests/lean/interactive): add --server test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/interactive/in4.input

@@ -0,0 +1,14 @@
+VISIT simple3.lean
+WAIT
+INFO 9
+REMOVE 9
+REMOVE 8
+ECHO AFTER REMOVE 8&9
+INFO 9
+INFO 8
+INSERT 8
+theorem tst {A : Type} (a b : A) : tst.foo a b = a :=
+INSERT 9
+rfl
+WAIT
+INFO 9

tests/lean/interactive/in4.input.expected.out

@@ -0,0 +1,18 @@
+-- BEGININFO
+-- TYPE|9|0
+∀ (a : A), eq a a
+-- ACK
+-- SYMBOL|9|0
+rfl
+-- ACK
+-- ENDINFO
+-- AFTER REMOVE 8&9
+-- BEGININFO
+-- NAY
+-- ENDINFO
+-- BEGININFO
+-- NAY
+-- ENDINFO
+-- BEGININFO
+-- NAY
+-- ENDINFO

tests/lean/interactive/simple3.lean

@@ -0,0 +1,9 @@
+import logic
+
+namespace tst
+definition foo {A B : Type} (a : A) (b : B) := a
+definition boo {A : Type} (a : A) := foo a a
+end tst
+
+theorem tst {A : Type} (a b : A) : tst.foo a b = a :=
+rfl