helm/software/components/ng_kernel/TEST

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