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