helm/software/components/ng_kernel/TEST

   1 CONTENUTO alluris.txt.OK, NEW typing, OLD typing
   2
   3 matita       11.89 11.71                      tranne freescale e tests
   4 Coq                       fixpoints
   5 BellLabs      0.21  0.22
   6 Cachan                    .....
   7 Dyade                     fixpoints
   8 Eindhoven     0.23  0.85
   9 IdealX        0.05  0.06
  10 Lyon                      impredicative set
  11 Marseille     1.04  2.23
  12 Montevideo    1.90  4.29
  13 Muenchen      0.05  0.07
  14 Nancy         0.13  0.24
  15 Orsay                     fixpoints
  16 Paris         0.39  0.48
  17 Rocq                      impredicative set   tranne ails, coc, higman,
  18                                               ALGEBRA/CATEGORY_THEORY
  19 Sophia-Antipolis                              tranne algebra, buchberger,
  20                                               math_groups, float, geometry
  21 Suresnes                  fixpoints
  22 Utrecht       0.82  0.92
  23
  24 ++++++++++++++++
  25
  26 file bug_universi.ma: sbaglia a fare il ranking!
  27
  28 [CoRN: calcolo grafi da caricare troppo lento]
  29 [Coq: calcolo grafi da caricare troppo lento]
  30 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
  31
  32 CoRN: type-checking vecchio nucleo troppo lento
  33 Rocq/AILS: type-checking vecchio nucleo troppo lento
  34 Rocq/COC: type-checking vecchio nucleo troppo lento
  35 nijmegen: type-checking vecchio nucleo troppo lento
  36 Sophia-Antipolis/Float: vecchio nucleo troppo lento
  37 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
  38 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
  39
  40 matita/tests: nuovo nucleo problema con universi!!!
  41
  42 Sophia-Antipolis/Algebra: nuovo nucleo diverge
  43    cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
  44 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
  45    cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
  46 matita/freescale: nuovo nucleo molto piu' lento del vecchio?
  47
  48 lannion: nuovo nucleo impredicative set
  49 rocq.higman: nuovo nucleo impredicative set
  50 lyon.impredicative_set: nuovo nucleo impredicative set
  51
  52 ============= IMPREDICATIVE SET ======================
  53 Lannion/Continuations
  54 Lyon/GraphBasics
  55 Lyon/Multiplier
  56 Lyon/CoinductiveExamples
  57 Lyon/Streams
  58 Rocq/Paradoxes: Hurkens e Russell
  59 Rocq/HistoricalExamples
  60 Rocq/HigmanNW
  61
  62 ============= CONVERSIONE FIX GENERATIVI ================
  63 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
  64 Appl: wrong application of le_S_n: the parameter H1 has type
  65 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
  66 but it should have type
  67 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
  68
  69 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
  70 Appl: wrong application of ...
  71   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
  72     (pair (list Key) Data x0 x))
  73   (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
  74   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
  75     (pair (list Key) Data x0 x))
  76   (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
  77
  78 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
  79 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
  80   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
  81   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
  82 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
  83   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
  84 but it should have type
  85 In C (B2C (K2B (KeyAB d0 d1)))
  86   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
  87
  88 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
  89 Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
  90   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
  91   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
  92 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
  93   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
  94 but it should have type
  95 In C (B2C (K2B (KeyAB d0 d1)))
  96   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
  97
  98 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
  99 Branch for constructor xI :=
 100 λp0:positive.
 101  λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
 102 has type ∀p0: positive.
 103  ∀n: nat.
 104   eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
 105     (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
 106 not convertible with positive
 107  → (λp0:positive.
 108        ∀n: nat.
 109         eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
 110           (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
 111
 112 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
 113 has type ∀p0: positive.
 114  ∀m: nat.
 115   eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
 116     (plus (plus m (Pmult_nat p (plus m m)))
 117       (plus m (Pmult_nat p0 (plus m m))))
 118 not convertible with positive
 119  → (λp0:positive.
 120        ∀n: nat.
 121         eq nat (Pmult_nat (Pplus (xI p) p0) n)
 122           (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
 123
 124 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
 125 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
 126 not convertible with positive
 127  → (λp0:positive.
 128        eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
 129        (xI __1)
 130
 131 cic:/Coq/NArith/BinPos/Pplus_comm.con
 132 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
 133 not convertible with positive
 134  → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
 135        (xI __1)
 136
 137 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
 138 has type ∀p0: positive.
 139  eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
 140 not convertible with positive
 141  → (λp0:positive.
 142        eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
 143        (xI __1)
 144
 145 cic:/Coq/NArith/BinPos/Pplus_assoc.con
 146  eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
 147    (xI (Pplus (Pplus_carry x1 y0) z0))
 148 not convertible with positive
 149  → (λp:positive.
 150        eq positive (Pplus (xI x1) (Pplus (xI y0) p))
 151          (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
 152
 153 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
 154 has type ∀y1: positive.
 155  ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
 156   eq positive (xI x1) (xI y1)
 157 not convertible with positive
 158  → (λp:positive.
 159        eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
 160         → eq positive (xI x1) p) (xI __1)
 161
 162 cic:/Coq/NArith/BinPos/ZL10.con
 163 has type ∀q: positive.
 164  ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
 165   eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
 166 not convertible with positive
 167  → (λp0:positive.
 168        eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
 169         → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
 170       End: cic:/Coq/NArith/BinPos/ZL10.con
 171
 172 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
 173 has type ∀q: positive.
 174  ∀H: eq comparison (Pcompare p q Eq) Gt.
 175   ex positive
 176     (λh:positive.
 177       and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
 178         (and
 179           (eq positive
 180             match h return λp0:positive. positive
 181              [ xI ⇒ λy':positive. xO (Pplus_carry q y')
 182              | xO ⇒ λy':positive. xI (Pplus q y')
 183              | xH ⇒ xO (Psucc q)]  (xI p))
 184           (or (eq positive h xH)
 185             (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
 186               (IsPos (Ppred h))))))
 187 not convertible with positive
 188  → (λp0:positive.
 189        eq comparison (Pcompare (xI p) p0 Eq) Gt
 190         → ex positive
 191               (λh:positive.
 192                 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
 193                   (and (eq positive (Pplus p0 h) (xI p))
 194                     (or (eq positive h xH)
 195                       (eq positive_mask (Pminus_mask_carry (xI p) p0)
 196                         (IsPos (Ppred h))))))) (xI __1)
 197
 198 cic:/Coq/NArith/BinPos/Pplus_diag.con
 199 ∀x0: positive.
 200  ∀IHx: eq positive (Pplus x0 x0) (xO x0).
 201   eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
 202 but it should have type
 203 ∀p: positive.
 204  eq positive (Pplus p p) (xO p)
 205   → eq positive (Pplus (xI p) (xI p)) (xO (xI p))