diff options
| author | Maxime Dénès | 2016-07-04 16:17:41 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 16:17:41 +0200 |
| commit | c78b84425be7535e46c63e80200c07a1921e67bd (patch) | |
| tree | 0ea661c36ca1da6966b12b1d6c3389c9c020ffc5 /test-suite/Makefile | |
| parent | 9468bcd39808f4587d3732f46773b1e339b2267c (diff) | |
| parent | c22f6694bac3479426cf179839430d9d8675e456 (diff) | |
Merge branch 'v8.5' into trunk
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 d779d1f9a4..81321729d4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -360,7 +360,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 @@ -389,6 +389,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 := 4 # Prop is not counted universes: misc/universes.log |