diff options
Diffstat (limited to 'test-suite/ide')
31 files changed, 589 insertions, 0 deletions
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake new file mode 100644 index 0000000000..541fb798c0 --- /dev/null +++ b/test-suite/ide/blocking-futures.fake @@ -0,0 +1,17 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Extraction will force the future computation, assert it is blocking +# Example courtesy of Jonathan (jonikelee) +# +ADD { Require Coq.extraction.Extraction. } +ADD { Require Import List. } +ADD { Import ListNotations. } +ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. } +ADD { Proof. } +ADD { induction l. } +ADD { eexists; reflexivity. } +ADD { cbn; destruct IHl as [rl' H]; rewrite <-H; eexists; reflexivity. } +ADD { Qed. } +ADD { Extraction myrev. } +GOALS diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake new file mode 100644 index 0000000000..16b552f679 --- /dev/null +++ b/test-suite/ide/bug4246.fake @@ -0,0 +1,14 @@ +# first proof +ADD { Lemma a : True. } +ADD { Proof using. } +ADD here { trivial. } # first error +ADD { fail. } +ADD { Qed. } +WAIT +EDIT_AT here +# Fixing the proof +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Qed. } +JOIN diff --git a/test-suite/ide/bug4249.fake b/test-suite/ide/bug4249.fake new file mode 100644 index 0000000000..20afe0fb8d --- /dev/null +++ b/test-suite/ide/bug4249.fake @@ -0,0 +1,16 @@ +ADD { Lemma a : True. } +ADD here { Proof using. } +ADD { fail. } +ADD { trivial. } # first error +ADD { Qed. } +WAIT +EDIT_AT here +# Fixing the proof +ADD fix { trivial. } +ADD { Qed. } +WAIT +EDIT_AT fix +ADD { Qed. } +EDIT_AT fix +ADD { Qed. } +JOIN diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake new file mode 100644 index 0000000000..e2a2aa52a0 --- /dev/null +++ b/test-suite/ide/bug7088.fake @@ -0,0 +1,13 @@ +ADD { Arguments id T x : rename. } +ADD { Lemma foo : True. } +ADD here { Proof. } +ADD { exact 3. } +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Arguments id FOO BAR : rename. } +ADD { exact I. } +ADD { Qed. } +ADD { Arguments id T x : assert. } +JOIN + diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake new file mode 100644 index 0000000000..aa68fad39e --- /dev/null +++ b/test-suite/ide/debug_ltac.fake @@ -0,0 +1,2 @@ +FAILADD { Debug On. } +ADD { Set Debug On. } diff --git a/test-suite/ide/join-sync.fake b/test-suite/ide/join-sync.fake new file mode 100644 index 0000000000..236028ce46 --- /dev/null +++ b/test-suite/ide/join-sync.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency + async proofs off +# coq-prog-args: ("-async-proofs" "off" "-async-proofs-command-error-resilience" "on") +# + +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +WAIT +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT diff --git a/test-suite/ide/load.fake b/test-suite/ide/load.fake new file mode 100644 index 0000000000..f6a7ef4dcb --- /dev/null +++ b/test-suite/ide/load.fake @@ -0,0 +1,11 @@ +ADD revert { Load "output/load/Load_noproof.v". } +ADD { Load "output/load/Load_proof.v". } +ADD { Fail Load "output/load/Load_openproof.v". } +WAIT +QUERY { Check f. } +QUERY { Check u. } +EDIT_AT revert +QUERY { Check f. } +QUERY { Fail Check u. } +JOIN + diff --git a/test-suite/ide/reopen.fake b/test-suite/ide/reopen.fake new file mode 100644 index 0000000000..8166d0137e --- /dev/null +++ b/test-suite/ide/reopen.fake @@ -0,0 +1,21 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + interp error while fixing. +# the error should note make the GUI unfocus the currently focused proof. + +# first proof +ADD { Lemma a : True. } +ADD here { Proof using. } +ADD { fail. } +ADD { trivial. } # first error +ADD { Qed. } +WAIT +EDIT_AT here +# Fixing the proof +ADD fix { trivial. } +ADD { Qed. } +WAIT +EDIT_AT fix +ADD { Qed. } +JOIN diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake new file mode 100644 index 0000000000..2c4f13de86 --- /dev/null +++ b/test-suite/ide/reopen1.fake @@ -0,0 +1,22 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping outside the focused zone should signal an unfocus. + +# first proof +ADD here { Goal True. } +ADD here1 { Proof. } +ADD { Qed. } +WAIT +EDIT_AT here1 +EDIT_AT here +# fwd again +ADD here2 { Proof. } +ADD here3 { Qed. } +WAIT +EDIT_AT here2 +# Fixing the proof +ADD { Proof. } +ADD { trivial. } +ADD { Qed. } +JOIN diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake new file mode 100644 index 0000000000..552636157a --- /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 +# +ADD here { Definition foo := 0. } +ADD { Definition bar := 1. } +EDIT_AT here +QUERY { Check foo. } +QUERY { Fail Check bar. } diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake new file mode 100644 index 0000000000..5284c5d3a5 --- /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 +# +ADD { Definition foo := 0. } +ADD { Definition bar := 1. } +EDIT_AT initial +QUERY { Fail Check foo. } +QUERY { Fail Check bar. } diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake new file mode 100644 index 0000000000..9075762766 --- /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 +# +ADD here { Definition foo := 0. } +EDIT_AT here +QUERY { Check foo. } diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake new file mode 100644 index 0000000000..9029b03e24 --- /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 +# +ADD here { Theorem a : O=O. } +ADD { Ltac f x := x. } +EDIT_AT here +# <replay> +ADD { Ltac f x := x. } +# <\replay> +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake new file mode 100644 index 0000000000..7e31c0b05f --- /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 +# +ADD { Theorem b : O=O. } +ADD here { assert True by trivial. } +ADD { Ltac g x := x. } +# <replay> +EDIT_AT here +# <\replay> +ADD { Ltac g x := x. } +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake new file mode 100644 index 0000000000..cdfdee1b7a --- /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 +# +ADD here { Theorem c : O=O. } +ADD { Inductive T : Type := I. } +EDIT_AT here +# <replay> +ADD { Inductive T : Type := I. } +# <\replay> +ADD { trivial. } +ADD { Qed. } diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake new file mode 100644 index 0000000000..72cab7a30e --- /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 +# +ADD { Theorem h : O=O. } +ADD { assert True by trivial. } +ADD here { Definition i := O. } +ADD { Definition j := O. } +EDIT_AT here +# <replay> +ADD { Definition j := O. } +# <\replay> +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } +QUERY { Check i. } diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake new file mode 100644 index 0000000000..76f400ef06 --- /dev/null +++ b/test-suite/ide/undo009.fake @@ -0,0 +1,21 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, interleaved with proof steps +# new in 8.2 *) +# +ADD { Theorem k : O=O. } +ADD here { assert True by trivial. } +ADD { Definition l := O. } +ADD { assert True by trivial. } +ADD { Definition m := O. } +QUERY { Show. } +EDIT_AT here +# <replay> +ADD { Definition l := O. } +ADD { assert True by trivial. } +ADD { Definition m := O. } +# <\replay> +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake new file mode 100644 index 0000000000..524416c32b --- /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 *) +# +ADD { Theorem n : O=O. } +ADD s2 { assert True by trivial. } +ADD s3 { Definition o := O. } +ADD s4 { Ltac h x := x. } +ADD s5 { assert True by trivial. } +ADD s6 { Focus. } +ADD { Definition p := O. } +EDIT_AT s6 +EDIT_AT s5 +EDIT_AT s4 +EDIT_AT s3 +EDIT_AT s2 +# <replay> +ADD { Definition o := O. } +ADD { Ltac h x := x. } +ADD { assert True by trivial. } +ADD { Focus. } +ADD { Definition p := O. } +# </replay> +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake new file mode 100644 index 0000000000..c95df1b11c --- /dev/null +++ b/test-suite/ide/undo012.fake @@ -0,0 +1,27 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# +ADD { Set Nested Proofs Allowed. } +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +ADD { Qed. } +QUERY { Show. } +ADD here { apply H. } +ADD { Qed. } +EDIT_AT here +# We should now be just before the Qed. +QUERY { Fail Check aa. } +QUERY { Check bb. } +QUERY { Check cc. } +ADD { Qed. } diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake new file mode 100644 index 0000000000..a3ccefd2ca --- /dev/null +++ b/test-suite/ide/undo013.fake @@ -0,0 +1,28 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# Second, trigger the undo of an inner proof +# +ADD { Set Nested Proofs Allowed. } +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD here { destruct H. } +ADD { Qed. } +ADD { apply H. } +EDIT_AT here +# <replay> +ADD { Qed. } +ADD { apply H. } +# </replay> +ADD { Qed. } +QUERY { Fail Show. } +QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake new file mode 100644 index 0000000000..13e718229c --- /dev/null +++ b/test-suite/ide/undo014.fake @@ -0,0 +1,27 @@ +# 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 +# +ADD { Set Nested Proofs Allowed. } +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD here { intro H. } +ADD { destruct H. } +EDIT_AT here +# <replay> +ADD { destruct H. } +# </replay> +ADD { Qed. } +ADD { apply H. } +ADD { Qed. } +QUERY { Fail Show. } +QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake new file mode 100644 index 0000000000..9cbd64460d --- /dev/null +++ b/test-suite/ide/undo015.fake @@ -0,0 +1,30 @@ +# 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 +# +ADD { Set Nested Proofs Allowed. } +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD here { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +EDIT_AT here +# <replay> +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +# </replay> +ADD { Qed. } +ADD { apply H. } +ADD { Qed. } +QUERY { Fail Show. } +QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake new file mode 100644 index 0000000000..15bd3cc92d --- /dev/null +++ b/test-suite/ide/undo016.fake @@ -0,0 +1,32 @@ +# 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 +# +ADD { Set Nested Proofs Allowed. } +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD here { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +EDIT_AT here +# <replay> +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +# </replay> +ADD { Qed. } +ADD { apply H. } +ADD { Qed. } +QUERY { Fail Show. } +QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake new file mode 100644 index 0000000000..37423dc727 --- /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 +# +ADD { Module M. } +ADD here { Definition x := 0. } +ADD { End M. } +EDIT_AT here +# <replay> +ADD { End M. } +# </replay> +QUERY { Check M.x. } diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake new file mode 100644 index 0000000000..11091bfa67 --- /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 +# +ADD { Section M. } +ADD here { Definition x := 0. } +ADD { End M. } +EDIT_AT here +# <replay> +ADD { End M. } +# </replay> +QUERY { Check x. } diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake new file mode 100644 index 0000000000..5df49ebbb7 --- /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 +# +ADD { Goal True. } +ADD { \{ } +ADD here { exact I. } +ADD { \} } +EDIT_AT here +# <replay> +ADD { \} } +# </replay> +ADD { Qed. } diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake new file mode 100644 index 0000000000..aa1d9bb2a7 --- /dev/null +++ b/test-suite/ide/undo020.fake @@ -0,0 +1,27 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# focusing a broken proof and fixing it + +# first proof +ADD { Lemma a : True. } +ADD { Proof using. } +ADD here { idtac. } +ADD { exact Ix. } +ADD { Qed. } +# second proof +ADD { Lemma b : False. } +ADD { Proof using. } +ADD { give_up. } +ADD last { Admitted. } +# We join and expect some proof to fail +WAIT +# Going back to the error +EDIT_AT here +# Fixing the proof +ADD { exact I. } +ADD { Qed. } +# we are back at the end +ASSERT TIP last +QUERY { Check a. } +QUERY { Check b. } diff --git a/test-suite/ide/undo021.fake b/test-suite/ide/undo021.fake new file mode 100644 index 0000000000..0d83ad25ac --- /dev/null +++ b/test-suite/ide/undo021.fake @@ -0,0 +1,29 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + +# first proof +ADD { Lemma a : True. } +ADD { Proof using. } +ADD here { idtac. } +ADD { exact Ix. } +ADD { Qed. } +# second proof +ADD { Lemma b : True. } +ADD here2 { Proof using. } +ADD { exact Ix. } +ADD { Qed. } +# We wait all slaves and expect both proofs to fail +WAIT +# Going back to the error +EDIT_AT here2 +# this is not implemented yet, all after here is erased +EDIT_AT here +# Fixing the proof +ADD { exact I. } +ADD last { Qed. } +ASSERT TIP last +# we are back at the end +QUERY { Check a. } +QUERY { Fail Check b. } diff --git a/test-suite/ide/undo022.fake b/test-suite/ide/undo022.fake new file mode 100644 index 0000000000..51d8d106e3 --- /dev/null +++ b/test-suite/ide/undo022.fake @@ -0,0 +1,41 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + interp error while fixing. +# the error should note make the GUI unfocus the currently focused proof. + +# first proof +ADD { Lemma a : True /\ True. } +ADD { Proof using. } +ADD here { split. } +ADD { exact Ix. } # first error +ADD { exact Ix. } # second error +ADD { Qed. } +# second proof +ADD { Lemma b : True. } +ADD { Proof using. } +ADD { exact I. } +ADD last { Qed. } +# We wait all slaves and expect both proofs to fail +WAIT +# Going back to the error +EDIT_AT here +# Fixing the proof +ADD fix { exact I. } +# showing the goals +GOALS +# re adding the wrong step +ADD { exact Ix. } +# showing the goals (failure) and retracting to the safe state suggested by Coq +FAILGOALS +# we assert we jumped back to the state immediately before the last (erroneous) +# one +ASSERT TIP fix +# finish off the proof +ADD { exact I. } +ADD { Qed. } +# here we unfocus, hence we jump back to the end of the document +ASSERT TIP last +# we are back at the end +QUERY { Check a. } +QUERY { Check b. } diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake new file mode 100644 index 0000000000..90af8785ad --- /dev/null +++ b/test-suite/ide/univ.fake @@ -0,0 +1,14 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping between broken proofs + interp error while fixing. +# the error should note make the GUI unfocus the currently focused proof. + +# first proof +ADD { Set Implicit Arguments. } +ADD { Record dynamic := dyn { dyn_type : Type; dyn_value : dyn_type }. } +ADD { Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2), dyn x1 = dyn x2 -> A1 = A2. } +ADD { Proof. } +ADD { now intros A1 A2 x1 x2 [= e1 e2]. } +ADD { Qed. } +JOIN |