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