[isabelle-dev] AFP statistics
Gerwin Klein
gerwin.klein at nicta.com.au
Tue May 17 12:28:22 CEST 2011
On 17/05/2011, at 7:56 PM, Makarius wrote:
On Tue, 17 May 2011, Alexander Krauss wrote:
>
>>> The plan is to move the afp test back to Munich when I'm in Munich in about two weeks. Then we should be back to the old routine.
>>> I'd prefer to run the test on a Linux machine. Is there one available with around 4 cores and lots of memory?
>>
>> Do 10GB already qualify? Then we can use lxbroy7/8, which are currently looking for a new job.
>
> It probably works if JinjaThreads is run with -M1. Some weeks ago I did some fine tuning in the management of futures within the theory loader, and JinjaThreads with -M4 or -M8 now needs "only" 16GB, instead of 24GB.
>
> It might actually work with less, but I did not try to squeeze it further yet.
Let's try lxbroy7/8 when I'm in town. Another few GB of memory could be quite cheap, so maybe a memory upgrade is an option as well.
Cheers,
Gerwin
More information about the isabelle-dev
mailing list