diff options
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 207f25ed0b..f1cb21ecd5 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 |