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 (limited to 'test-suite/coq-makefile') 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 (limited to 'test-suite/coq-makefile') 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(-) (limited to 'test-suite/coq-makefile') 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