From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- test-suite/Makefile | 45 ++++++++++++++++++++----- test-suite/bugs/closed/shouldsucceed/2360.v | 13 +++++++ test-suite/bugs/closed/shouldsucceed/2375.v | 18 ++++++++++ test-suite/bugs/closed/shouldsucceed/2388.v | 10 ++++++ test-suite/failure/prop-set-proof-irrelevance.v | 12 +++++++ test-suite/misc/deps/client/bar.v | 11 ++++++ test-suite/misc/deps/client/foo.v | 1 + test-suite/misc/deps/deps.out | 1 + test-suite/misc/deps/lib/foo.v | 1 + test-suite/success/implicit.v | 21 ++++++++++++ test-suite/success/ltac.v | 32 ++++++++++++++++++ test-suite/success/unfold.v | 8 +++++ 12 files changed, 165 insertions(+), 8 deletions(-) create mode 100644 test-suite/bugs/closed/shouldsucceed/2360.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2375.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2388.v create mode 100644 test-suite/failure/prop-set-proof-irrelevance.v create mode 100644 test-suite/misc/deps/client/bar.v create mode 100644 test-suite/misc/deps/client/foo.v create mode 100644 test-suite/misc/deps/deps.out create mode 100644 test-suite/misc/deps/lib/foo.v (limited to 'test-suite') diff --git a/test-suite/Makefile b/test-suite/Makefile index 2503368f..62d443d0 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/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v new file mode 100644 index 00000000..4ae97c97 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -0,0 +1,13 @@ +(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) +Definition interp (etyp : nat -> Type) (p: nat) := etyp p. + +Record Value (etyp : nat -> Type) := Mk { + typ : nat; + value : interp etyp typ +}. + +Definition some_value (etyp : nat -> Type) : (Value etyp). +Proof. + intros. + Fail apply Mk. (* Check that it does not raise an anomaly *) + diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v new file mode 100644 index 00000000..c17c426c --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2375.v @@ -0,0 +1,18 @@ +(* In the following code, the (superfluous) lemma [lem] is responsible +for the failure of congruence. *) + +Definition f : nat -> Prop := fun x => True. + +Lemma lem : forall x, (True -> True) = ( True -> f x). +Proof. + intros. reflexivity. +Qed. + +Goal forall (x:nat), x = x. +Proof. + intros. + assert (lem := lem). + (*clear ax.*) + congruence. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v new file mode 100644 index 00000000..c7926711 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2388.v @@ -0,0 +1,10 @@ +(* Error message was not printed in the correct environment *) + +Fail Parameters (A:Prop) (a:A A). + +(* This is a variant (reported as part of bug #2347) *) + +Require Import EquivDec. +Fail Program Instance bool_eq_eqdec : EqDec bool eq := + {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. + diff --git a/test-suite/failure/prop-set-proof-irrelevance.v b/test-suite/failure/prop-set-proof-irrelevance.v new file mode 100644 index 00000000..ad494108 --- /dev/null +++ b/test-suite/failure/prop-set-proof-irrelevance.v @@ -0,0 +1,12 @@ +Require Import ProofIrrelevance. + +Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. + exact proof_irrelevance. +Qed. + +Lemma paradox : False. + assert (H : 0 <> 1) by discriminate. + apply H. + Fail apply proof_irrelevance. (* inlined version is rejected *) + apply proof_irrelevance_set. +Qed. diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v new file mode 100644 index 00000000..62969418 --- /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 00000000..fc82069e --- /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 00000000..68b48d60 --- /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 00000000..b745fbd4 --- /dev/null +++ b/test-suite/misc/deps/lib/foo.v @@ -0,0 +1 @@ +Definition a := 0. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 59e1a935..ce3e692f 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -86,3 +86,24 @@ Fixpoint plus n m {struct n} := | 0 => m | S p => S (plus p m) end. + +(* Check multiple implicit arguments signatures *) + +Implicit Arguments eq_refl [[A] [x]] [[A]]. + +Check eq_refl : 0 = 0. + +(* Check that notations preserve implicit (since 8.3) *) + +Parameter p : forall A, A -> forall n, n = 0 -> True. +Implicit Arguments p [A n]. +Notation Q := (p 0). +Check Q eq_refl. + +(* Check implicits with Context *) + +Section C. +Context {A:Set}. +Definition h (a:A) := a. +End C. +Check h 0. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index dfa41c82..02618c2c 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -243,3 +243,35 @@ test_open_match (forall z y, y + z = 0). reflexivity. apply I. Qed. + +(* Test regular failure when clear/intro breaks soundness of the + interpretation of terms in current environment *) + +Ltac g y := clear y; assert (y=y). +Goal forall x:nat, True. +intro x. +Fail g x. +Abort. + +Ltac h y := assert (y=y). +Goal forall x:nat, True. +intro x. +Fail clear x; f x. +Abort. + +(* Do not consider evars as unification holes in Ltac matching (and at + least not as holes unrelated to the original evars) + [Example adapted from Ynot code] + *) + +Ltac not_eq e1 e2 := + match e1 with + | e2 => fail 1 + | _ => idtac + end. + +Goal True. +evar(foo:nat). +let evval := eval compute in foo in not_eq evval 1. +let evval := eval compute in foo in not_eq 1 evval. +Abort. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 47ca0836..5649e2f7 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -13,3 +13,11 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. + +(* Check regular failure when statically existing ref does not exist + any longer at run time *) + +Goal let x := 0 in True. +intro x. +Fail (clear x; unfold x). +Abort. -- cgit v1.2.3