diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | Makefile.build | 9 | ||||
-rw-r--r-- | test-suite/Makefile | 22 | ||||
-rw-r--r-- | test-suite/ide/undo001.fake | 10 | ||||
-rw-r--r-- | test-suite/ide/undo002.fake | 10 | ||||
-rw-r--r-- | test-suite/ide/undo003.fake | 8 | ||||
-rw-r--r-- | test-suite/ide/undo004.fake | 14 | ||||
-rw-r--r-- | test-suite/ide/undo005.fake | 15 | ||||
-rw-r--r-- | test-suite/ide/undo006.fake | 14 | ||||
-rw-r--r-- | test-suite/ide/undo007.fake | 17 | ||||
-rw-r--r-- | test-suite/ide/undo008.fake | 18 | ||||
-rw-r--r-- | test-suite/ide/undo009.fake | 20 | ||||
-rw-r--r-- | test-suite/ide/undo010.fake | 28 | ||||
-rw-r--r-- | test-suite/ide/undo011.fake | 32 | ||||
-rw-r--r-- | test-suite/ide/undo012.fake | 26 | ||||
-rw-r--r-- | test-suite/ide/undo013.fake | 31 | ||||
-rw-r--r-- | test-suite/ide/undo014.fake | 26 | ||||
-rw-r--r-- | test-suite/ide/undo015.fake | 29 | ||||
-rw-r--r-- | test-suite/ide/undo016.fake | 34 | ||||
-rw-r--r-- | test-suite/ide/undo017.fake | 13 | ||||
-rw-r--r-- | test-suite/ide/undo018.fake | 13 | ||||
-rw-r--r-- | test-suite/ide/undo019.fake | 14 | ||||
-rw-r--r-- | tools/fake_ide.ml | 70 |
23 files changed, 472 insertions, 3 deletions
@@ -165,7 +165,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) + rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) bin/fake_ide find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) diff --git a/Makefile.build b/Makefile.build index d84030664..46512e28a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -379,7 +379,7 @@ MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE) check:: validate test-suite -test-suite: world $(ALLSTDLIB).v +test-suite: world $(ALLSTDLIB).v bin/fake_ide $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all $(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi @@ -508,6 +508,13 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) +# fake_ide : for debugging or test-suite purpose, a fake ide simulating +# a connection to coqtop -ideslave + +bin/fake_ide: toplevel/ide_intf.mli toplevel/ide_intf.ml tools/fake_ide.ml + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,unix) + # Special rule for the compatibility-with-camlp5 extension for camlp4 ifeq ($(CAMLP4),camlp4) 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. diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml new file mode 100644 index 000000000..3bcbb96aa --- /dev/null +++ b/tools/fake_ide.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *) + +exception Comment + +let coqtop = ref (stdin, stdout) + +let eval_call (call:'a Ide_intf.call) = + prerr_endline (Ide_intf.pr_call call); + Marshal.to_channel (snd !coqtop) call []; flush (snd !coqtop); + let res = ((Marshal.from_channel (fst !coqtop)) : 'a Ide_intf.value) in + prerr_endline (Ide_intf.pr_full_value call res); + match res with Ide_intf.Fail _ -> exit 1 | _ -> () + +let commands = + [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s))); + "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s))); + "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s))); + "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); + "GOALS", (fun _ -> eval_call Ide_intf.goals); + "STATUS", (fun _ -> eval_call Ide_intf.status); + "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); + "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); + "#", (fun _ -> raise Comment); + ] + +let read_eval_print line = + let lline = String.length line in + let rec find_cmd = function + | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1 + | (cmd,fn) :: cmds -> + let lcmd = String.length cmd in + if lline >= lcmd && String.sub line 0 lcmd = cmd then + let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> "" + in fn arg + else find_cmd cmds + in + find_cmd commands + +let usage () = + Printf.printf + "A fake coqide process talking to a coqtop -ideslave.\n\ + Usage: %s [<coqtop>]\n\ + Input syntax is one API call per line, the keyword coming first,\n\ + with the rest of the line as string argument (e.g. INTERP Check plus.)\n\ + Supported API keywords are:\n" (Filename.basename Sys.argv.(0)); + List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands; + exit 1 + +let main = + let coqtop_name = match Array.length Sys.argv with + | 1 -> "coqtop" + | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1) + | _ -> usage () + in + coqtop := Unix.open_process (coqtop_name^" -ideslave"); + while true do + try read_eval_print (read_line ()) + with + | End_of_file -> exit 0 + | Comment -> () + done |