[isabelle-dev] Library/List_Prefix

[David Matthews]

On 31/08/2012 05:21, Christian Sternagel wrote:
> On 08/31/2012 12:44 PM, Gerwin Klein wrote:
>>
>> On 31/08/2012, at 1:25 PM, Christian Sternagel <c-sterna at jaist.ac.jp>
>> wrote:
>>
>>> Well, it almost worked now ;).
>>>
>>> even without -b all my memory was wasted and just as swapping started
>>> in earnest I got an error message, i.e., I have to adapt JinjaThreads
>>> to some previous changes.
>>>
>>> Still, I am nowhere close to the 3-4 GB RAM usage that seem to be
>>> possible. Maybe the reason is that I'm on x86_64?
>>
>> Yes, that'll be it. Memory usage on x86_64 is almost twice that of the
>> 32bit version (which makes sense if you think about it).
> Now that you mention it ... ;)
>
> With TypeComp adapted (only minor changes) JinjaThread succeeded while
> using 6-8 GB RAM (which magically corresponds to the 3-4 GB on an i386 ;)).

If you're using Poly/ML 5.5 from SVN it could well be worth setting the 
maximum heap size to about 80% of the available memory e.g.
--maxheap 7G
Basically, choose the largest value that will avoid swapping on your 
machine with whatever else you have running.  Commit 1579 has reduced 
the default maximum (without any --maxheap option) from 100% of the 
memory to 80%.

The new heap sizer in 5.5 will detect swapping and reduce the heap 
accordingly but it cannot know exactly how much memory is required by 
the operating system and anything else you are running so it requires 
some swapping activity to know it is at the limit.

The experiments Makarius and I were doing on x86_32 were on machines 
that had at least 4G of real memory so swapping was not an issue.  The 
limit was imposed by the address length and/or the operating system. 
Effectively the OS was setting a value for --maxheap below the memory size.

David