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

[Makarius]

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


 	Makarius