Package: coq / 8.12.0-3

remove-bytecode-failing-tests.patch Patch series | download
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
56
57
58
59
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(-)

Index: coq/test-suite/Makefile
===================================================================
--- coq.orig/test-suite/Makefile	2020-08-21 14:58:14.079912139 +0200
+++ coq/test-suite/Makefile	2020-08-21 15:00:12.651911312 +0200
@@ -115,7 +115,7 @@
   coqdoc ssr primitive/uint63 primitive/float ltac2
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS)
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide coqchk output-coqchk coqwc coq-makefile tools
 
 .csdp.cache: .csdp.cache.test-suite
 	cp $< $@
Index: coq/test-suite/coq-makefile/findlib-package-unpacked/run.sh
===================================================================
--- coq.orig/test-suite/coq-makefile/findlib-package-unpacked/run.sh	2020-08-21 14:58:14.079912139 +0200
+++ /dev/null	1970-01-01 00:00:00.000000000 +0000
@@ -1,22 +0,0 @@
-#!/usr/bin/env bash
-
-. ../template/init.sh
-mv src/test_plugin.mlpack src/test_plugin.mllib
-
-echo "let () = Foolib.foo ();;" >> src/test_aux.ml
-export OCAMLPATH=$OCAMLPATH:$PWD/findlib
-if which cygpath 2>/dev/null; then
-  # the only way I found to pass OCAMLPATH on win is to have it contain
-  # only one entry
-  OCAMLPATH=$(cygpath -w "$PWD"/findlib)
-  export OCAMLPATH
-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