diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | test-suite/Makefile | 6 | ||||
| -rw-r--r-- | test-suite/ide/undo007.fake | 20 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 14 |
4 files changed, 14 insertions, 28 deletions
diff --git a/Makefile.build b/Makefile.build index d98dc30f5..075638a23 100644 --- a/Makefile.build +++ b/Makefile.build @@ -541,7 +541,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) ide/document$(BESTOBJ) tools/fake_ide$(BESTOBJ) +$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,-I ide,str unix) diff --git a/test-suite/Makefile b/test-suite/Makefile index 83ea91a7d..389dffc49 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -218,8 +218,8 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$*" -coq-slaves on \ - -coq-slaves-opts fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \ + $(coqc) "$*" -async-proofs on \ + -async-proofs-worker-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -416,7 +416,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -boot -coq-slaves on -coq-slaves-opts min-proof-length-to-delegate=0" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-worker-flags min-proof-length-to-delegate=0" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake deleted file mode 100644 index 7a1dc81e0..000000000 --- a/test-suite/ide/undo007.fake +++ /dev/null @@ -1,20 +0,0 @@ -# Script simulating a dialog between coqide and coqtop -ideslave -# Run it via fake_ide -# -# Undoing declarations, as first step -# new in 8.2 -# -ADD { Theorem d : O=O. } -ADD here { Definition e := O. } -ADD { Definition f := O. } - -# This is a bug in Stm undo, e is lost from master -EDIT_AT here -ADD { Definition f := O. } -ADD { assert True by trivial. } -ADD { exact (eq_refl e). } -ADD { Qed. } -# QUERY { Stm PrintDag. } -# QUERY { Stm Finish. } -QUERY { Print d. } -QUERY { Check e. } diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 5b6db94a4..6567c2fe2 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -289,17 +289,23 @@ let usage () = (Filename.basename Sys.argv.(0)) (Parser.print grammar)) +module Coqide = Spawn.Sync(struct + let add_timeout ~sec:_ _ = () +end) + let main = Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let coqtop_name, input_file = match Sys.argv with - | [| _; f |] -> "coqtop", f - | [| _; f; ct |] -> ct, f + let coqtop_name, coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> "coqtop",[|"-ideslave"|], f + | [| _; f; ct |] -> + let ct = Str.split (Str.regexp " ") ct in + List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = - let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in + let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in let op = Xml_printer.make (Xml_printer.TChannel cout) in Xml_parser.check_eof ip false; |