1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
Performance analysis (trunk repository)
---------------------------------------
Jun 7, 2010: delayed re-typing of Ltac instances in matching
(-1% on HighSchoolGeometry, -2% on JordanCurveTheorem)
Jun 4, 2010: improvement in eauto and type classes inference by removing
systematic preparation of debugging pretty-printing streams (std_ppcmds)
(-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk;
-6% in HighSchoolGeometry)
Apr 19, 2010: small improvement obtained by reducing evar instantiation
from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert,
-2% AreaMethod, -15% in Ssreflect)
Apr 17, 2010: small improvement obtained by not repeating unification
twice in auto (-2% in Compcert, -2% in Algebra)
Feb 15, 2010: Global decrease due to unicode inefficiency repaired
Jan 8, 2010: Global increase due to an inefficiency in unicode treatment
Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to
exact (generally not significative but, e.g., +25% on Subst, +8% on
ZFC, +5% on AreaMethod)
Oct 19, 2009: Change in modules (CoLoR +35%)
Aug 9, 2009: new files added in AreaMethod
May 21, 2008: New version of CoRN
(needs +84% more time to compile)
Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu)
(+28% CoRN)
Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug
fixes, control of zeta in rewrite, auto (??))
(-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg,
but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%)
Mar 11, 2008:
(+19% PersistentUnionFind wrt Mar 3, +21% Angles,
+270% Continuations between 7/3 and 18/4)
Mar 7, 2008:
(-10% PersistentUnionFind wrt Mar 3)
Feb 20, 2008: temporary 1-day slow down
(+64% LinAlg)
Feb 14, 2008:
(-10% PersistentUnionFind, -19% Groups)
Feb 7, 8, 2008: temporary 2-days long slow down
(+20 LinAlg, +50% BDDs)
Feb 2, 2008: many updates of the module system
(-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind,
-42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices)
Jan 1, 2008: merge of TypeClasses branch
(+8% PersistentUnionFind, +36% LinAlg, +76% Goedel)
Nov 16, 17, 2007:
(+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days)
Nov 8, 2007:
(+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL,
+220% SquareMatrices)
Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables)
Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the
tactic interpreter (from revision 10222 to 10267)
(+22% CoRN, +10% geometry, ...)
Sep 16, 2007:
(+16% PersistentUnionFind on 3 days, LinAlg stable,
Sep 4, 2007:
(+26% PersistentUnionFind, LinAlg stable,
Jun 6, 2007: optimization of the need for type unification in with-bindings
(-3.5% Stalmark, -6% Kildall)
May 20, 21, 22, 2007: improved inference of with-bindings (including activation
of unification on types)
(+4% PICALC, +5% Stalmark, +7% Kildall)
May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...)
Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's
computer (-25% CoRN, -25% Fairisle, ...)
Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions
(+4% in general during these two days)
Oct 17, 2006: improvement in new field [r9248]
(QArith -3%, geometry: -2%)
Oct 5, 2006: fixing wrong unification of Meta below binders
(e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%,
DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%)
Sep 26, 2006: new field [r9178-9181]
(QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it)
Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s)
Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s)
May 30, 2006: Nancy/CoLoR added (~ 319s)
May 23, 2006: new, lighter version of polymorphic inductive types
(CoRN: -27%, back to Mar-24 time)
May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -)
May 5, 2006: improvement in closure (array instead of lists)
(e.g. CatsInZFC: -10%, CoRN: -3%,
May 23, 2006: polymorphic inductive types (precise, heavy algorithm)
(CoRN: +37%)
Dec 29, 2005: new test and use of -vm in Stalmarck
Dec 27, 2005: contrib Karatsuba added (~ 30s)
Dec 28, 2005: size decrease
mainly due to Defined moved to Qed in FSets (reduction from 95M to 7Mo)
Dec 1-14, 2005: benchmarking server down
between the two dates: Godel: -10%, CoRN: -10%
probably due to changes around vm (new informative Cast,
change of equality in named_context_val)
Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 25s)
Aug 19, 2005: time decrease after application of "Array.length x=0" Xavier's
suggestions for optimisation
(e.g. Nijmegen/QArith: -3%, Nijmegen/CoRN: -7%, Godel: -3%)
Aug 1, 2005: contrib Kildall added (~ 65s)
Jul 26-Aug 2, 2005: bench down
Jul 14-15, 2005: 4 contribs failed including CoRN
Jul 14, 2005: time increase after activation of "closure optimisation"
(e.g. Nijmegen/QArith: +8%, Nijmegen/CoRN: +3%, Godel: +13%)
Jul 7, 2005: adding contrib Fermat4
Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 30s)
May 19, 2005: contrib Goodstein and prfx (~ 9s) added
Apr 21, 2005: strange time decrease
(could it be due to the change of Back and Reset mechanism)
(e.g. Nijmegen/CoRN: -2%, Nijmegen/QARITH: -4%, Godel: -11%)
Mar 20, 2005: fixed Logic.with_check bug
global time decrease (e.g. Nijmegen/CoRN: -3%, Nijmegen/QARITH: -1.5%)
Jan 31-Feb 8, 2005: small instability
(e.g. CoRN: ~2015s -> ~1999s -> ~2032s, Godel: ~340s -> ~370s)
Jan 13, 2005: contrib SumOfTwoSquare added (~ 38s)
|
