[isabelle-dev] Build time for Isabelle/HOL (was: Aquamacs emacs)
makarius at sketis.net
Mon May 17 20:48:29 CEST 2010
On Mon, 17 May 2010, Brian Huffman wrote:
> 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?
Concerning the concrete situation, I have already bisected the 3-4 steps
to be seen on http://isabelle.in.tum.de/devel/stats/at-poly.html some time
ago and Florian and Clemens know about the cause already -- they will find
ways to make it work again for the release. (Hopefully, we should be able
to converge this week or next week.)
In general, the sheer image size alone does not cause a performance
problem on "modern" systems, i.e. a nimble Mac Pro with several GB RAM and
several cores. On "regular" systems, say a 1-2 GB laptop that is a few
years old, it can easily spoil the user experience even now, if images
need to be rebuilt.
Some of our Cygwin tests are close to breakdown as well, e.g. main HOL or
HOL-Nominal-Examples sometimes don't work because of too little memory --
only 2 GB. Current Cygwin is inherently limited to 32bit, and this won't
change within the next few years. 64 bit Windows is in its infancy anyway,
only now some people notice that their address space is getting too small.
They probably will have to switch to Linux soon, because 64bit drivers for
Windows are still hard to get, i.e. Windows64 is much worse than Linux64
in that respect.
The good news is that 64bit Mac OS works very well, too. I have Snow
Leopard running in this special "64" boot mode since a couple of weeks,
with great success. I.e. it is faster, and it runs both 32bit and 64bit
applications as before. (Platform identification is quite delicate on Mac
OS though -- forget plain old "uname".)
More information about the isabelle-dev