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

[Makarius]

On Wed, 19 May 2010, Johannes Hölzl wrote:

> Am Montag, den 17.05.2010, 09:41 -0700 schrieb Brian Huffman:
> [..]
>> 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.
>
> Today I discoverd a simple procedure to speed up the build time of HOL:
> Set the heap size:
>  ML_OPTIONS="-H 1024"
>
> I had it set for a while now and the elapsed time was around 7 minutes.
> With -H 500 it is around 11 minutes. I always wondered why it was so
> fast on my machine, until I discovered that I had a different heap size.
>
> But setting the heap size is dangerous: I need to set it back to 500 as
> some AFP entries crash with a "Run out of store - interrupting threads"
> message. I assume that due to the big heap address space not enough
> address space is available for the thread stacks?
>
> - Johannes
>
> PS. My computer is a iMac9,1:
>  4GiB RAM
>  2x Core(TM)2 Duo CPU E8335 @ 2.93GHz
>  Running 32-bit Ubuntu

Yes, this tuning of the initial heap sizes can make a big difference.  It 
is indeed a bit delicate to get it right -- the defaults are "one size 
fits for all", such that it almost always works out of the box.

Apart from -H you can also specify --mutable and --immutable heap segments 
separately (otherwise -H will split it according to a hardwired ratio 
between the two).  E.g. "--mutable 500 --immutable 500" on x86-linux or 
x86-darwin.  The Mac OS platform allows for slightly larger total process 
sizes, so you could start a bit higher there.

On x86_64 you won't hit the "Run out of store" easily, but run into the 
typical thrashing when physical memory fills up.  We did not see this in 
the past few years, because the 32 address space of a process has become 
much smaller than physical memory.  With 64 bit addressing you are back to 
normal for the coming decades.


It might be worth doing some systematicy measurements how the two 
dimensions of --mutable and --immutable affect performance, but it will 
also vary according to the total heap utilization, as Isabelle/HOL or 
applications change over time.


 	Makarius