fake_ide: a short program to mimic an ide talking to coqtop -ideslave

  This way, we can test each night that coqtop -ideslave handles
  correctly some specific sequences of API calls.
  For the moment, we add a few tests of the backtracking.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 372 insertions, 0 deletions

diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
new file mode 100644
index 000000000..9e54f4f08
--- /dev/null
+++ b/test-suite/ide/undo001.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 1 between two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 1
+INTERPRAW Check foo.
+INTERPRAW Fail Check bar.
\ No newline at end of file
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
new file mode 100644
index 000000000..36a0e8982
--- /dev/null
+++ b/test-suite/ide/undo002.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 2 before two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 2
+INTERPRAW Fail Check foo.
+INTERPRAW Fail Check bar.
\ No newline at end of file
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
new file mode 100644
index 000000000..4c72e8dc7
--- /dev/null
+++ b/test-suite/ide/undo003.fake
@@ -0,0 +1,8 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 0 should be a no-op
+#
+INTERP Definition foo := 0.
+REWIND 0
+INTERPRAW Check foo.
diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
new file mode 100644
index 000000000..c2ddfb8cb
--- /dev/null
+++ b/test-suite/ide/undo004.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as first step
+#
+INTERP Theorem a : O=O.
+INTERP Ltac f x := x.
+REWIND 1
+# <replay>
+INTERP Ltac f x := x.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
new file mode 100644
index 000000000..525b9f2a6
--- /dev/null
+++ b/test-suite/ide/undo005.fake
@@ -0,0 +1,15 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as non-first step
+#
+INTERP Theorem b : O=O.
+INTERP assert True by trivial.
+INTERP Ltac g x := x.
+# <replay>
+REWIND 1
+# <\replay>
+INTERP Ltac g x := x.
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
new file mode 100644
index 000000000..ed88bef51
--- /dev/null
+++ b/test-suite/ide/undo006.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# Was bugged in 8.1
+#
+INTERP Theorem c : O=O.
+INTERP Inductive T : Type := I.
+REWIND 1
+# <replay>
+INTERP Inductive T : Type := I.
+# <\replay>
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
new file mode 100644
index 000000000..3b2ca2b6b
--- /dev/null
+++ b/test-suite/ide/undo007.fake
@@ -0,0 +1,17 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# new in 8.2
+#
+INTERP Theorem d : O=O.
+INTERP Definition e := O.
+INTERP Definition f := O.
+REWIND 1
+# <replay>
+INTERP Definition f := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check e.
\ No newline at end of file
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
new file mode 100644
index 000000000..799dc1ac1
--- /dev/null
+++ b/test-suite/ide/undo008.fake
@@ -0,0 +1,18 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as non-first step
+# new in 8.2
+#
+INTERP Theorem h : O=O.
+INTERP assert True by trivial.
+INTERP Definition i := O.
+INTERP Definition j := O.
+REWIND 1
+# <replay>
+INTERP Definition j := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check i.
\ No newline at end of file
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
new file mode 100644
index 000000000..47c77d23d
--- /dev/null
+++ b/test-suite/ide/undo009.fake
@@ -0,0 +1,20 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps
+# new in 8.2 *)
+#
+INTERP Theorem k : O=O.
+INTERP assert True by trivial.
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+REWIND 3
+# <replay>
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
new file mode 100644
index 000000000..4fe9df986
--- /dev/null
+++ b/test-suite/ide/undo010.fake
@@ -0,0 +1,28 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps and commands *)
+# new in 8.2 *)
+#
+INTERP Theorem n : O=O.
+INTERP assert True by trivial.
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+# <replay>
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+# </replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
new file mode 100644
index 000000000..cc85a764b
--- /dev/null
+++ b/test-suite/ide/undo011.fake
@@ -0,0 +1,32 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Bug 2082
+# Broken due to proof engine rewriting
+#
+INTERP Variable A : Prop.
+INTERP Variable B : Prop.
+INTERP Axiom OR : A \/ B.
+INTERP Lemma MyLemma2 : True.
+INTERP proof.
+INTERP per cases of (A \/ B) by OR.
+INTERP suppose A.
+INTERP     then (1 = 1).
+INTERP     then H1 : thesis.
+INTERP     thus thesis by H1.
+INTERP suppose B.
+REWIND 1
+# <replay>
+INTERP suppose B.
+# </replay>
+REWIND 2
+# <replay>
+INTERP     thus thesis by H1.
+INTERP suppose B.
+# </replay>
+INTERP    then (1 = 1).
+INTERP    then H2 : thesis.
+INTERP    thus thesis by H2.
+INTERP end cases.
+INTERP end proof.
+INTERP Qed.
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
new file mode 100644
index 000000000..f9b29ca18
--- /dev/null
+++ b/test-suite/ide/undo012.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# First, undoing the whole
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+REWIND 1
+# We should now be just before aa, without opened proofs
+INTERPRAW Fail idtac.
+INTERPRAW Fail Check aa.
+INTERPRAW Fail Check bb.
+INTERPRAW Fail Check cc.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
new file mode 100644
index 000000000..def2da59e
--- /dev/null
+++ b/test-suite/ide/undo013.fake
@@ -0,0 +1,31 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Second, trigger the full undo of an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+REWIND 2
+# We should now be just before "Lemma cc"
+# <replay>
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+# </replay>
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
\ No newline at end of file
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
new file mode 100644
index 000000000..60897c652
--- /dev/null
+++ b/test-suite/ide/undo014.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Third, undo inside an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 1
+# <replay>
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
\ No newline at end of file
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
new file mode 100644
index 000000000..2bf391051
--- /dev/null
+++ b/test-suite/ide/undo015.fake
@@ -0,0 +1,29 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fourth, undo from an inner proof to a above proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 4
+# <replay>
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
\ No newline at end of file
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
new file mode 100644
index 000000000..bbc4c578c
--- /dev/null
+++ b/test-suite/ide/undo016.fake
@@ -0,0 +1,34 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fifth, undo from an inner proof to a previous inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 6
+# We should be just before "Lemma bb"
+# <replay>
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
\ No newline at end of file
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
new file mode 100644
index 000000000..e5baf6ca6
--- /dev/null
+++ b/test-suite/ide/undo017.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside modules
+#
+INTERP Module M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check M.x.
\ No newline at end of file
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
new file mode 100644
index 000000000..42e64218e
--- /dev/null
+++ b/test-suite/ide/undo018.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside section
+#
+INTERP Section M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check x.
\ No newline at end of file
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
new file mode 100644
index 000000000..70e70d7e4
--- /dev/null
+++ b/test-suite/ide/undo019.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing a focused subproof
+#
+INTERP Goal True.
+INTERP {
+INTERP exact I.
+INTERP }
+REWIND 1
+# <replay>
+INTERP }
+# </replay>
+INTERP Qed.