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

20 files changed, 393 insertions, 1 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 4e94f29a0..a77b9fffd 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -75,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   interactive micromega $(COMPLEXITY) modules
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide
 
 #######################################################################
 # Phony targets
@@ -131,6 +131,7 @@ summary:
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
+	  $(call summary_dir, "IDE tests", ide); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -423,3 +424,22 @@ misc/universes.log: misc/universes/all_stdlib.v
 
 misc/universes/all_stdlib.v:
 	cd .. && $(MAKE) test-suite/$@
+
+
+# IDE : some tests of backtracking for coqtop -ideslave
+
+ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
+
+%.fake.log : %.fake
+	@echo "TEST      $<"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(BIN)fake_ide $(BIN)coqtop < $< 2>&1; \
+	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	  fi; \
+	} > "$@"
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.