From cf916fd97fbac51af6fa68ec2704da2a28ef9ede Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:12:28 -0500 Subject: Prepare to import ssrmatching in 8.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Upstream has corrected most of the licensing issues with ssrmatching in 8.9.0. That version introduced one new file with a CeCILL-B license, but it’s an .mli file, so OCaml should be able to infer its contents. Don’t import the offending .mli, but do import the files with corrected license headers. Remove the patch introduced in 5d3dc22cc205021e517a81943952655c51777083 (which backported the correctly licensed files). --- .../0005-remove-tests-that-need-coqlib.patch | 633 +++++++++++++++++++++ 1 file changed, 633 insertions(+) create mode 100644 debian/patches/0005-remove-tests-that-need-coqlib.patch (limited to 'debian/patches/0005-remove-tests-that-need-coqlib.patch') diff --git a/debian/patches/0005-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/0005-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 -- cgit v1.2.3