components/ng_kernel/TEST

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