From: Benjamin Barenblat <bbaren@debian.org>
Date: Sun, 11 Aug 2019 18:33:23 +0200
Subject: Disable tests which require -coqlib to be set

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.
---
 test-suite/coq-makefile/arg/run.sh             |   7 --
 test-suite/coq-makefile/compat-subdirs/run.sh  |   8 --
 test-suite/coq-makefile/coqdoc1/run.sh         |  59 --------------
 test-suite/coq-makefile/coqdoc2/run.sh         |  57 --------------
 test-suite/coq-makefile/emptyprefix/run.sh     |  17 ----
 test-suite/coq-makefile/extend-subdirs/run.sh  |   8 --
 test-suite/coq-makefile/findlib-package/run.sh |  19 -----
 test-suite/coq-makefile/latex1/run.sh          |  13 ---
 test-suite/coq-makefile/merlin1/run.sh         |  13 ---
 test-suite/coq-makefile/mlpack1/run.sh         |  23 ------
 test-suite/coq-makefile/mlpack2/run.sh         |  23 ------
 test-suite/coq-makefile/multiroot/run.sh       |  61 --------------
 test-suite/coq-makefile/only/run.sh            |  10 ---
 test-suite/coq-makefile/plugin1/run.sh         |  26 ------
 test-suite/coq-makefile/plugin2/run.sh         |  26 ------
 test-suite/coq-makefile/plugin3/run.sh         |  26 ------
 test-suite/coq-makefile/quick2vo/run.sh        |  12 ---
 test-suite/coq-makefile/timing/run.sh          | 105 -------------------------
 test-suite/coq-makefile/uninstall1/run.sh      |  23 ------
 test-suite/coq-makefile/uninstall2/run.sh      |  23 ------
 test-suite/coq-makefile/validate1/run.sh       |   8 --
 test-suite/coq-makefile/vio2vo/run.sh          |  13 ---
 test-suite/misc/printers.sh                    |   2 -
 23 files changed, 582 deletions(-)
 delete mode 100755 test-suite/coq-makefile/arg/run.sh
 delete mode 100755 test-suite/coq-makefile/compat-subdirs/run.sh
 delete mode 100755 test-suite/coq-makefile/coqdoc1/run.sh
 delete mode 100755 test-suite/coq-makefile/coqdoc2/run.sh
 delete mode 100755 test-suite/coq-makefile/emptyprefix/run.sh
 delete mode 100755 test-suite/coq-makefile/extend-subdirs/run.sh
 delete mode 100755 test-suite/coq-makefile/findlib-package/run.sh
 delete mode 100755 test-suite/coq-makefile/latex1/run.sh
 delete mode 100755 test-suite/coq-makefile/merlin1/run.sh
 delete mode 100755 test-suite/coq-makefile/mlpack1/run.sh
 delete mode 100755 test-suite/coq-makefile/mlpack2/run.sh
 delete mode 100755 test-suite/coq-makefile/multiroot/run.sh
 delete mode 100755 test-suite/coq-makefile/only/run.sh
 delete mode 100755 test-suite/coq-makefile/plugin1/run.sh
 delete mode 100755 test-suite/coq-makefile/plugin2/run.sh
 delete mode 100755 test-suite/coq-makefile/plugin3/run.sh
 delete mode 100755 test-suite/coq-makefile/quick2vo/run.sh
 delete mode 100755 test-suite/coq-makefile/timing/run.sh
 delete mode 100755 test-suite/coq-makefile/uninstall1/run.sh
 delete mode 100755 test-suite/coq-makefile/uninstall2/run.sh
 delete mode 100755 test-suite/coq-makefile/validate1/run.sh
 delete mode 100755 test-suite/coq-makefile/vio2vo/run.sh
 delete mode 100755 test-suite/misc/printers.sh

