From 8dc97f734f90f50980b636e2c0c8de34d20a5843 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 20 Sep 2017 12:59:38 +0200 Subject: new quick2vo target: like vio2vo, but smarter --- tools/CoqMakefile.in | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index ca02c983d..a426c3cb2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -381,7 +381,7 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralph's bugreport +# FIXME, see Ralf's bugreport quick: $(VOFILES:.vo=.vio) .PHONY: quick @@ -390,6 +390,18 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +quick2vo: + $(HIDE)make -j $(J) quick + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + checkproofs: $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -- cgit v1.2.3 From 4176a769bcafc9c43cae88fc11ed3d83919263fb Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 6 Feb 2018 16:33:22 +0100 Subject: test "make quick2vo" --- test-suite/coq-makefile/quick2vo/_CoqProject | 10 ++++++++++ test-suite/coq-makefile/quick2vo/run.sh | 9 +++++++++ 2 files changed, 19 insertions(+) create mode 100644 test-suite/coq-makefile/quick2vo/_CoqProject create mode 100755 test-suite/coq-makefile/quick2vo/run.sh diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh new file mode 100755 index 000000000..b8ce4709e --- /dev/null +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make quick2vo J=2 +test -f theories/test.vo +make validate -- cgit v1.2.3 From 56b8b0e05c4c48a83a327c5e385c8d7ab0fec784 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 6 Feb 2018 16:47:09 +0100 Subject: also test vio2vo --- test-suite/coq-makefile/vio2vo/_CoqProject | 10 ++++++++++ test-suite/coq-makefile/vio2vo/run.sh | 10 ++++++++++ 2 files changed, 20 insertions(+) create mode 100644 test-suite/coq-makefile/vio2vo/_CoqProject create mode 100755 test-suite/coq-makefile/vio2vo/run.sh diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject new file mode 100644 index 000000000..69f47302e --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh new file mode 100755 index 000000000..86b2cfa28 --- /dev/null +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make quick +make vio2vo J=2 +test -f theories/test.vo +make validate -- cgit v1.2.3 From 999a7059840bdfbdc46ce198e1a16b8621f93588 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 9 Feb 2018 10:16:55 +0100 Subject: disable tests: vio2vo is broken in Windows --- test-suite/coq-makefile/quick2vo/run.sh | 11 +++++++---- test-suite/coq-makefile/vio2vo/run.sh | 11 +++++++---- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh index b8ce4709e..9e681223b 100755 --- a/test-suite/coq-makefile/quick2vo/run.sh +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -1,9 +1,12 @@ #!/usr/bin/env bash +a=`uname` . ../template/init.sh coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make quick2vo J=2 -test -f theories/test.vo -make validate +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make quick2vo J=2 + test -f theories/test.vo + make validate +fi diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh index 86b2cfa28..85656da41 100755 --- a/test-suite/coq-makefile/vio2vo/run.sh +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -1,10 +1,13 @@ #!/usr/bin/env bash +a=`uname` . ../template/init.sh coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf make quick -make vio2vo J=2 -test -f theories/test.vo -make validate +# vio2vo is broken on Windows (#6720) +if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then + make vio2vo J=2 + test -f theories/test.vo + make validate +fi -- cgit v1.2.3