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