From 8300ef2c07a17451f594bcbd6f0689cafb87c3fb Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 10:40:49 -0500 Subject: Refresh patches --- debian/patches/remove-tests-that-need-coqlib.patch | 387 +++++++++++---------- 1 file changed, 206 insertions(+), 181 deletions(-) (limited to 'debian/patches/remove-tests-that-need-coqlib.patch') 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 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 < 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 </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 </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 < 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 < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired </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 < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual +-(cd "$(find tmp -name user-contrib)" && find .) | sort > 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 $? +- 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 </dev/null && find . && popd >/dev/null +- done < <(find tmp -name user-contrib -print0) +-) | sort -u > actual +-sort -u > desired <