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

[Johannes Hölzl]

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