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.

3 files changed, 636 insertions, 1 deletions

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 <bbaren@debian.org>
+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 <<EOT
+-.
+-./test
+-./test/test_plugin.cmi
+-./test/test_plugin.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.glob
+-./test/test.v
+-./test/test.vo
+-./test/sub
+-./test/sub/testsub.glob
+-./test/sub/testsub.v
+-./test/sub/testsub.vo
+-./test/mlihtml
+-./test/mlihtml/index_exceptions.html
+-./test/mlihtml/index.html
+-./test/mlihtml/index_class_types.html
+-./test/mlihtml/type_Test_aux.html
+-./test/mlihtml/index_module_types.html
+-./test/mlihtml/index_classes.html
+-./test/mlihtml/type_Test.html
+-./test/mlihtml/style.css
+-./test/mlihtml/index_attributes.html
+-./test/mlihtml/index_types.html
+-./test/mlihtml/Test_aux.html
+-./test/mlihtml/index_values.html
+-./test/mlihtml/Test.html
+-./test/mlihtml/index_extensions.html
+-./test/mlihtml/index_methods.html
+-./test/mlihtml/index_modules.html
+-./test/html
+-./test/html/index.html
+-./test/html/test.sub.testsub.html
+-./test/html/toc.html
+-./test/html/coqdoc.css
+-./test/html/test.test.html
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/coqdoc2/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 <<EOT
+-.
+-./test
+-./test/test_plugin.cmi
+-./test/test_plugin.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.glob
+-./test/test.v
+-./test/test.vo
+-./test/sub
+-./test/sub/testsub.glob
+-./test/sub/testsub.v
+-./test/sub/testsub.vo
+-./test/mlihtml
+-./test/mlihtml/index_exceptions.html
+-./test/mlihtml/index.html
+-./test/mlihtml/index_class_types.html
+-./test/mlihtml/type_Test_aux.html
+-./test/mlihtml/index_module_types.html
+-./test/mlihtml/index_classes.html
+-./test/mlihtml/type_Test.html
+-./test/mlihtml/style.css
+-./test/mlihtml/index_attributes.html
+-./test/mlihtml/index_types.html
+-./test/mlihtml/Test_aux.html
+-./test/mlihtml/index_values.html
+-./test/mlihtml/Test.html
+-./test/mlihtml/index_extensions.html
+-./test/mlihtml/index_methods.html
+-./test/mlihtml/index_modules.html
+-./test/html
+-./test/html/index.html
+-./test/html/test.sub.testsub.html
+-./test/html/toc.html
+-./test/html/coqdoc.css
+-./test/html/test.test.html
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/emptyprefix/run.sh
++++ /dev/null
+@@ -1,17 +0,0 @@
+-#!/usr/bin/env bash
+-
+-set -e
+-
+-. ../template/init.sh
+-
+-mv theories/sub theories2
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+-
+-cp ../_CoqProject.sub theories2/_CoqProject
+-cd theories2
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make
+--- a/test-suite/coq-makefile/extend-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/findlib-package/run.sh
++++ /dev/null
+@@ -1,18 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-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
+-  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 <<EOT
+-B src
+-S src
+-EOT
+-tail -2 .merlin > 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 <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test_plugin.cmi
+-./test/test_plugin.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/mlpack2/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 <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test_plugin.cmi
+-./test/test_plugin.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/multiroot/run.sh
++++ /dev/null
+@@ -1,56 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-cp -r theories theories2
+-mv src/test_plugin.mlpack src/test_plugin.mllib
+-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 > desired <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test.cmi
+-./test/test.cmx
+-./test/test_aux.cmi
+-./test/test_aux.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-./test2
+-./test2/test.glob
+-./test2/test.v
+-./test2/test.vo
+-./orphan_test_test2_test
+-./orphan_test_test2_test/html
+-./orphan_test_test2_test/html/coqdoc.css
+-./orphan_test_test2_test/html/index.html
+-./orphan_test_test2_test/html/test2.test.html
+-./orphan_test_test2_test/html/test.test.html
+-./orphan_test_test2_test/html/toc.html
+-./orphan_test_test2_test/mlihtml
+-./orphan_test_test2_test/mlihtml/index_attributes.html
+-./orphan_test_test2_test/mlihtml/index_classes.html
+-./orphan_test_test2_test/mlihtml/index_class_types.html
+-./orphan_test_test2_test/mlihtml/index_exceptions.html
+-./orphan_test_test2_test/mlihtml/index_extensions.html
+-./orphan_test_test2_test/mlihtml/index.html
+-./orphan_test_test2_test/mlihtml/index_methods.html
+-./orphan_test_test2_test/mlihtml/index_modules.html
+-./orphan_test_test2_test/mlihtml/index_module_types.html
+-./orphan_test_test2_test/mlihtml/index_types.html
+-./orphan_test_test2_test/mlihtml/index_values.html
+-./orphan_test_test2_test/mlihtml/style.css
+-./orphan_test_test2_test/mlihtml/Test_aux.html
+-./orphan_test_test2_test/mlihtml/Test.html
+-./orphan_test_test2_test/mlihtml/type_Test_aux.html
+-./orphan_test_test2_test/mlihtml/type_Test.html
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/only/run.sh
++++ /dev/null
+@@ -1,10 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-cat Makefile.conf
+-make only TGTS="src/test.cmi src/test_aux.cmi" -j2
+-test -f src/test.cmi
+-test -f src/test_aux.cmi
+-! test -f src/test.cmo
+--- a/test-suite/coq-makefile/plugin1/run.sh
++++ /dev/null
+@@ -1,26 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-mv src/test_plugin.mlpack src/test_plugin.mllib
+-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 <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test.cmi
+-./test/test.cmx
+-./test/test_aux.cmi
+-./test/test_aux.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/plugin2/run.sh
++++ /dev/null
+@@ -1,26 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-mv src/test_plugin.mlpack src/test_plugin.mllib
+-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 <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test.cmi
+-./test/test.cmx
+-./test/test_aux.cmi
+-./test/test_aux.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/plugin3/run.sh
++++ /dev/null
+@@ -1,26 +0,0 @@
+-#!/usr/bin/env bash
+-
+-. ../template/init.sh
+-
+-mv src/test_plugin.mlpack src/test_plugin.mllib
+-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 <<EOT
+-.
+-./test
+-./test/test.glob
+-./test/test.cmi
+-./test/test.cmx
+-./test/test_aux.cmi
+-./test/test_aux.cmx
+-./test/test_plugin.cmxa
+-./test/test_plugin.cmxs
+-./test/test.v
+-./test/test.vo
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/quick2vo/run.sh
++++ /dev/null
+@@ -1,12 +0,0 @@
+-#!/usr/bin/env bash
+-a=`uname`
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-# 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
+--- a/test-suite/coq-makefile/uninstall1/run.sh
++++ /dev/null
+@@ -1,18 +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 uninstall DSTROOT="$PWD/tmp"
+-make uninstall-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 <<EOT
+-.
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/uninstall2/run.sh
++++ /dev/null
+@@ -1,18 +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 uninstall DSTROOT="$PWD/tmp"
+-make uninstall-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 <<EOT
+-.
+-EOT
+-exec diff -u desired actual
+--- a/test-suite/coq-makefile/validate1/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 make validate
+--- a/test-suite/coq-makefile/vio2vo/run.sh
++++ /dev/null
+@@ -1,13 +0,0 @@
+-#!/usr/bin/env bash
+-a=`uname`
+-
+-. ../template/init.sh
+-
+-coq_makefile -f _CoqProject -o Makefile
+-make quick
+-# 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
+--- a/test-suite/coq-makefile/timing/run.sh
++++ /dev/null
+@@ -1,108 +0,0 @@
+-#!/usr/bin/env bash
+-
+-#set -x
+-set -e
+-
+-. ../template/path-init.sh
+-
+-# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues
+-
+-MAKEFLAGS=
+-
+-cd precomputed-time-tests
+-./run.sh || exit $?
+-
+-cd ../error
+-coq_makefile -f _CoqProject -o Makefile
+-make cleanall
+-if make pretty-timed TGTS="all" -j1; then
+-    echo "Error: make pretty-timed should have failed"
+-    exit 1
+-fi
+-
+-cd ../aggregate
+-coq_makefile -f _CoqProject -o Makefile
+-make cleanall
+-make pretty-timed TGTS="all" -j1 || exit $?
+-
+-cd ../before
+-coq_makefile -f _CoqProject -o Makefile
+-make cleanall
+-make make-pretty-timed-before TGTS="all" -j1 || exit $?
+-
+-cd ../after
+-coq_makefile -f _CoqProject -o Makefile
+-make cleanall
+-make make-pretty-timed-after TGTS="all" -j1 || exit $?
+-rm -f time-of-build-before.log
+-make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
+-cp ../before/time-of-build-before.log ./
+-make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $?
+-
+-INFINITY="∞"
+-INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase
+-
+-TO_SED_IN_BOTH=(
+-    -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
+-    -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
+-    -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces
+-    -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
+-    -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
+-    -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
+-)
+-
+-TO_SED_IN_PER_FILE=(
+-    -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
+-    -e s'/  */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
+-    -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
+-)
+-
+-TO_SED_IN_PER_LINE=(
+-    -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
+-    -e s'/  */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
+-    )
+-
+-for ext in "" .desired; do
+-    for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
+-        cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${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: