diff options
Diffstat (limited to 'test-suite')
23 files changed, 250 insertions, 15 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1268ed14bc..ae426f0daf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -85,8 +85,10 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed +INTERACTIVE := interactive + VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm \ + output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc # All subsystems @@ -528,8 +530,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR f=`basename $*`; \ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ - diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ - grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \ + diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ + grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ if [ $$R = 0 -a $$S = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v new file mode 100644 index 0000000000..77bf169e18 --- /dev/null +++ b/test-suite/bugs/closed/5245.v @@ -0,0 +1,18 @@ +Set Primitive Projections. + +Record foo := Foo { + foo_car : Type; + foo_rel : foo_car -> foo_car -> Prop +}. +Arguments foo_rel : simpl never. + +Definition foo_fun {A B} := Foo (A -> B) (fun f g => forall x, f x = g x). + +Goal @foo_rel foo_fun (fun x : nat => x) (fun x => x). +Proof. +intros x; exact eq_refl. +Undo. +progress hnf; intros; exact eq_refl. +Undo. +unfold foo_rel. intros x. exact eq_refl. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v deleted file mode 100644 index fce671c754..0000000000 --- a/test-suite/bugs/closed/5469.v +++ /dev/null @@ -1,3 +0,0 @@ -(* Some problems with the special treatment of curly braces *) - -Reserved Notation "'a' { x }" (at level 0, format "'a' { x }"). diff --git a/test-suite/bugs/closed/5608.v b/test-suite/bugs/closed/5608.v new file mode 100644 index 0000000000..f02eae69c2 --- /dev/null +++ b/test-suite/bugs/closed/5608.v @@ -0,0 +1,33 @@ +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). +Reserved Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "T x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). + +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Inductive base_type := TZ | TWord (logsz : nat). +Inductive flat_type := Tbase (T : base_type) | Prod (A B : flat_type). +Context {var : base_type -> Type}. +Fixpoint interp_flat_type (interp_base_type : base_type -> Type) (t : +flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type interp_base_type x) (interp_flat_type +interp_base_type y) + end. +Inductive exprf : flat_type -> Type := +| Var {t} (v : var t) : exprf (Tbase t) +| LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type var tx -> exprf tC) : +exprf tC +| Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). +Global Arguments Var {_} _. +Global Arguments LetIn {_} _ {_} _. +Global Arguments Pair {_} _ {_} _. +Notation "T x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A +(fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Definition foo := + (fun x3 => + (LetIn (Var x3) (fun x18 : var TZ + => (Pair (Var x18) (Var x18))))). +Print foo. diff --git a/test-suite/bugs/closed/5683.v b/test-suite/bugs/closed/5683.v new file mode 100644 index 0000000000..b5c6a48ec0 --- /dev/null +++ b/test-suite/bugs/closed/5683.v @@ -0,0 +1,71 @@ +Require Import Program.Tactics. +Require Import FunctionalExtensionality. + +Inductive Succ A := +| Succ_O : Succ A +| Succ_S : A -> Succ A. +Arguments Succ_O {A}. +Arguments Succ_S {A} _. + +Inductive Zero : Type :=. + +Inductive ty := +| ty_nat : ty +| ty_arr : ty -> ty -> ty. + +Inductive term A := +| term_abs : ty -> term (Succ A) -> term A +| term_app : term A -> term A -> term A +| term_var : A -> term A +| term_nat : nat -> term A. +Arguments term_abs {A} _ _. +Arguments term_app {A} _ _. +Arguments term_var {A} _. +Arguments term_nat {A} _. + +Class Functor F := +{ + ret : forall {A}, A -> F A; + fmap : forall {A B}, (A -> B) -> F A -> F B; + fmap_id : forall {A} (fa : F A), fmap (@id A) fa = fa; + fmap_compose : forall {A B C} (fa : F A) (g : B -> C) (h : A -> B), fmap (fun +a => g (h a)) fa = fmap g (fmap h fa) +}. + +Class Monad M `{Functor M} := +{ + bind : forall {A B}, M A -> (A -> M B) -> M B; + ret_left_id : forall {A B} (a : A) (f : A -> M B), bind (ret a) f = f a; + ret_right_id : forall {A} (m : M A), bind m ret = m; + bind_assoc : forall {A B C} (m : M A) (f : A -> M B) (g : B -> M C), bind +(bind m f) g = bind m (fun x => bind (f x) g) +}. + +Instance Succ_Functor : Functor Succ. +Proof. + unshelve econstructor. + - intros A B f fa. + destruct fa. + + apply Succ_O. + + apply Succ_S. tauto. + - intros. apply Succ_S. assumption. + - intros A [|a]; reflexivity. + - intros A B C [|a] g h; reflexivity. +Defined. + +(* Anomaly: Not an arity *) +Program Fixpoint term_bind {A B} (tm : term A) (f : A -> term B) : term B := + let Succ_f (var : Succ A) := + match var with + | Succ_O => term_var Succ_O + | Succ_S var' => _ + end in + match tm with + | term_app tm1 tm2 => term_app (term_bind tm1 f) (term_bind tm2 f) + | term_abs ty body => term_abs ty (term_bind body Succ_f) + | term_var a => f a + | term_nat n => term_nat n + end. +Next Obligation. + intros. +Admitted. diff --git a/test-suite/bugs/closed/5697.v b/test-suite/bugs/closed/5697.v new file mode 100644 index 0000000000..c653f992af --- /dev/null +++ b/test-suite/bugs/closed/5697.v @@ -0,0 +1,19 @@ +Set Primitive Projections. + +Record foo : Type := Foo { foo_car: nat }. + +Goal forall x y : nat, x <> y -> Foo x <> Foo y. +Proof. +intros. +intros H'. +congruence. +Qed. + +Record bar (A : Type) : Type := Bar { bar_car: A }. + +Goal forall x y : nat, x <> y -> Bar nat x <> Bar nat y. +Proof. +intros. +intros H'. +congruence. +Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 39a7103d1b..40abb215e9 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local new file mode 100644 index 0000000000..0f4a7d9954 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META new file mode 100644 index 0000000000..ff5f1c7c96 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META @@ -0,0 +1,4 @@ +archive(byte)="foo.cma" +archive(native)="foo.cmxa" +linkopts="-linkall" +requires="str" diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile new file mode 100644 index 0000000000..31cf116652 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile @@ -0,0 +1,14 @@ +-include ../../Makefile.conf + +CO=$(COQMF_OCAMLFIND) opt +CB=$(COQMF_OCAMLFIND) ocamlc + +all: + $(CO) -c foolib.ml + $(CO) -a foolib.cmx -o foo.cmxa + $(CB) -c foolib.ml + $(CB) -a foolib.cmo -o foo.cma + $(CB) -c foo.mli # empty .mli file, to be understood + +clean: + rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml new file mode 100644 index 0000000000..81306fb89b --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml @@ -0,0 +1,2 @@ +let foo () = + assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3) diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh new file mode 100755 index 0000000000..a0d8a7fea7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 51669f28f5..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 51669f28f5..03df9cf050 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3bec11cb75..89bafe9ad1 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,6 +18,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index a9ae74fd67..e5dbfcb4be 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -1,3 +1,5 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set [<0, 2 >] : nat * nat * (nat * nat) [<0, 2 >] @@ -109,9 +111,14 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) -{0, 1} +{{0, 1}} : nat * nat -{0, 1, 2} +{{0, 1, 2}} : nat * (nat * nat) -{0, 1, 2, 3} +{{0, 1, 2, 3}} : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dee0f70f79..b1015137d6 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -1,4 +1,9 @@ (**********************************************************************) +(* Check precedence, spacing, etc. in printing with curly brackets *) + +Check {x|x=0}+{True/\False}+{forall x, x=0}. + +(**********************************************************************) (* Check printing of notations with several instances of a recursive pattern *) (* Was wrong but I could not trigger a problem due to the collision between *) (* different instances of ".." *) @@ -161,10 +166,23 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). -(**********************************************************************) (* Test recursive notations with the recursive pattern repeated on the right *) -Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). -Check {0,1}. -Check {0,1,2}. -Check {0,1,2,3}. +Notation "{{ x , .. , y , z }}" := (pair x .. (pair y z) ..). +Check {{0,1}}. +Check {{0,1,2}}. +Check {{0,1,2,3}}. + +(* Test printing of #5608 *) + +Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" + (at level 200, format "'letpair' x [1] = { A } ; '//' 'return' ( b0 , b1 , .. , b2 )"). +Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := + (let x:=a in ( .. (b0,b1) .., b2)). +Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 0ed5b524f3..4e36dec15b 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -16,3 +16,14 @@ eremember (S (S ?[x])). instantiate (x:=0). reflexivity. Qed. + +(* Don't know if it is good or not but the compatibility tells that + the asserted goal to prove is subject to beta-iota but not the + asserted hypothesis *) + +Goal True. +assert ((fun x => x) False). +Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) +2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) +Abort. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1d35f1ef6c..29e373eaa5 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -337,3 +337,14 @@ Goal True. evar (0=0). Abort. +(* Test location of hypothesis in "symmetry in H". This was broken in + 8.6 where H, when the oldest hyp, was moved at the place of most + recent hypothesis *) + +Goal 0=1 -> True -> True. +intros H H0. +symmetry in H. +(* H should be the first hypothesis *) +match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *) +exact (eq_refl H0). +Abort. |