diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 37 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 5 | ||||
| -rw-r--r-- | test-suite/success/goal_selector.v | 14 |
3 files changed, 47 insertions, 9 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 8239600b1d..9d84cd5c7d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -79,6 +79,8 @@ log_anomaly = "==========> FAILURE <==========" log_failure = "==========> FAILURE <==========" log_intro = "==========> TESTING $(1) <==========" +FAIL = >&2 echo 'FAILED $@' + ####################################################################### # Testing subsystems ####################################################################### @@ -115,25 +117,24 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace .lia.cache - $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" + rm -f trace .lia.cache output/MExtraction.out + $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>" $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ + -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ \) -print0 | xargs -0 rm -f distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f + $(SHOW) "RM <**/*.aux>" + $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f ####################################################################### # Per-subsystem targets ####################################################################### -define mkstamp -$(1): $(1).stamp ; @true -$(1).stamp: $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) ; \ - $(HIDE)touch $$@ +define vdeps +$(1): $(patsubst %.v,%.v.log,$(wildcard $(1)/*.v)) endef -$(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) +$(foreach S,$(VSUBSYSTEMS),$(eval $(call vdeps,$(S)))) ####################################################################### # Summary @@ -221,6 +222,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be closed, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -236,6 +238,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (bug seems to be opened, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -251,6 +254,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ + $(FAIL); \ else \ echo $(log_success); \ echo " $<...correctly prepared" ; \ @@ -269,6 +273,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %. else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -285,6 +290,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -299,6 +305,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be rejected)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -321,6 +328,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ } > "$@" @@ -363,6 +371,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ rm $$tmpexpected; \ @@ -379,6 +388,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should be accepted)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -411,6 +421,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error! (should run faster)"; \ + $(FAIL); \ fi; \ fi; \ } > "$@" @@ -428,6 +439,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG else \ echo $(log_failure); \ echo " $<...Good news! (wish seems to be granted, please check)"; \ + $(FAIL); \ fi; \ } > "$@" @@ -462,6 +474,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -480,6 +493,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -499,6 +513,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -517,6 +532,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ } > "$@" @@ -536,6 +552,7 @@ coqwc/%.v.log : coqwc/%.v else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ rm $$tmpoutput; \ } > "$@" @@ -556,6 +573,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh else \ echo $(log_failure); \ echo " $<...Error!"; \ + $(FAIL); \ fi; \ ) > "$@" @@ -580,5 +598,6 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR else \ echo $(log_failure); \ echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ fi; \ } > "$@" diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 5b13f35d57..253b48e4d9 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -421,3 +421,8 @@ Goal exists n : nat, n = n -> True. eexists. set (H := _ = _). Abort. + +(* Check interpretation of default evar instance in pretyping *) +(* (reported as bug #7356) *) + +Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 8681405175..0951c5c8d4 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x. Proof. intro H; eexists ?[x]; only [x]: exact True. 1: assumption. Qed. + +(* Strict focusing! *) +Set Default Goal Selector "!". + +Goal True -> True /\ True /\ True. +Proof. + intro. + split;only 2:split. + Fail exact I. + Fail !:exact I. + 1:exact I. + - !:exact H. + - exact I. +Qed. |