[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

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

Attached is again sublist.hgbundle (but rebased w.r.t. the latest 
commits to the main repo, corresponding to changeset 8e124393c281) and 
sublist-afp.hgbundle (which is now also tested against JinjaThreads).

cheers

chris

-------------- next part --------------
A non-text attachment was scrubbed...
Name: sublist.hgbundle
Type: application/octet-stream
Size: 15225 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120831/c3130f2d/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sublist-afp.hgbundle
Type: application/octet-stream
Size: 10983 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120831/c3130f2d/attachment-0005.obj>