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 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 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
  42 Sophia-Antipolis/Algebra: vecchio nucleo variabili
  43 lyon.ok: 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 ============= 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))