diff options
-rw-r--r-- | test-suite/Makefile | 45 | ||||
-rw-r--r-- | test-suite/misc/deps/client/bar.v | 11 | ||||
-rw-r--r-- | test-suite/misc/deps/client/foo.v | 1 | ||||
-rw-r--r-- | test-suite/misc/deps/deps.out | 1 | ||||
-rw-r--r-- | test-suite/misc/deps/lib/foo.v | 1 | ||||
-rw-r--r-- | tools/coqdep_common.ml | 2 |
6 files changed, 52 insertions, 9 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 2503368f6..62d443d09 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ endif command := $(coqtop) -top Top -load-vernac-source coqc := $(coqtop) -compile +coqdep := $(BIN)coqdep SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) @@ -74,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) xml bugs +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ####################################################################### # Phony targets @@ -114,7 +115,6 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) # Summary ####################################################################### -summary_one = echo $(1); if [ -f $(2).log ]; then tail -n1 $(2).log; fi | sort -g summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g .PHONY: summary summary.log @@ -128,7 +128,7 @@ summary: $(call summary_dir, "Output tests", output); \ $(call summary_dir, "Interactive tests", interactive); \ $(call summary_dir, "Micromega tests", micromega); \ - $(call summary_one, "Miscellaneous tests", xml); \ + $(call summary_dir, "Miscellaneous tests", misc); \ $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ @@ -354,10 +354,12 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik. # Miscellaneous tests ####################################################################### +misc: misc/xml.log misc/deps-order.log + # Test xml compilation -xml: xml.log -xml.log: - @echo "TEST xml" +xml: misc/xml.log +misc/xml.log: + @echo "TEST misc/xml" $(HIDE){ \ echo $(call log_intro,xml); \ rm -rf misc/xml; \ @@ -365,9 +367,36 @@ xml.log: $(bincoqc) -xml misc/berardi_test 2>&1; times; \ if [ ! -d misc/xml ]; then \ echo $(log_failure); \ - echo " xml... failed"; \ + echo " misc/xml... failed"; \ else \ echo $(log_success); \ - echo " xml...apparently ok"; \ + echo " misc/xml...apparently ok"; \ fi; rm -r misc/xml; \ } > "$@" + +# Check that both coqdep and coqtop/coqc takes the later -I/-R +# Check that both coqdep and coqtop/coqc supports both -R and -I dir -as lib +# See bugs 2242, 2337, 2339 +deps-order: misc/deps-order.log +misc/deps-order.log: + @echo "TEST misc/deps-order" + $(HIDE){ \ + echo $(call log_intro,deps-order); \ + rm -f misc/deps/*/*.vo; \ + tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ + $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ + | head -n 1 > $$tmpoutput; \ + diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \ + $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \ + $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ + $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ + S=$$?; times; \ + if [ $$R = 0 -a $$S = 0 ]; then \ + echo $(log_success); \ + echo " misc/deps-order...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/deps-order...Error! (unexpected order)"; \ + fi; \ + rm $$tmpoutput; \ + } > "$@" diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v new file mode 100644 index 000000000..629694186 --- /dev/null +++ b/test-suite/misc/deps/client/bar.v @@ -0,0 +1,11 @@ +(* We assume the file compiled with -R ../lib lib -R . client *) +(* foo alone should refer to client.foo because -R . client comes last *) + +Require Import foo. +Goal a = 1. +reflexivity. +Qed. +Require Import lib.foo. +Goal a = 0. +reflexivity. +Qed. diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v new file mode 100644 index 000000000..fc82069e5 --- /dev/null +++ b/test-suite/misc/deps/client/foo.v @@ -0,0 +1 @@ +Definition a := 1. diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out new file mode 100644 index 000000000..68b48d604 --- /dev/null +++ b/test-suite/misc/deps/deps.out @@ -0,0 +1 @@ +misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v new file mode 100644 index 000000000..b745fbd48 --- /dev/null +++ b/test-suite/misc/deps/lib/foo.v @@ -0,0 +1 @@ +Definition a := 0. diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 797c25ccc..a2d908339 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -137,7 +137,7 @@ let warning_clash file dir = let d2 = Filename.dirname f2 in let dl = List.map Filename.dirname (List.rev fl) in eprintf - "*** Warning: in file %s, \n required library %s is ambiguous!\n (found %s.v in " + "*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in " file (String.concat "." dir) f; List.iter (fun s -> eprintf "%s, " s) dl; eprintf "%s and %s; used the latter)\n" d2 d1 |