helm/software/components/ng_kernel/TEST

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