matita/components/ng_kernel/TEST

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