test(tests/lean/interactive): add old 'interactive' tests

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

tests/lean/interactive/t1.input

@@ -1,8 +0,0 @@
-print "hello"
-print "block1"
-#ACK
-print "block2"
--- comment
-print "block2b"
-#ACK
-print "block3"

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

@@ -1,5 +0,0 @@
-hello
-block1
-block2
-block2b
-block3

tests/lean/interactive/t2.input

@@ -1,4 +0,0 @@
-print "hello"
-#ACK
-print pr
-#ACK

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

@@ -1,2 +0,0 @@
-hello
-[stdin]:2:7: error: invalid print command

tests/lean/interactive/t3.input

@@ -1,7 +0,0 @@
-section
-   parameter A : Type
-   check A
-#ACK
-   check A
-end
-print "done"

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

@@ -1,3 +0,0 @@
-A : Type
-A : Type
-done

tests/lean/interactive/t4.input

@@ -1,26 +0,0 @@
-variable N : Type.{1}
-print "block 1"
-#SNAPSHOT
-variable f : N -> N
-variable g : N -> N
-#SNAPSHOT
-check N
-print "before restore"
-#RESTORE 3
--- Restore will remove all lines >= 3
--- You will be able to reuse the first snapshot
-print "after restore"
-print "only once"
-check N
-variable f : N -> N
-#RESTORE 6
--- Restore will remove all lines >= 6
-print "after second restore"
-#RESTART
-variable N : Type.{1}
-print "block 1"
--- Restore will remove all lines >= 3
--- You will be able to reuse the first snapshot
-print "after restore"
-check N
-print "done"

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

@@ -1,11 +0,0 @@
-block 1
-N : Type
-before restore
-after restore
-only once
-N : Type
-after restore
-after second restore
-after restore
-N : Type
-done