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