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