diff options
| -rw-r--r-- | test-suite/Makefile | 22 | ||||
| -rw-r--r-- | test-suite/misc/deps/A/A.v | 1 | ||||
| -rw-r--r-- | test-suite/misc/deps/B/A.v | 1 | ||||
| -rw-r--r-- | test-suite/misc/deps/B/B.v | 7 | ||||
| -rw-r--r-- | test-suite/misc/deps/checksum.v | 2 |
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. |