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