diff options
20 files changed, 679 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1243.v b/test-suite/bugs/closed/shouldsucceed/1243.v new file mode 100644 index 000000000..7d6781db2 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1243.v @@ -0,0 +1,12 @@ +Require Import ZArith. +Require Import Arith. +Open Scope Z_scope. + +Theorem r_ex : (forall x y:nat, x + y = x + y)%nat. +Admitted. + +Theorem r_ex' : forall x y:nat, (x + y = x + y)%nat. +Admitted. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/shouldsucceed/1302.v new file mode 100644 index 000000000..e94dfcfb0 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1302.v @@ -0,0 +1,22 @@ +Module Type T. + +Parameter A : Type. + +Inductive L : Type := +| L0 : L (* without this constructor, it works right *) +| L1 : A -> L. + +End T. + +Axiom Tp : Type. + +Module TT : T. + +Definition A : Type := Tp. + +Inductive L : Type := +| L0 : L +| L1 : A -> L. + +End TT. + diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v new file mode 100644 index 000000000..d021107d1 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1419.v @@ -0,0 +1,8 @@ +Goal True. + set(a := 0). + set(b := a). + unfold a in b. + clear a. + Eval vm_compute in b. + trivial. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v new file mode 100644 index 000000000..d4e7cea81 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1446.v @@ -0,0 +1,20 @@ +Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false. +Proof. + destruct b;intros;trivial. + elim H. + exact (refl_equal true). +Qed. + +Section BUG. + + Variable b : bool. + Hypothesis H : b <> true. + Hypothesis H0 : b = true. + Hypothesis H1 : b <> true. + + Goal False. + rewrite (not_true_eq_false _ H) in * |-. + contradiction. + Qed. + +End BUG. diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v new file mode 100644 index 000000000..bd016c995 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1448.v @@ -0,0 +1,26 @@ +Require Import Relations. +Require Import Ring_theory. +Require Import Ring_base. + +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. + +Variable Req : R -> R -> Prop. + +Hypothesis Req_refl : reflexive _ Req. +Hypothesis Req_sym : symmetric _ Req. +Hypothesis Req_trans : transitive _ Req. + +Add Relation R Req + reflexivity proved by Req_refl + symmetry proved by Req_sym + transitivity proved by Req_trans + as Req_rel. + +Add Ring my_ring : my_ring_theory (abstract). diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/shouldsucceed/1477.v new file mode 100644 index 000000000..dfc8c3280 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1477.v @@ -0,0 +1,18 @@ +Inductive I : Set := + | A : nat -> nat -> I + | B : nat -> nat -> I. + +Definition foo1 (x:I) : nat := + match x with + | A a b | B a b => S b + end. + +Definition foo2 (x:I) : nat := + match x with + | A _ b | B b _ => S b + end. + +Definition foo (x:I) : nat := + match x with + | A a b | B b a => S b + end. diff --git a/test-suite/bugs/closed/shouldsucceed/1483.v b/test-suite/bugs/closed/shouldsucceed/1483.v new file mode 100644 index 000000000..a3d7f1683 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1483.v @@ -0,0 +1,10 @@ +Require Import BinPos. + +Definition P := (fun x : positive => x = xH). + +Goal forall (p q : positive), P q -> q = p -> P p. +intros; congruence. +Qed. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v new file mode 100644 index 000000000..32e6489c5 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1507.v @@ -0,0 +1,121 @@ +(* + Implementing reals a la Stolzenberg + + Danko Ilik, March 2007 + svn revision: $Id$ + + XField.v -- (unfinished) axiomatisation of the theories of real and + rational intervals. +*) + +Definition associative (A:Type)(op:A->A->A) := + forall x y z:A, op (op x y) z = op x (op y z). + +Definition commutative (A:Type)(op:A->A->A) := + forall x y:A, op x y = op y x. + +Definition trichotomous (A:Type)(R:A->A->Prop) := + forall x y:A, R x y \/ x=y \/ R y x. + +Definition relation (A:Type) := A -> A -> Prop. +Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x. +Definition transitive (A:Type)(R:relation A) := + forall x y z:A, R x y -> R y z -> R x z. +Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x. + +Record interval (X:Set)(le:X->X->Prop) : Set := + interval_make { + interval_left : X; + interval_right : X; + interval_nonempty : le interval_left interval_right + }. + +Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { + Icar := interval grnd le; + Iplus : Icar -> Icar -> Icar; + Imult : Icar -> Icar -> Icar; + Izero : Icar; + Ione : Icar; + Iopp : Icar -> Icar; + Iinv : Icar -> Icar; + Ic : Icar -> Icar -> Prop; (* consistency *) + (* monoids *) + Iplus_assoc : associative Icar Iplus; + Imult_assoc : associative Icar Imult; + (* abelian groups *) + Iplus_comm : commutative Icar Iplus; + Imult_comm : commutative Icar Imult; + Iplus_0_l : forall x:Icar, Ic (Iplus Izero x) x; + Iplus_0_r : forall x:Icar, Ic (Iplus x Izero) x; + Imult_0_l : forall x:Icar, Ic (Imult Ione x) x; + Imult_0_r : forall x:Icar, Ic (Imult x Ione) x; + Iplus_opp_r : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero); + Imult_inv_r : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione; + (* distributive laws *) + Imult_plus_distr_l : forall x x' y y' z z' z'', + Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' -> + Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z'')); + (* order and lattice structure *) + Ilt : Icar -> Icar -> Prop; + Ilc := fun (x y:Icar) => Ilt x y \/ Ic x y; + Isup : Icar -> Icar -> Icar; + Iinf : Icar -> Icar -> Icar; + Ilt_trans : transitive _ lt; + Ilt_trich : forall x y:Icar, Ilt x y \/ Ic x y \/ Ilt y x; + Isup_lub : forall x y z:Icar, Ilc x z -> Ilc y z -> Ilc (Isup x y) z; + Iinf_glb : forall x y z:Icar, Ilc x y -> Ilc x z -> Ilc x (Iinf y z); + (* order preserves operations? *) + (* properties of Ic *) + Ic_refl : reflexive _ Ic; + Ic_sym : symmetric _ Ic +}. + +Definition interval_set (X:Set)(le:X->X->Prop) := + (interval X le) -> Prop. (* can be Set as well *) +Check interval_set. +Check Ic. +Definition consistent (X:Set)(le:X->X->Prop)(TI:I X le)(p:interval_set X le) := + forall I J:interval X le, p I -> p J -> (Ic X le TI) I J. +Check consistent. +(* define 'fine' *) + +Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake { + Ncar := interval_set grnd le; + Nplus : Ncar -> Ncar -> Ncar; + Nmult : Ncar -> Ncar -> Ncar; + Nzero : Ncar; + None : Ncar; + Nopp : Ncar -> Ncar; + Ninv : Ncar -> Ncar; + Nc : Ncar -> Ncar -> Prop; (* Ncistency *) + (* monoids *) + Nplus_assoc : associative Ncar Nplus; + Nmult_assoc : associative Ncar Nmult; + (* abelian groups *) + Nplus_comm : commutative Ncar Nplus; + Nmult_comm : commutative Ncar Nmult; + Nplus_0_l : forall x:Ncar, Nc (Nplus Nzero x) x; + Nplus_0_r : forall x:Ncar, Nc (Nplus x Nzero) x; + Nmult_0_l : forall x:Ncar, Nc (Nmult None x) x; + Nmult_0_r : forall x:Ncar, Nc (Nmult x None) x; + Nplus_opp_r : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero); + Nmult_inv_r : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None; + (* distributive laws *) + Nmult_plus_distr_l : forall x x' y y' z z' z'', + Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' -> + Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z'')); + (* order and lattice structure *) + Nlt : Ncar -> Ncar -> Prop; + Nlc := fun (x y:Ncar) => Nlt x y \/ Nc x y; + Nsup : Ncar -> Ncar -> Ncar; + Ninf : Ncar -> Ncar -> Ncar; + Nlt_trans : transitive _ lt; + Nlt_trich : forall x y:Ncar, Nlt x y \/ Nc x y \/ Nlt y x; + Nsup_lub : forall x y z:Ncar, Nlc x z -> Nlc y z -> Nlc (Nsup x y) z; + Ninf_glb : forall x y z:Ncar, Nlc x y -> Nlc x z -> Nlc x (Ninf y z); + (* order preserves operations? *) + (* properties of Nc *) + Nc_refl : reflexive _ Nc; + Nc_sym : symmetric _ Nc +}. + diff --git a/test-suite/bugs/closed/shouldsucceed/1519.v b/test-suite/bugs/closed/shouldsucceed/1519.v new file mode 100644 index 000000000..66bab241d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1519.v @@ -0,0 +1,14 @@ +Section S. + + Variable A:Prop. + Variable W:A. + + Remark T: A -> A. + intro Z. + rename W into Z_. + rename Z into W. + rename Z_ into Z. + exact Z. + Qed. + +End S. diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v new file mode 100644 index 000000000..9f10f7490 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1568.v @@ -0,0 +1,13 @@ +CoInductive A: Set := + mk_A: B -> A +with B: Set := + mk_B: A -> B. + +CoFixpoint a:A := mk_A b +with b:B := mk_B a. + +Goal b = match a with mk_A a1 => a1 end. + simpl. reflexivity. +Qed. + + diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v new file mode 100644 index 000000000..c9ebbd142 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1576.v @@ -0,0 +1,38 @@ +Module Type TA. +Parameter t : Set. +End TA. + +Module Type TB. +Declare Module A: TA. +End TB. + +Module Type TC. +Declare Module B : TB. +End TC. + +Module Type TD. + +Declare Module B: TB . +Declare Module C: TC + with Module B := B . +End TD. + +Module Type TE. +Declare Module D : TD. +End TE. + +Module Type TF. +Declare Module E: TE. +End TF. + +Module G (D: TD). +Module B' := D.C.B. +End G. + +Module H (F: TF). +Module I := G(F.E.D). +End H. + +Declare Module F: TF. +Module K := H(F). + diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v new file mode 100644 index 000000000..47953a66f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1582.v @@ -0,0 +1,15 @@ +Require Import Peano_dec. + +Definition fact_F : + forall (n:nat), + (forall m, m<n -> nat) -> + nat. +refine + (fun n fact_rec => + if eq_nat_dec n 0 then + 1 + else + let fn := fact_rec (n-1) _ in + n * fn). +Admitted. + diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v new file mode 100644 index 000000000..a90290bfb --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1618.v @@ -0,0 +1,23 @@ +Inductive A: Set := +| A1: nat -> A. + +Definition A_size (a: A) : nat := + match a with + | A1 n => 0 + end. + +Require Import Recdef. + +Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a := + match a return (P a) with + | A1 n => f n + end. + + +Function n1 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {measure A_size a} : +P +a := + match a return (P a) with + | A1 n => f n + end. + diff --git a/test-suite/bugs/closed/shouldsucceed/348.v b/test-suite/bugs/closed/shouldsucceed/348.v new file mode 100644 index 000000000..28cc5cb1e --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/348.v @@ -0,0 +1,13 @@ +Module Type S. + Parameter empty: Set. +End S. + +Module D (M:S). + Import M. + Definition empty:=nat. +End D. + +Module D' (M:S). + Import M. + Definition empty:Set. exact nat. Save. +End D'. diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v new file mode 100644 index 000000000..7bc04b1fe --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/38.v @@ -0,0 +1,22 @@ +Require Import Setoid. + +Variable A : Set. + +Inductive liste : Set := +| vide : liste +| c : A -> liste -> liste. + +Inductive e : A -> liste -> Prop := +| ec : forall (x : A) (l : liste), e x (c x l) +| ee : forall (x y : A) (l : liste), e x l -> e x (c y l). + +Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m. + +Definition same_refl (x:liste) : (same x x). + unfold same; split; intros; trivial. +Save. + +Goal forall (x:liste), (same x x). + intro. + apply (same_refl x). +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/545.v b/test-suite/bugs/closed/shouldsucceed/545.v new file mode 100644 index 000000000..926af7dd1 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/545.v @@ -0,0 +1,5 @@ +Require Export Reals. + +Parameter toto : nat -> nat -> nat. + +Notation " e # f " := (toto e f) (at level 30, f at level 0). diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v new file mode 100644 index 000000000..a963b225f --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/846.v @@ -0,0 +1,213 @@ +Set Implicit Arguments. + +Open Scope type_scope. + +Inductive One : Set := inOne: One. + +Definition maybe: forall A B:Set,(A -> B) -> One + A -> One + B. +Proof. + intros A B f c. + case c. + left; assumption. + right; apply f; assumption. +Defined. + +Definition id (A:Set)(a:A):=a. + +Definition LamF (X: Set -> Set)(A:Set) :Set := + A + (X A)*(X A) + X(One + A). + +Definition LamF' (X: Set -> Set)(A:Set) :Set := + LamF X A. + +Require Import List. +Require Import Bool. + +Definition index := list bool. + +Inductive L (A:Set) : index -> Set := + initL: A -> L A nil + | pluslL: forall l:index, One -> L A (false::l) + | plusrL: forall l:index, L A l -> L A (false::l) + | varL: forall l:index, L A l -> L A (true::l) + | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l) + | absL: forall l:index, L A (true::false::l) -> L A (true::l). + +Scheme L_rec_simp := Minimality for L Sort Set. + +Definition Lam' (A:Set) := L A (true::nil). + +Definition aczelapp: forall (l1 l2: index)(A:Set), L (L A l2) l1 -> L A + (l1++l2). +Proof. + intros l1 l2 A. + generalize l1. + clear l1. + (* Check (fun i:index => L A (i++l2)). *) + apply (L_rec_simp (A:=L A l2) (fun i:index => L A (i++l2))). + trivial. + intros l o. + simpl app. + apply pluslL; assumption. + intros l _ t. + simpl app. + apply plusrL; assumption. + intros l _ t. + simpl app. + apply varL; assumption. + intros l _ t1 _ t2. + simpl app in *|-*. + Check 0. + apply appL; [exact t1| exact t2]. + intros l _ t. + simpl app in *|-*. + Check 0. + apply absL; assumption. +Defined. + +Definition monL: forall (l:index)(A:Set)(B:Set), (A->B) -> L A l -> L B l. +Proof. + intros l A B f. + intro t. + elim t. + intro a. + exact (initL (f a)). + intros i u. + exact (pluslL _ _ u). + intros i _ r. + exact (plusrL r). + intros i _ r. + exact (varL r). + intros i _ r1 _ r2. + exact (appL r1 r2). + intros i _ r. + exact (absL r). +Defined. + +Definition lam': forall (A B:Set), (A -> B) -> Lam' A -> Lam' B. +Proof. + intros A B f t. + unfold Lam' in *|-*. + Check 0. + exact (monL f t). +Defined. + +Definition inLam': forall A:Set, LamF' Lam' A -> Lam' A. +Proof. + intros A [[a|[t1 t2]]|r]. + unfold Lam'. + exact (varL (initL a)). + exact (appL t1 t2). + unfold Lam' in * |- *. + Check 0. + apply absL. + change (L A ((true::nil) ++ (false::nil))). + apply aczelapp. + (* Check (fun x:One + A => (match (maybe (fun a:A => initL a) x) with + | inl u => pluslL _ _ u + | inr t' => plusrL t' end)). *) + exact (monL (fun x:One + A => + (match (maybe (fun a:A => initL a) x) with + | inl u => pluslL _ _ u + | inr t' => plusrL t' end)) r). +Defined. + +Section minimal. + +Definition sub1 (F G: Set -> Set):= forall A:Set, F A->G A. +Hypothesis G: Set -> Set. +Hypothesis step: sub1 (LamF' G) G. + +Fixpoint L'(A:Set)(i:index){struct i} : Set := + match i with + nil => A + | false::l => One + L' A l + | true::l => G (L' A l) + end. + +Definition LinL': forall (A:Set)(i:index), L A i -> L' A i. +Proof. + intros A i t. + elim t. + intro a. + unfold L'. + assumption. + intros l u. + left; assumption. + intros l _ r. + right; assumption. + intros l _ r. + apply (step (A:=L' A l)). + exact (inl _ (inl _ r)). + intros l _ r1 _ r2. + apply (step (A:=L' A l)). + (* unfold L' in * |- *. + Check 0. *) + exact (inl _ (inr _ (pair r1 r2))). + intros l _ r. + apply (step (A:=L' A l)). + exact (inr _ r). +Defined. + +Definition L'inG: forall A: Set, L' A (true::nil) -> G A. +Proof. + intros A t. + unfold L' in t. + assumption. +Defined. + +Definition Itbasic: sub1 Lam' G. +Proof. + intros A t. + apply L'inG. + unfold Lam' in t. + exact (LinL' t). +Defined. + +End minimal. + +Definition recid := Itbasic inLam'. + +Definition L'Lam'inL: forall (i:index)(A:Set), L' Lam' A i -> L A i. +Proof. + intros i A t. + induction i. + unfold L' in t. + apply initL. + assumption. + induction a. + simpl L' in t. + apply (aczelapp (l1:=true::nil) (l2:=i)). + exact (lam' IHi t). + simpl L' in t. + induction t. + exact (pluslL _ _ a). + exact (plusrL (IHi b)). +Defined. + + +Lemma recidgen: forall(A:Set)(i:index)(t:L A i), L'Lam'inL i A (LinL' inLam' t) + = t. +Proof. + intros A i t. + induction t. + trivial. + trivial. + simpl. + rewrite IHt. + trivial. + simpl L'Lam'inL. + rewrite IHt. + trivial. + simpl L'Lam'inL. + simpl L'Lam'inL in IHt1. + unfold lam' in IHt1. + simpl L'Lam'inL in IHt2. + unfold lam' in IHt2. + + (* going on. This fails for the original solution. *) + rewrite IHt1. + rewrite IHt2. + trivial. +Abort. (* one goal still left *) + diff --git a/test-suite/bugs/closed/shouldsucceed/931.v b/test-suite/bugs/closed/shouldsucceed/931.v new file mode 100644 index 000000000..21f15e721 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/931.v @@ -0,0 +1,7 @@ +Parameter P : forall n : nat, n=n -> Prop. + +Goal Prop. + refine (P _ _). + instantiate (1:=0). + trivial. +Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1680.v b/test-suite/bugs/opened/shouldnotfail/1680.v new file mode 100644 index 000000000..524c7bab4 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1680.v @@ -0,0 +1,9 @@ +Ltac int1 := let h := fresh in intro h. + +Goal nat -> nat -> True. + let h' := fresh in (let h := fresh in intro h); intro h'. + Restart. let h' := fresh in int1; intro h'. + trivial. +Qed. + + diff --git a/test-suite/check b/test-suite/check index 504e96cc2..907b773c4 100755 --- a/test-suite/check +++ b/test-suite/check @@ -145,12 +145,82 @@ test_complexity() { fi } +test_bugs () { + # Process verifications concerning submitted bugs. A message is + # printed for all opened bugs (still active or seem to be closed. + # For closed bugs that behave as expected, no message is printed + + # All files are assumed to have <# of the bug>.v as a name + + echo "Testing opened bugs..." + # We first test opened bugs that should not succeed + files=`/bin/ls -1 $1/opened/shoulnotsucceed/*.v 2> /dev/null` + for f in $files; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f $2 > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "still active" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (bug seems to be closed, please check)" + fi + done + + # And opened bugs that should not fail + files=`/bin/ls -1 $1/opened/shouldnotfail/*.v 2> /dev/null` + for f in $files; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f > /dev/null 2>&1 + if [ $? != 0 ]; then + echo "still active" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (bug seems to be closed, please check)" + fi + done + + echo "Testing closed bugs..." + # Then closed bugs that should succeed + files=`/bin/ls -1 $1/closed/shouldsucceed/*.v 2> /dev/null` + for f in $files; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f $2 > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (bug seems to be opened, please check)" + fi + done + + + # At last, we test closed bugs that should fail + files=`/bin/ls -1 $1/bugs/closed/shouldfail/*.v 2> /dev/null` + for f in $files; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command $f > /dev/null 2>&1 + if [ $? != 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (bug seems to be opend, please check)" + fi + done + +} + # Programme principal echo "Success tests" test_success success echo "Failure tests" test_failure failure +echo "Bugs test" +test_bugs bugs echo "Output tests" test_output output echo "Parser tests" |