From 02988615cb53fac19cf640e47521dc9285c7b2f6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Sep 2011 16:47:29 +0000 Subject: 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 --- test-suite/ide/undo001.fake | 10 ++++++++++ test-suite/ide/undo002.fake | 10 ++++++++++ test-suite/ide/undo003.fake | 8 ++++++++ test-suite/ide/undo004.fake | 14 ++++++++++++++ test-suite/ide/undo005.fake | 15 +++++++++++++++ test-suite/ide/undo006.fake | 14 ++++++++++++++ test-suite/ide/undo007.fake | 17 +++++++++++++++++ test-suite/ide/undo008.fake | 18 ++++++++++++++++++ test-suite/ide/undo009.fake | 20 ++++++++++++++++++++ test-suite/ide/undo010.fake | 28 ++++++++++++++++++++++++++++ test-suite/ide/undo011.fake | 32 ++++++++++++++++++++++++++++++++ test-suite/ide/undo012.fake | 26 ++++++++++++++++++++++++++ test-suite/ide/undo013.fake | 31 +++++++++++++++++++++++++++++++ test-suite/ide/undo014.fake | 26 ++++++++++++++++++++++++++ test-suite/ide/undo015.fake | 29 +++++++++++++++++++++++++++++ test-suite/ide/undo016.fake | 34 ++++++++++++++++++++++++++++++++++ test-suite/ide/undo017.fake | 13 +++++++++++++ test-suite/ide/undo018.fake | 13 +++++++++++++ test-suite/ide/undo019.fake | 14 ++++++++++++++ 19 files changed, 372 insertions(+) create mode 100644 test-suite/ide/undo001.fake create mode 100644 test-suite/ide/undo002.fake create mode 100644 test-suite/ide/undo003.fake create mode 100644 test-suite/ide/undo004.fake create mode 100644 test-suite/ide/undo005.fake create mode 100644 test-suite/ide/undo006.fake create mode 100644 test-suite/ide/undo007.fake create mode 100644 test-suite/ide/undo008.fake create mode 100644 test-suite/ide/undo009.fake create mode 100644 test-suite/ide/undo010.fake create mode 100644 test-suite/ide/undo011.fake create mode 100644 test-suite/ide/undo012.fake create mode 100644 test-suite/ide/undo013.fake create mode 100644 test-suite/ide/undo014.fake create mode 100644 test-suite/ide/undo015.fake create mode 100644 test-suite/ide/undo016.fake create mode 100644 test-suite/ide/undo017.fake create mode 100644 test-suite/ide/undo018.fake create mode 100644 test-suite/ide/undo019.fake (limited to 'test-suite/ide') 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 +# +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. +# +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 +# +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 +# +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 +# +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 +# +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 +# +INTERP Definition o := O. +INTERP Ltac h x := x. +INTERP assert True by trivial. +INTERP Focus. +INTERP Definition p := O. +# +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 +# +INTERP suppose B. +# +REWIND 2 +# +INTERP thus thesis by H1. +INTERP suppose B. +# +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" +# +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +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/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 +# +INTERP destruct H. +# +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 +# +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +# +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" +# +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. +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 +# +INTERP End M. +# +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 +# +INTERP End M. +# +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 +# +INTERP } +# +INTERP Qed. -- cgit v1.2.3