aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/archive/perf-analysis
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-15 13:32:36 +0100
committerThéo Zimmermann2019-03-15 13:32:36 +0100
commit0063c4c985078fd181c4a3a149ccbb06752edc97 (patch)
treebfc3d7dc243a921643e6ceb42bdcb2522a412053 /dev/doc/archive/perf-analysis
parent710a7cad94dcc9c734ab9ccc425f7a080dddc5f8 (diff)
Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder.
Diffstat (limited to 'dev/doc/archive/perf-analysis')
-rw-r--r--dev/doc/archive/perf-analysis167
1 files changed, 167 insertions, 0 deletions
diff --git a/dev/doc/archive/perf-analysis b/dev/doc/archive/perf-analysis
new file mode 100644
index 0000000000..ac54fa6f73
--- /dev/null
+++ b/dev/doc/archive/perf-analysis
@@ -0,0 +1,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)