aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/Makefile22
-rw-r--r--test-suite/misc/deps/A/A.v1
-rw-r--r--test-suite/misc/deps/B/A.v1
-rw-r--r--test-suite/misc/deps/B/B.v7
-rw-r--r--test-suite/misc/deps/checksum.v2
5 files changed, 32 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 207f25ed0..f1cb21ecd 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -361,7 +361,7 @@ modules/%.vo: modules/%.v
# Miscellaneous tests
#######################################################################
-misc: misc/deps-order.log misc/universes.log
+misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log
# Check that both coqdep and coqtop/coqc supports -R
# Check that both coqdep and coqtop/coqc takes the later -R
@@ -390,6 +390,26 @@ misc/deps-order.log:
rm $$tmpoutput; \
} > "$@"
+deps-checksum: misc/deps-checksum.log
+misc/deps-checksum.log:
+ @echo "TEST misc/deps-checksum"
+ $(HIDE){ \
+ echo $(call log_intro,deps-checksum); \
+ rm -f misc/deps/*/*.vo; \
+ $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \
+ $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \
+ $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \
+ $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
+ if [ $$? = 0 ]; then \
+ echo $(log_success); \
+ echo " misc/deps-checksum...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " misc/deps-checksum...Error!"; \
+ fi; \
+ } > "$@"
+
+
# Sort universes for the whole standard library
EXPECTED_UNIVERSES := 5
universes: misc/universes.log
diff --git a/test-suite/misc/deps/A/A.v b/test-suite/misc/deps/A/A.v
new file mode 100644
index 000000000..49aaf4a79
--- /dev/null
+++ b/test-suite/misc/deps/A/A.v
@@ -0,0 +1 @@
+Definition b := true.
diff --git a/test-suite/misc/deps/B/A.v b/test-suite/misc/deps/B/A.v
new file mode 100644
index 000000000..c01a30dca
--- /dev/null
+++ b/test-suite/misc/deps/B/A.v
@@ -0,0 +1 @@
+Definition b := false.
diff --git a/test-suite/misc/deps/B/B.v b/test-suite/misc/deps/B/B.v
new file mode 100644
index 000000000..f3cda70a9
--- /dev/null
+++ b/test-suite/misc/deps/B/B.v
@@ -0,0 +1,7 @@
+Require A.
+
+Definition c := A.b.
+Lemma foo : c = false.
+Proof.
+reflexivity.
+Qed.
diff --git a/test-suite/misc/deps/checksum.v b/test-suite/misc/deps/checksum.v
new file mode 100644
index 000000000..450045e4b
--- /dev/null
+++ b/test-suite/misc/deps/checksum.v
@@ -0,0 +1,2 @@
+Require Import A.
+Fail Require Import B.