From 5e690404233e6c772c1d5ddc52142edf474953ac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 May 2017 21:47:12 +0200 Subject: Cleaning old untested not any more interesting testing files. --- test-suite/bench/lists-100.v | 107 ---------------------------- test-suite/bench/lists_100.v | 107 ---------------------------- test-suite/kernel/inds.mv | 3 - test-suite/misc/berardi_test.v | 153 ----------------------------------------- 4 files changed, 370 deletions(-) delete mode 100644 test-suite/bench/lists-100.v delete mode 100644 test-suite/bench/lists_100.v delete mode 100644 test-suite/kernel/inds.mv delete mode 100644 test-suite/misc/berardi_test.v diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v deleted file mode 100644 index 5c64716c72..0000000000 --- a/test-suite/bench/lists-100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v deleted file mode 100644 index 5c64716c72..0000000000 --- a/test-suite/bench/lists_100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv deleted file mode 100644 index bd1cc49f86..0000000000 --- a/test-suite/kernel/inds.mv +++ /dev/null @@ -1,3 +0,0 @@ -Inductive [] nat : Set := O : nat | S : nat->nat. -Check Construct nat 0 1. -Check Construct nat 0 2. diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v deleted file mode 100644 index a64db4dab7..0000000000 --- a/test-suite/misc/berardi_test.v +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > *) - -Set Implicit Arguments. - -Section Berardis_paradox. - -(** Excluded middle *) -Hypothesis EM : forall P:Prop, P \/ ~ P. - -(** Conditional on any proposition. *) -Definition IFProp (P B:Prop) (e1 e2:P) := - match EM B with - | or_introl _ => e1 - | or_intror _ => e2 - end. - -(** Axiom of choice applied to disjunction. - Provable in Coq because of dependent elimination. *) -Lemma AC_IF : - forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), - (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). -Proof. -intros P B e1 e2 Q p1 p2. -unfold IFProp. -case (EM B); assumption. -Qed. - - -(** We assume a type with two elements. They play the role of booleans. - The main theorem under the current assumptions is that [T=F] *) -Variable Bool : Prop. -Variable T : Bool. -Variable F : Bool. - -(** The powerset operator *) -Definition pow (P:Prop) := P -> Bool. - - -(** A piece of theory about retracts *) -Section Retracts. - -Variables A B : Prop. - -Record retract : Prop := - {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - -Record retract_cond : Prop := - {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - - -(** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. - -End Retracts. - -(** This lemma is basically a commutation of implication and existential - quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) - which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) - -Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). -Proof. -intros A B. -destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; - destruct hf; auto. -Qed. - - -(** The paradoxical set *) -Definition U := forall P:Prop, pow P. - -(** Bijection between [U] and [(pow U)] *) -Definition f (u:U) : pow U := u U. - -Definition g (h:pow U) : U := - fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). - -(** We deduce that the powerset of [U] is a retract of [U]. - This lemma is stated in Berardi's article, but is not used - afterwards. *) -Lemma retract_pow_U_U : retract (pow U) U. -Proof. -exists g f. -intro a. -unfold f, g; simpl. -apply AC. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. -Qed. - -(** Encoding of Russel's paradox *) - -(** The boolean negation. *) -Definition Not_b (b:Bool) := IFProp (b = T) F T. - -(** the set of elements not belonging to itself *) -Definition R : U := g (fun u:U => Not_b (u U u)). - - -Lemma not_has_fixpoint : R R = Not_b (R R). -Proof. -unfold R at 1. -unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). -trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. -Qed. - - -Theorem classical_proof_irrelevence : T = F. -Proof. -generalize not_has_fixpoint. -unfold Not_b. -apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. - -intros not_true is_true. -elim not_true; trivial. -Qed. - -End Berardis_paradox. -- cgit v1.2.3 From 7f17e151c0a2666263d3854c064acdfea29edf53 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 8 May 2017 17:19:22 +0200 Subject: Adding tests for testing exit status and #use"include". --- test-suite/.csdp.cache | Bin 89077 -> 89077 bytes test-suite/Makefile | 30 +++++++++++++++++++++++++++++- test-suite/misc/exitstatus/illtyped.v | 1 + 3 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 test-suite/misc/exitstatus/illtyped.v diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache index ba85286dd3..b99d80e95f 100644 Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed44..779f5455ae 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,6 +33,7 @@ LIB := $(shell cd ..; pwd) coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqc := $(coqtop) -compile @@ -405,7 +406,7 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log +misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R @@ -477,6 +478,33 @@ misc/universes.log: misc/universes/all_stdlib.v misc/universes/all_stdlib.v: cd .. && $(MAKE) test-suite/$@ +misc/printers.log: + @echo "TEST printers" + $(HIDE){ \ + echo $(call log_intro,$<); \ + printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \ + if [ $$R != 0 ]; then \ + echo $(log_success); \ + echo " misc/printers...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/printers...Error!"; \ + fi; \ + } > "$@" + +misc/exitstatus.log: + @echo "TEST exitstatus" + $(HIDE){ \ + echo $(call log_intro,$<); \ + $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \ + if [ $$R != 0 ]; then \ + echo $(log_success); \ + echo " misc/exitstatus...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/exitstatus...Error!"; \ + fi; \ + } > "$@" # IDE : some tests of backtracking for coqtop -ideslave diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v new file mode 100644 index 0000000000..df6bbb389c --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. -- cgit v1.2.3 From 63510329fae28f7a9d18935f24e3ebf0485dabc8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 8 May 2017 18:28:55 +0200 Subject: A more regular naming of variables in test-suite Makefile. --- test-suite/Makefile | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 779f5455ae..5d3c118445 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -31,12 +31,12 @@ BIN := ../bin/ LIB := $(shell cd ..; pwd) coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite -bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite -bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte -command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source -coqc := $(coqtop) -compile +coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source +coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) SHOW := $(if $(VERBOSE),@true,@echo) @@ -53,7 +53,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_ # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) -get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) +get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) bogomips:= @@ -220,7 +220,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -250,7 +250,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -421,8 +421,8 @@ misc/deps-order.log: $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ | head -n 1 > $$tmpoutput; \ diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ - $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ - $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ + $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ + $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ $(coqtop) -R misc/deps/lib 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 \ @@ -441,9 +441,9 @@ misc/deps-checksum.log: $(HIDE){ \ echo $(call log_intro,deps-checksum); \ rm -f misc/deps/*/*.vo; \ - $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \ + $(coqc) -R misc/deps/A A misc/deps/A/A.v; \ + $(coqc) -R misc/deps/B A misc/deps/B/A.v; \ + $(coqc) -R misc/deps/B A misc/deps/B/B.v; \ $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ @@ -461,8 +461,8 @@ universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" $(HIDE){ \ - $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ - $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \ + $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ + $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \ mv universes.txt misc/universes; \ N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ times; \ @@ -529,9 +529,9 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -quick -R vio vio $* 2>&1 && \ $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \ - $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ + $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -546,8 +546,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -R coqchk coqchk $* 2>&1 && \ - $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ + $(coqc) -R coqchk coqchk $* 2>&1 && \ + $(coqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ -- cgit v1.2.3 From 98a927aefb6df05a957d94cf2fd22d88e9e6c6b6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 May 2017 21:48:43 +0200 Subject: Moving code for miscellaneous tests to specific files. The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all. --- test-suite/Makefile | 102 +++++---------------------------------- test-suite/misc/deps-checksum.sh | 5 ++ test-suite/misc/deps-order.sh | 20 ++++++++ test-suite/misc/exitstatus.sh | 7 +++ test-suite/misc/printers.sh | 3 ++ test-suite/misc/universes.sh | 8 +++ 6 files changed, 54 insertions(+), 91 deletions(-) create mode 100755 test-suite/misc/deps-checksum.sh create mode 100755 test-suite/misc/deps-order.sh create mode 100755 test-suite/misc/exitstatus.sh create mode 100755 test-suite/misc/printers.sh create mode 100755 test-suite/misc/universes.sh diff --git a/test-suite/Makefile b/test-suite/Makefile index 5d3c118445..39ef05269f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -406,103 +406,23 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log - -# Check that both coqdep and coqtop/coqc supports -R -# Check that both coqdep and coqtop/coqc takes the later -R -# 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) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ - | head -n 1 > $$tmpoutput; \ - diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ - $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ - $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ - $(coqtop) -R misc/deps/lib 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; \ - } > "$@" - -deps-checksum: misc/deps-checksum.log -misc/deps-checksum.log: - @echo "TEST misc/deps-checksum" - $(HIDE){ \ - echo $(call log_intro,deps-checksum); \ - rm -f misc/deps/*/*.vo; \ - $(coqc) -R misc/deps/A A misc/deps/A/A.v; \ - $(coqc) -R misc/deps/B A misc/deps/B/A.v; \ - $(coqc) -R misc/deps/B A misc/deps/B/B.v; \ - $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ - if [ $$? = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-checksum...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-checksum...Error!"; \ - fi; \ - } > "$@" - +misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) -# Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 # Prop is not counted -universes: misc/universes.log -misc/universes.log: misc/universes/all_stdlib.v - @echo "TEST misc/universes" - $(HIDE){ \ - $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ - $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \ - mv universes.txt misc/universes; \ - N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ - times; \ - if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \ - echo $(log_success); \ - echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \ - else \ - echo $(log_failure); \ - echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \ - fi; \ - } > "$@" - -misc/universes/all_stdlib.v: - cd .. && $(MAKE) test-suite/$@ - -misc/printers.log: - @echo "TEST printers" - $(HIDE){ \ - echo $(call log_intro,$<); \ - printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \ - if [ $$R != 0 ]; then \ - echo $(log_success); \ - echo " misc/printers...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/printers...Error!"; \ - fi; \ - } > "$@" - -misc/exitstatus.log: - @echo "TEST exitstatus" +$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) + @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \ - if [ $$R != 0 ]; then \ + export coqc="$(coqc)"; \ + export coqtop="$(coqtop)"; \ + export coqdep="$(coqdep)"; \ + export coqtopbyte="$(coqtopbyte)"; \ + "$<" 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ echo $(log_success); \ - echo " misc/exitstatus...Ok"; \ + echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " misc/exitstatus...Error!"; \ + echo " $<...Error!"; \ fi; \ } > "$@" diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh new file mode 100755 index 0000000000..1e2afb7540 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,5 @@ +rm -f misc/deps/*/*.vo +$coqc -R misc/deps/A A misc/deps/A/A.v +$coqc -R misc/deps/B A misc/deps/B/A.v +$coqc -R misc/deps/B A misc/deps/B/B.v +$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh new file mode 100755 index 0000000000..375b706f0a --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,20 @@ +# Check that both coqdep and coqtop/coqc supports -R +# Check that both coqdep and coqtop/coqc takes the later -R +# See bugs 2242, 2337, 2339 +rm -f misc/deps/*/*.vo +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput +diff -u misc/deps/deps.out $tmpoutput 2>&1 +R=$? +times +$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 +$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +S=$? +if [ $R = 0 -a $S = 0 ]; then + printf "coqdep and coqtop agree\n" + exit 0 +else + printf "coqdep and coqtop disagree\n" + exit 1 +fi diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 0000000000..cea1de862f --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,7 @@ +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned $N.\n" +printf "On ill-typed input, coqc returned $P.\n" +if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 0000000000..c822d0eb37 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,3 @@ +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +if [ $? = 0 ]; then exit 1; else exit 0; fi + diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 0000000000..d87a86035c --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,8 @@ +# Sort universes for the whole standard library +EXPECTED_UNIVERSES=4 # Prop is not counted +$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 +$coqc -R misc/universes Universes misc/universes/universes 2>&1 +mv universes.txt misc/universes +N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` +printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi -- cgit v1.2.3