From e23d443a3a64b30a77e8ea92f347f933a865bb99 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 16:41:25 -0500 Subject: Disable tests which require `-coqlib` to be set A number of tests (mostly for coq_makefile) assume that Coq is installed when the test runs. This isn't true in an sbuild environment, though, so disable those tests. --- .../0006-remove-tests-that-need-coqlib.patch | 633 +++++++++++++++++++++ debian/patches/series | 1 + debian/rules | 3 +- 3 files changed, 636 insertions(+), 1 deletion(-) create mode 100644 debian/patches/0006-remove-tests-that-need-coqlib.patch diff --git a/debian/patches/0006-remove-tests-that-need-coqlib.patch b/debian/patches/0006-remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/0006-remove-tests-that-need-coqlib.patch @@ -0,0 +1,633 @@ +From: Benjamin Barenblat +Subject: Disable tests which require -coqlib to be set +Bug: https://github.com/coq/coq/issues/5975 +Forwarded: not-needed + +A number of tests (mostly for coq_makefile) assume that Coq is +installed when the test runs. This isn't true in an sbuild environment, +though, so disable those tests. +--- a/test-suite/misc/printers.sh ++++ /dev/null +@@ -1,3 +0,0 @@ +-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" +-if [ $? = 0 ]; then exit 1; else exit 0; fi +- +--- a/test-suite/coq-makefile/arg/run.sh ++++ /dev/null +@@ -1,7 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/compat-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/coqdoc1/run.sh ++++ /dev/null +@@ -1,51 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <> 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 +- export OCAMLPATH=`cygpath -w $PWD/findlib` +-fi +-make -C findlib/foo clean +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-cat Makefile.local +-make -C findlib/foo +-make +-make byte +--- a/test-suite/coq-makefile/latex1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-if which pdflatex; then +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make all.pdf +- +-fi +-exit 0 # test skipped +--- a/test-suite/coq-makefile/merlin1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make .merlin +-cat > desired < actual +-exec diff -u desired actual +--- a/test-suite/coq-makefile/mlpack1/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort > desired < actual +-sort > desired < actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired < ${file}${ext}.processed +- done +-done +-for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-cd ../per-file-before +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=before -j2 || exit $? +- +-cd ../per-file-after +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=after -j2 || exit $? +- +-find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +-make all.timing.diff -j2 || exit $? +-echo "cat A.v.before-timing" +-cat A.v.before-timing +-echo +-echo "cat A.v.after-timing" +-cat A.v.after-timing +-echo +-echo "cat A.v.timing.diff" +-cat A.v.timing.diff +-echo +- +-for ext in "" .desired; do +- for file in A.v.timing.diff; do +- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed +- done +-done +-for file in A.v.timing.diff; do +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-exit 0 diff --git a/debian/patches/series b/debian/patches/series index dab7506c..8e94de36 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -3,3 +3,4 @@ 0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch 0004-5127-fails-on-mips.patch 0005-remove-ssrmatching.patch +0006-remove-tests-that-need-coqlib.patch diff --git a/debian/rules b/debian/rules index c12c540d..8c97cf17 100755 --- a/debian/rules +++ b/debian/rules @@ -79,7 +79,8 @@ endif .PHONY: override_dh_auto_test override_dh_auto_test: - $(MAKE) test-suite COMPLEXITY= + CAML_LD_LIBRARY_PATH=$PWD/kernel/byterun COQLIB=$PWD \ + $(MAKE) test-suite COMPLEXITY= .PHONY: override_dh_auto_install override_dh_auto_install: -- cgit v1.2.3