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)
|