--- coq.orig/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
--- coq.orig/test-suite/coq-makefile/coqdoc1/run.sh
+++ /dev/null
@@ -1,76 +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
-
-# 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
-./test/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-./test/sub
-./test/sub/.coq-native
-./test/sub/.coq-native/Ntest_sub_testsub.cmi
-./test/sub/.coq-native/Ntest_sub_testsub.cmx
-./test/sub/.coq-native/Ntest_sub_testsub.cmxs
-./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
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test_plugin.cmi
-./test_plugin.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/coqdoc2/run.sh
+++ /dev/null
@@ -1,74 +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
-(
-  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
-./test/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-./test/sub
-./test/sub/.coq-native
-./test/sub/.coq-native/Ntest_sub_testsub.cmi
-./test/sub/.coq-native/Ntest_sub_testsub.cmx
-./test/sub/.coq-native/Ntest_sub_testsub.cmxs
-./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
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test_plugin.cmi
-./test_plugin.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/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
--- coq.orig/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"
--- coq.orig/test-suite/coq-makefile/findlib-package/run.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-
-. ../template/init.sh
-
-sed -i.old 's/coq-core.plugins.ltac/coq-core.plugins.ltac,foo/' src/META.coq-test-suite
-
-echo "let () = Foolib.foo ();;" >> src/test_aux.ml
-if which cygpath 2>/dev/null; then
-  # separator is ; on windows
-  OCAMLPATH=$OCAMLPATH;$(cygpath -m "$PWD"/findlib)
-else
-  OCAMLPATH=$OCAMLPATH:$PWD/findlib
-fi
-export OCAMLPATH
-make -C findlib/foo clean
-coq_makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-cat Makefile.local
-make -C findlib/foo
-make
-make byte
--- coq.orig/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
--- coq.orig/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
--- coq.orig/test-suite/coq-makefile/mlpack1/run.sh
+++ /dev/null
@@ -1,36 +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/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test_plugin.cmi
-./test_plugin.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/mlpack2/run.sh
+++ /dev/null
@@ -1,36 +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/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test_plugin.cmi
-./test_plugin.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/multiroot/run.sh
+++ /dev/null
@@ -1,78 +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
-(
-  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
-./test/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-./test2
-./test2/.coq-native
-./test2/.coq-native/Ntest2_test.cmi
-./test2/.coq-native/Ntest2_test.cmx
-./test2/.coq-native/Ntest2_test.cmxs
-./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
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test.cmi
-./test.cmx
-./test_aux.cmi
-./test_aux.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/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
--- coq.orig/test-suite/coq-makefile/plugin1/run.sh
+++ /dev/null
@@ -1,39 +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/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test.cmi
-./test.cmx
-./test_aux.cmi
-./test_aux.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/plugin2/run.sh
+++ /dev/null
@@ -1,39 +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/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test.cmi
-./test.cmx
-./test_aux.cmi
-./test_aux.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/plugin3/run.sh
+++ /dev/null
@@ -1,39 +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/.coq-native
-./test/.coq-native/Ntest_test.cmi
-./test/.coq-native/Ntest_test.cmx
-./test/.coq-native/Ntest_test.cmxs
-./test/test.glob
-./test/test.v
-./test/test.vo
-./test/test_plugin.cmxs
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired
-diff -u desired actual
-
-(cd "$(find tmp -name coq-test-suite)" && find .) | sort > actual
-sort > desired <<EOT
-.
-./META
-./test.cmi
-./test.cmx
-./test_aux.cmi
-./test_aux.cmx
-./test_plugin.cmxa
-./test_plugin.cmxs
-EOT
-diff -u desired actual
--- coq.orig/test-suite/coq-makefile/uninstall1/run.sh
+++ /dev/null
@@ -1,26 +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 -o -name coq-test-suite \) -print0)
-) | sort -u > actual
-sort -u > desired <<EOT
-.
-./test
-./test/sub
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired
-exec diff -u desired actual
--- coq.orig/test-suite/coq-makefile/uninstall2/run.sh
+++ /dev/null
@@ -1,26 +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
-.
-./test
-./test/sub
-EOT
-(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired
-exec diff -u desired actual
--- coq.orig/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
--- coq.orig/test-suite/misc/printers.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/sh
-
-command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; }
-
-f=$(mktemp)
-{
-    printf 'Drop.\n#go;;\nQuit.\n' | "${BIN}coqtop.byte" -q
-} 2>&1 | tee "$f"
-
-# if there's an issue in `include_utilities`, `#go;;` won't be mentioned
-# if there's an issue in `include_printers`, it will be an undefined printer
-if ! grep -q -F '#go;;' "$f" ||
-        grep -q -E -i 'Error|Unbound|Anomaly' "$f";
-then exit 1; fi