From 98a927aefb6df05a957d94cf2fd22d88e9e6c6b6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 9 May 2017 21:48:43 +0200
Subject: Moving code for miscellaneous tests to specific files.

The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.

This avoids making the main Makefile more or more complex.

We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.

Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
---
 test-suite/misc/deps-order.sh | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100755 test-suite/misc/deps-order.sh

(limited to 'test-suite/misc/deps-order.sh')

diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
new file mode 100755
index 000000000..375b706f0
--- /dev/null
+++ b/test-suite/misc/deps-order.sh
@@ -0,0 +1,20 @@
+# Check that both coqdep and coqtop/coqc supports -R
+# Check that both coqdep and coqtop/coqc takes the later -R
+# See bugs 2242, 2337, 2339
+rm -f misc/deps/*/*.vo
+tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
+diff -u misc/deps/deps.out $tmpoutput 2>&1
+R=$?
+times
+$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
+$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
+$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1
+S=$?
+if [ $R = 0 -a $S = 0 ]; then
+    printf "coqdep and coqtop agree\n"
+    exit 0
+else
+    printf "coqdep and coqtop disagree\n"
+    exit 1
+fi
-- 
cgit v1.2.3