diff options
| author | Maxime Dénès | 2016-07-04 09:51:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 13:30:15 +0200 |
| commit | 2ce64cc3124d30dbd42324c345cec378ccd66106 (patch) | |
| tree | 5956f1cbb5dd4d0942776f099ab0d7f66d4c3292 /test-suite/Makefile | |
| parent | 5832742143fbb3ecd72044d426bfafaa3d3ce47e (diff) | |
test-suite: test checking of libraries checksum.
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 |