diff options
Diffstat (limited to 'debian/patches/remove-tests-that-need-coqlib.patch')
| -rw-r--r-- | debian/patches/remove-tests-that-need-coqlib.patch | 387 |
1 files changed, 206 insertions, 181 deletions
diff --git a/debian/patches/remove-tests-that-need-coqlib.patch b/debian/patches/remove-tests-that-need-coqlib.patch index 48cd1b96..be694991 100644 --- a/debian/patches/remove-tests-that-need-coqlib.patch +++ b/debian/patches/remove-tests-that-need-coqlib.patch @@ -1,6 +1,5 @@ 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 @@ -8,10 +7,9 @@ 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 -- +@@ -1,2 +0,0 @@ +-#!/bin/sh +-if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi --- a/test-suite/coq-makefile/arg/run.sh +++ /dev/null @@ -1,7 +0,0 @@ @@ -33,9 +31,96 @@ though, so disable those tests. -cat Makefile.conf -make -exec test -f "subdir/done" +--- 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/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/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/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/coqdoc1/run.sh +++ /dev/null -@@ -1,51 +0,0 @@ +@@ -1,59 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh @@ -47,7 +132,15 @@ though, so disable those tests. -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 +- +-# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +- -sort -u > desired <<EOT -. -./test @@ -89,7 +182,7 @@ though, so disable those tests. -exec diff -u desired actual --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ /dev/null -@@ -1,51 +0,0 @@ +@@ -1,57 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh @@ -101,7 +194,13 @@ though, so disable those tests. -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 +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +- -sort -u > desired <<EOT -. -./test @@ -141,40 +240,9 @@ though, so disable those tests. -./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 @@ +@@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh @@ -184,7 +252,8 @@ though, so disable those tests. -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` +- OCAMLPATH=$(cygpath -w "$PWD"/findlib) +- export OCAMLPATH -fi -make -C findlib/foo clean -coq_makefile -f _CoqProject -o Makefile @@ -193,38 +262,6 @@ though, so disable those tests. -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 @@ @@ -238,7 +275,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired <<EOT -. -./test @@ -264,7 +301,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired <<EOT -. -./test @@ -279,7 +316,7 @@ though, so disable those tests. -exec diff -u desired actual --- a/test-suite/coq-makefile/multiroot/run.sh +++ /dev/null -@@ -1,56 +0,0 @@ +@@ -1,61 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh @@ -293,7 +330,12 @@ though, so disable those tests. -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 +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual -sort > desired <<EOT -. -./test @@ -336,19 +378,6 @@ though, so disable those tests. -./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 @@ @@ -363,7 +392,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired <<EOT -. -./test @@ -392,7 +421,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired <<EOT -. -./test @@ -421,7 +450,7 @@ though, so disable those tests. -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired <<EOT -. -./test @@ -440,89 +469,20 @@ though, so disable those tests. +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash --a=`uname` +-a=$(uname) - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -# vio2vo is broken on Windows (#6720) --if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +-if [ "$a" = "Darwin" ] || [ "$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 @@ +@@ -1,105 +0,0 @@ -#!/usr/bin/env bash - -#set -x @@ -587,16 +547,14 @@ though, so disable those tests. - -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 $? +- for ext in "" .desired; do +- grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed +- done +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? -done - -cd ../per-file-before @@ -621,13 +579,80 @@ though, so disable those tests. -cat A.v.timing.diff -echo - +-file=A.v.timing.diff +- -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 $? +- sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed" -done - +-diff -u "$file.desired.processed" "$file.processed" || exit $? +- -exit 0 +--- a/test-suite/coq-makefile/uninstall1/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 install-doc DSTROOT="$PWD/tmp" +-make uninstall DSTROOT="$PWD/tmp" +-make uninstall-doc DSTROOT="$PWD/tmp" +-#make debug +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +-sort -u > desired <<EOT +-. +-EOT +-exec diff -u desired actual +--- a/test-suite/coq-makefile/uninstall2/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 install-doc DSTROOT="$PWD/tmp" +-make uninstall DSTROOT="$PWD/tmp" +-make uninstall-doc DSTROOT="$PWD/tmp" +-#make debug +-( +- while IFS= read -r -d '' d +- do +- pushd "$d" >/dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +-sort -u > desired <<EOT +-. +-EOT +-exec diff -u desired actual +--- 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" ] || [ "$a" = "Linux" ]; then +- make vio2vo J=2 +- test -f theories/test.vo +- make validate +-fi |