diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-23 17:24:18 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-24 14:14:31 +0200 |
| commit | c15571e367cf4d75c9e4aac589170e0213e4fe3b (patch) | |
| tree | ca12232b2b7c24d3e2a8e08491c6ca2c5da18034 | |
| parent | 1774a87504945a6e8b8aa465297dce672364b8a4 (diff) | |
fixup fakeide test-suite
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 1 | ||||
| -rw-r--r-- | test-suite/Makefile | 4 | ||||
| -rw-r--r-- | tools/coqc.ml | 3 |
4 files changed, 6 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index dd1c30a23..8dfc3fbfe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -625,7 +625,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) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(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) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,-I ide,str unix) diff --git a/Makefile.common b/Makefile.common index 4bc203197..f1817a956 100644 --- a/Makefile.common +++ b/Makefile.common @@ -54,6 +54,7 @@ endif BESTOBJ:=$(if $(OPT),.cmx,.cmo) BESTLIB:=$(if $(OPT),.cmxa,.cma) +BESTDYN:=$(if $(OPT),.cmxs,.cma) COQBINARIES:= $(COQMKTOP) \ $(COQTOPBYTE) $(COQTOPEXE) \ diff --git a/test-suite/Makefile b/test-suite/Makefile index 211797251..81a556671 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -228,7 +228,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(HIDE){ \ echo $(call log_intro,$<); \ $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \ - -async-proofs-worker-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \ + -async-proofs-private-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); \ @@ -425,7 +425,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-worker-flags min-proof-length-to-delegate=0" 2>&1; \ + $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-always-delegate" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/tools/coqc.ml b/tools/coqc.ml index 1d416a1c4..5aa6f0b04 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -96,6 +96,7 @@ let parse_args () = |"-impredicative-set"|"-vm"|"-no-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick" + |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem @@ -105,7 +106,7 @@ let parse_args () = |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" - |"-async-proofs-j" |"-async-proofs-worker-flags" |"-async-proofs" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" as o) :: rem -> begin match rem with |