From 4bf1d996c98a37c312c5dddf418316d77086e9c2 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 16:49:08 -0500 Subject: Disable .vio tests, as they don’t work on bytecode architectures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operations with .vio files fail when Coq has been compiled with ocamlc; see https://github.com/coq/coq/issues/9141. Disable tests related to .vio generation to prevent this from breaking the build. --- debian/patches/remove-bytecode-failing-tests.patch | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/debian/patches/remove-bytecode-failing-tests.patch b/debian/patches/remove-bytecode-failing-tests.patch index 49fe7fc3..393ae940 100644 --- a/debian/patches/remove-bytecode-failing-tests.patch +++ b/debian/patches/remove-bytecode-failing-tests.patch @@ -5,6 +5,9 @@ Forwarded: not-needed Disable unit tests. They require ocamlopt, which isn't available on all Debian architectures, and Gaëtan Gilbert says that "they don't test much yet" anyway. + +Also disable .vio tests, as they run afoul +of https://github.com/coq/coq/issues/9141. --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -102,7 +102,7 @@ @@ -12,7 +15,7 @@ yet" anyway. # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests -+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools ++SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide coqchk coqwc coq-makefile tools PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ -- cgit v1.2.3