[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