]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/TEST
removed spurious "
[helm.git] / helm / software / components / ng_kernel / TEST
1 CONTENUTO alluris.txt.OK, NEW typing, OLD typing
2
3 matita       11.89 11.71                      tranne freescale
4 Coq                       fixpoints
5 BellLabs      0.21  0.22
6 Cachan                    .....
7 Dyade                     fixpoints
8 Eindhoven     0.23  0.85
9 IdealX        0.05  0.06
10 Lyon                      impredicative set
11 Marseille     1.04  2.23
12 Montevideo    1.90  4.29
13 Muenchen      0.05  0.07
14 Nancy         0.13  0.24
15 Orsay                     fixpoints
16 Paris         0.39  0.48
17 Rocq                      impredicative set   tranne ails, coc, higman,
18                                               ALGEBRA/CATEGORY_THEORY
19 Sophia-Antipolis                              tranne algebra, buchberger,
20                                               math_groups, float, geometry
21 Suresnes                  fixpoints
22 Utrecht       0.82  0.92
23
24 ++++++++++++++++
25
26 TODO: Andrea mi ha cassato la parte sulla reentrance; secondo me quella e'
27 importante
28
29 ATTENZIONE: cosa succede con un PTS non full? Un (Prod : Type) non lo tipiamo,
30 ma tipiamo (Lambda : Type)!
31
32 file bug_universi.ma: sbaglia a fare il ranking!
33
34 [CoRN: calcolo grafi da caricare troppo lento]
35 [Coq: calcolo grafi da caricare troppo lento]
36 [Sophia-Antipolis: calcolo grafi da caricare troppo lento]
37
38 CoRN: type-checking vecchio nucleo troppo lento
39 Rocq/AILS: type-checking vecchio nucleo troppo lento
40 Rocq/COC: type-checking vecchio nucleo troppo lento
41 nijmegen: type-checking vecchio nucleo troppo lento
42 Sophia-Antipolis/Float: vecchio nucleo troppo lento
43 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
44 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
45
46 ## = diventato addirittura velocissimo dopo universi + proof irrelevance + altezze
47 ##Sophia-Antipolis/Algebra: nuovo nucleo diverge
48 ##   cic:/Sophia-Antipolis/Algebra/Sub_module/submodule_op.con
49 ##Sophia-Antipolis/Buchberger: nuovo nucleo diverge
50 ##   cic:/Sophia-Antipolis/Buchberger/BuchRed/redbuch_stable.con
51 matita/freescale: nuovo nucleo molto piu' lento del vecchio?
52
53 lannion: nuovo nucleo impredicative set
54 rocq.higman: nuovo nucleo impredicative set
55 lyon.impredicative_set: nuovo nucleo impredicative set
56
57 ============= IMPREDICATIVE SET ======================
58 Lannion/Continuations
59 Lyon/GraphBasics
60 Lyon/Multiplier
61 Lyon/CoinductiveExamples
62 Lyon/Streams
63 Rocq/Paradoxes: Hurkens e Russell
64 Rocq/HistoricalExamples
65 Rocq/HigmanNW
66
67 ============= CONVERSIONE FIX GENERATIVI ================
68 cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con
69 Appl: wrong application of le_S_n: the parameter H1 has type
70 le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0))
71 but it should have type
72 le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0))
73
74 cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con
75 Appl: wrong application of ...
76   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
77     (pair (list Key) Data x0 x))
78   (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or
79   (eq (prod (list Key) Data) (pair (list Key) Data lk d)
80     (pair (list Key) Data x0 x))
81   (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm)
82
83 cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con
84 Appl: wrong application of AlreadyIn1: the parameter or_introl (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   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
87 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
88   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
89 but it should have type
90 In C (B2C (K2B (KeyAB d0 d1)))
91   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB))
92
93 cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con
94 Appl: wrong application of AlreadyIn1: the parameter or_introl (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   (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type
97 or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1))))
98   (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
99 but it should have type
100 In C (B2C (K2B (KeyAB d0 d1)))
101   (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab))
102
103 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
104 Branch for constructor xI :=
105 λp0:positive.
106  λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
107 has type ∀p0: positive.
108  ∀n: nat.
109   eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
110     (plus n (Pmult_nat (Pplus_carry p p0) (plus n n)))
111 not convertible with positive
112  → (λp0:positive.
113        ∀n: nat.
114         eq nat (Pmult_nat (Pplus_carry (xI p) p0) n)
115           (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1)
116
117 cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con
118 has type ∀p0: positive.
119  ∀m: nat.
120   eq nat (Pmult_nat (Pplus_carry p p0) (plus m m))
121     (plus (plus m (Pmult_nat p (plus m m)))
122       (plus m (Pmult_nat p0 (plus m m))))
123 not convertible with positive
124  → (λp0:positive.
125        ∀n: nat.
126         eq nat (Pmult_nat (Pplus (xI p) p0) n)
127           (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1)
128
129 cic:/Coq/NArith/BinPos/Pplus_carry_spec.con
130 has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0))
131 not convertible with positive
132  → (λp0:positive.
133        eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0)))
134        (xI __1)
135
136 cic:/Coq/NArith/BinPos/Pplus_comm.con
137 has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p))
138 not convertible with positive
139  → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p)))
140        (xI __1)
141
142 cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con
143 has type ∀p0: positive.
144  eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0))
145 not convertible with positive
146  → (λp0:positive.
147        eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0)))
148        (xI __1)
149
150 cic:/Coq/NArith/BinPos/Pplus_assoc.con
151  eq positive (xI (Pplus x1 (Pplus_carry y0 z0)))
152    (xI (Pplus (Pplus_carry x1 y0) z0))
153 not convertible with positive
154  → (λp:positive.
155        eq positive (Pplus (xI x1) (Pplus (xI y0) p))
156          (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1)
157
158 cic:/Coq/NArith/BinPos/Pplus_reg_r.con
159 has type ∀y1: positive.
160  ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)).
161   eq positive (xI x1) (xI y1)
162 not convertible with positive
163  → (λp:positive.
164        eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0))
165         → eq positive (xI x1) p) (xI __1)
166
167 cic:/Coq/NArith/BinPos/ZL10.con
168 has type ∀q: positive.
169  ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH).
170   eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul
171 not convertible with positive
172  → (λp0:positive.
173        eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH)
174         → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1)
175       End: cic:/Coq/NArith/BinPos/ZL10.con
176
177 cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con
178 has type ∀q: positive.
179  ∀H: eq comparison (Pcompare p q Eq) Gt.
180   ex positive
181     (λh:positive.
182       and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h))
183         (and
184           (eq positive
185             match h return λp0:positive. positive
186              [ xI ⇒ λy':positive. xO (Pplus_carry q y')
187              | xO ⇒ λy':positive. xI (Pplus q y')
188              | xH ⇒ xO (Psucc q)]  (xI p))
189           (or (eq positive h xH)
190             (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q))
191               (IsPos (Ppred h))))))
192 not convertible with positive
193  → (λp0:positive.
194        eq comparison (Pcompare (xI p) p0 Eq) Gt
195         → ex positive
196               (λh:positive.
197                 and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h))
198                   (and (eq positive (Pplus p0 h) (xI p))
199                     (or (eq positive h xH)
200                       (eq positive_mask (Pminus_mask_carry (xI p) p0)
201                         (IsPos (Ppred h))))))) (xI __1)
202
203 cic:/Coq/NArith/BinPos/Pplus_diag.con
204 ∀x0: positive.
205  ∀IHx: eq positive (Pplus x0 x0) (xO x0).
206   eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0))
207 but it should have type
208 ∀p: positive.
209  eq positive (Pplus p p) (xO p)
210   → eq positive (Pplus (xI p) (xI p)) (xO (xI p))