[isabelle-dev] Build time for Isabelle/HOL (was: Aquamacs emacs)
makarius at sketis.net
Wed May 19 16:32:04 CEST 2010
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.
More information about the isabelle-dev