diff options
| author | Maxime Dénès | 2019-10-21 15:50:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-21 15:50:26 +0200 |
| commit | 50e3fd2b6f30ab209200950fd5a804a18b47288f (patch) | |
| tree | 21085d5efc424c36d69963eab3fe123f0a261422 | |
| parent | c6056bdc54d02dc5c6a91aeacb13460e8dd365e3 (diff) | |
| parent | cd03a27b917dedc129af980a6099b20134cba9f5 (diff) | |
Merge PR #10857: Fix votour after the change of representation of opaques.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | checker/votour.ml | 1 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rwxr-xr-x | test-suite/misc/votour.sh | 3 |
5 files changed, 7 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index 35f5e26272..ed4cde2b16 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ coq.timing.diff: coqlib.timing.diff # shouldn't be done in a same make -j... run, otherwise both ocamlc and # ocamlopt might race for access to the same .cmi files. -byte: coqbyte coqide-byte pluginsbyte printers +byte: coqbyte coqide-byte pluginsbyte printers bin/votour.byte .PHONY: world coq byte world.timing.diff coq.timing.diff diff --git a/Makefile.common b/Makefile.common index 2d1200c071..1ad255d156 100644 --- a/Makefile.common +++ b/Makefile.common @@ -41,9 +41,10 @@ COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py +VOTOUR:=bin/votour TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) $(DOC_GRAM) + $(COQWORKMGR) $(COQPP) $(DOC_GRAM) $(VOTOUR) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) diff --git a/checker/votour.ml b/checker/votour.ml index 5a610e6938..97584831e5 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -364,7 +364,6 @@ let visit_vo f = make_seg "summary" Values.v_libsum; make_seg "library" Values.v_lib; make_seg "univ constraints of opaque proofs" Values.v_univopaques; - make_seg "discharging info" (Opt Any); make_seg "STM tasks" (Opt Values.v_stm_seg); make_seg "opaque proofs" Values.v_opaquetable; |] in diff --git a/configure.ml b/configure.ml index e59a41a8d4..8e04dc46b2 100644 --- a/configure.ml +++ b/configure.ml @@ -20,7 +20,7 @@ let state_magic = 581091 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; - "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"] + "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep";"votour"] let verbose = ref false (* for debugging this script *) diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh new file mode 100755 index 0000000000..ac26aed49b --- /dev/null +++ b/test-suite/misc/votour.sh @@ -0,0 +1,3 @@ +command -v "${BIN}votour" || { echo "Missing votour"; exit 1; } + +"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null |