coq/dev/doc/perf-analysis, branch master The formal proof system Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder. 2019-03-15T12:32:36+00:00 Théo Zimmermann 2019-03-15T12:32:36+00:00 0063c4c985078fd181c4a3a149ccbb06752edc97 






Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.
2010-06-09T10:08:53+00:00

herbelin

2010-06-09T10:08:53+00:00

cb586ea65a1ad38626b7481ff8b30007f488705d

Also updated perf-analysis file (the part of the commit that delays typing of
ltac instances seems to slightly improve a few contributions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13096 85f007b7-540e-0410-9357-904b9bb8a0f7





Also updated perf-analysis file (the part of the commit that delays typing of
ltac instances seems to slightly improve a few contributions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13096 85f007b7-540e-0410-9357-904b9bb8a0f7







Updated performance analysis file
2010-06-06T12:59:49+00:00

herbelin

2010-06-06T12:59:49+00:00

5cfed41826bb2c1cb6946bc53f56d93232c98011

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13079 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13079 85f007b7-540e-0410-9357-904b9bb8a0f7







Improved the efficiency of evars traverals thanks to a split of
2010-05-13T07:24:56+00:00

herbelin

2010-05-13T07:24:56+00:00

6cca4015db457f91b8eb9cf824f21246cbe7c6e6

evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7





evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7







Few misc. updates.
2010-01-04T14:07:59+00:00

herbelin

2010-01-04T14:07:59+00:00

883bea94e52fff9cee76894761d3704872d7a61d

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7







- Correction bug highlighting "Module" dans Coqide
2008-05-28T09:09:12+00:00

herbelin

2008-05-28T09:09:12+00:00

941bac504672283a351d9a90f40f66fee7268e7d

- Divers code mort (evarutil.ml, Bvector.v)
- MAJ perf-analysis



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7





- Divers code mort (evarutil.ml, Bvector.v)
- MAJ perf-analysis



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7







Quelques éléments de réflexion
2008-05-03T13:13:14+00:00

herbelin

2008-05-03T13:13:14+00:00

795fc3c75cb7966532c4337bdb0606b6ae1e32bd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10880 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10880 85f007b7-540e-0410-9357-904b9bb8a0f7







MAJ
2007-10-29T08:43:46+00:00

herbelin

2007-10-29T08:43:46+00:00

737f45c9362d1435f66889bad3fbce638c982643

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10268 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10268 85f007b7-540e-0410-9357-904b9bb8a0f7







MAJ
2007-05-21T07:35:31+00:00

herbelin

2007-05-21T07:35:31+00:00

79d1421ce90b7f3c0c6a719a93a87d36b3abdfcd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9844 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9844 85f007b7-540e-0410-9357-904b9bb8a0f7







MAJ
2006-11-19T10:42:51+00:00

herbelin

2006-11-19T10:42:51+00:00

20a39fbca7b31284929c19df5c7c24225448c378

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9390 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9390 85f007b7-540e-0410-9357-904b9bb8a0f7