helm/software/components/ng_kernel/TEST

   1 CONTENUTO alluris.txt.OK:
   2
   3 matita
   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, huffmann, math_groups,
  17                         float, geometry
  18 Suresnes
  19 Utrecht
  20
  21 ++++++++++++++++
  22
  23 contrib di matita?
  24
  25 ++++++++++++++++
  26
  27 [CoRN: calcolo grafi da caricare troppo lento]
  28 [Coq: calcolo grafi da caricare troppo lento]
  29 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
  30
  31 CoRN: type-checking vecchio nucleo troppo lento
  32 Rocq/AILS: type-checking vecchio nucleo troppo lento
  33 Rocq/COC: type-checking vecchio nucleo troppo lento
  34 nijmegen: type-checking vecchio nucleo troppo lento
  35 Sophia-Antipolis/Float: vecchio nucleo troppo lento
  36 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
  37
  38 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
  39 orsay: nuovo nucleo diverge (vedi sopra)
  40 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
  41
  42 Sophia-Antipolis/huffmann: Unknown constant
  43 Sophia-Antipolis/MATH/GROUPS: Unknown constant
  44
  45 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ???
  46 Sophia-Antipolis/Algebra: vecchio nucleo variabili
  47 lyon/PROCESSES: vecchio nucleo, variabili
  48
  49 lannion: nuovo nucleo impredicative set
  50 rocq.higman: nuovo nucleo impredicative set
  51 lyon.impredicative_set: nuovo nucleo impredicative set
  52
  53 ============= IMPREDICATIVE SET ======================
  54 Lannion/Continuations
  55 Lyon/GraphBasics
  56 Lyon/Multiplier
  57 Lyon/CoinductiveExamples
  58 Lyon/Streams
  59 Rocq/Paradoxes: Hurkens e Russell
  60 Rocq/HistoricalExamples
  61 Rocq/HigmanNW
  62
  63 ============= BUG VECCHIO NUCLEO =======================
  64 Problema con permutazione ens?
  65 cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
  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))