Prepare to import ssrmatching in 8.9.0

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).

1 files changed, 633 insertions, 0 deletions

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 <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