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