diff options
Diffstat (limited to 'debian/patches/remove-tests-that-need-coqlib.patch')
-rw-r--r-- | debian/patches/remove-tests-that-need-coqlib.patch | 633 |
1 files changed, 633 insertions, 0 deletions
diff --git a/debian/patches/remove-tests-that-need-coqlib.patch b/debian/patches/remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/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 |