[isabelle-dev] Build time for Isabelle/HOL (was: Aquamacs emacs)

[Brian Huffman]

On Mon, May 17, 2010 at 7:43 AM, Makarius <makarius at sketis.net> wrote:
>
> Right now I am bisecting our repository as David suggested, which is an
> interesting experience because last year's Isabelle/HOL builds really fast
> (factor 2 compared to today).

A factor of 2 slowdown is quite significant, and also rather worrying.
Part of the difference can be attributed to sheer size (my HOL image
today is 123 MB, compared with 108 MB for 2009-1 and 89 MB for 2009)
but there is still a significant slowdown yet to be accounted for.

Are there any measurements we can do (e.g. profiling the entire build
of Isabelle/HOL) that could help determine the cause of the slowdown?
For libraries that haven't changed much in the last year, are their
build times slower by a similar factor? I don't think users would be
very pleased if the new version of Isabelle takes twice as long to
process their old theories. Perhaps only theory files that use certain
features (like defining type classes, maybe) are slowed down; how
could we test this?

- Brian