1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sun, 11 Aug 2019 18:33:24 +0200
Subject: Disable tests which require ocamlopt
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit
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.
---
test-suite/Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
--- coq.orig/test-suite/Makefile
+++ coq/test-suite/Makefile
@@ -143,7 +143,7 @@
coqdoc ssr $(wildcard primitive/*) ltac2
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc ide bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS)
+SUBSYSTEMS := $(VSUBSYSTEMS) misc ide bugs ide coqchk output-coqchk coqwc coq-makefile tools
.csdp.cache: .csdp.cache.test-suite
cp $< $@
--- coq.orig/test-suite/coq-makefile/findlib-package-unpacked/run.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/bash
-
-. ../template/init.sh
-mv src/test_plugin.mlpack src/test_plugin.mllib
-sed -i.old 's/coq-core.plugins.ltac/coq-core.plugins.ltac,foo/' src/META.coq-test-suite
-
-echo "let () = Foolib.foo ();;" >> src/test_aux.ml
-if which cygpath 2>/dev/null; then
- # separator is ; on windows
- OCAMLPATH=$OCAMLPATH;$(cygpath -m "$PWD"/findlib)
-else
- OCAMLPATH=$OCAMLPATH:$PWD/findlib
-fi
-make -C findlib/foo clean
-coq_makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-cat Makefile.local
-make -C findlib/foo
-if which ocamlopt >/dev/null 2>&1; then
- make
-fi
-make byte
|
