From a173b7f6e631f83b36131237ced090c72a104a98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Aug 2014 14:57:08 -0700
Subject: [PATCH] test(tests/lean/interactive): add old 'interactive' tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/interactive/t1.input              |  8 ------
 tests/lean/interactive/t1.input.expected.out |  5 ----
 tests/lean/interactive/t2.input              |  4 ---
 tests/lean/interactive/t2.input.expected.out |  2 --
 tests/lean/interactive/t3.input              |  7 ------
 tests/lean/interactive/t3.input.expected.out |  3 ---
 tests/lean/interactive/t4.input              | 26 --------------------
 tests/lean/interactive/t4.input.expected.out | 11 ---------
 8 files changed, 66 deletions(-)
 delete mode 100644 tests/lean/interactive/t1.input
 delete mode 100644 tests/lean/interactive/t1.input.expected.out
 delete mode 100644 tests/lean/interactive/t2.input
 delete mode 100644 tests/lean/interactive/t2.input.expected.out
 delete mode 100644 tests/lean/interactive/t3.input
 delete mode 100644 tests/lean/interactive/t3.input.expected.out
 delete mode 100644 tests/lean/interactive/t4.input
 delete mode 100644 tests/lean/interactive/t4.input.expected.out

diff --git a/tests/lean/interactive/t1.input b/tests/lean/interactive/t1.input
deleted file mode 100644
index dc5057870a..0000000000
--- a/tests/lean/interactive/t1.input
+++ /dev/null
@@ -1,8 +0,0 @@
-print "hello"
-print "block1"
-#ACK
-print "block2"
--- comment
-print "block2b"
-#ACK
-print "block3"
diff --git a/tests/lean/interactive/t1.input.expected.out b/tests/lean/interactive/t1.input.expected.out
deleted file mode 100644
index 73de1770c9..0000000000
--- a/tests/lean/interactive/t1.input.expected.out
+++ /dev/null
@@ -1,5 +0,0 @@
-hello
-block1
-block2
-block2b
-block3
diff --git a/tests/lean/interactive/t2.input b/tests/lean/interactive/t2.input
deleted file mode 100644
index c1aecf5091..0000000000
--- a/tests/lean/interactive/t2.input
+++ /dev/null
@@ -1,4 +0,0 @@
-print "hello"
-#ACK
-print pr
-#ACK
diff --git a/tests/lean/interactive/t2.input.expected.out b/tests/lean/interactive/t2.input.expected.out
deleted file mode 100644
index 5550847553..0000000000
--- a/tests/lean/interactive/t2.input.expected.out
+++ /dev/null
@@ -1,2 +0,0 @@
-hello
-[stdin]:2:7: error: invalid print command
diff --git a/tests/lean/interactive/t3.input b/tests/lean/interactive/t3.input
deleted file mode 100644
index 5357f91386..0000000000
--- a/tests/lean/interactive/t3.input
+++ /dev/null
@@ -1,7 +0,0 @@
-section
-   parameter A : Type
-   check A
-#ACK
-   check A
-end
-print "done"
\ No newline at end of file
diff --git a/tests/lean/interactive/t3.input.expected.out b/tests/lean/interactive/t3.input.expected.out
deleted file mode 100644
index ec8db88d06..0000000000
--- a/tests/lean/interactive/t3.input.expected.out
+++ /dev/null
@@ -1,3 +0,0 @@
-A : Type
-A : Type
-done
diff --git a/tests/lean/interactive/t4.input b/tests/lean/interactive/t4.input
deleted file mode 100644
index 0a7dbea799..0000000000
--- a/tests/lean/interactive/t4.input
+++ /dev/null
@@ -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"
\ No newline at end of file
diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out
deleted file mode 100644
index f9fb8ec8a5..0000000000
--- a/tests/lean/interactive/t4.input.expected.out
+++ /dev/null
@@ -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