Re: [isabelle] Any way to deactivate multithreading in Isabelle 2009-1?



Thanks for the advice everyone. Sorry for not consulting the System Manual first.

This was a poor error report - let me make it clear that I strongly suspect the combination of PolyML and my hardware is the issue. Some of the crashes are caused by assertion failures in PolyML itself, so Isabelle is not to blame. Memory usage doesn't seem to be the problem though - many of the crashes report a specific error rather than out of memory, and occur when more memory is available. Given time, I may try some other PolyML versions and see if that helps.

Yours,
    Thomas.
________________________________________
From: Alexander Krauss [krauss at in.tum.de]
Sent: Wednesday, February 24, 2010 7:47 PM
To: Jasmin Blanchette
Cc: Thomas Sewell; Isabelle Users ML
Subject: Re: [isabelle] Any way to deactivate multithreading in Isabelle        2009-1?

Hi Thomas,

>> Is there any simple way to deactivate multithreading in Isabelle? I'm
>> using Isabelle 2009-1 with PolyML 5.3, and I'm seeing multithreading
>> for the first time.
>
> I've seen it done as follows:
>
> ML {* Multithreading.max_threads := 1 *}
> ML {* Goal.parallel_proofs := 0 *}

Better use ISABELLE_USEDIR_OPTIONS in your .isabelle/etc/settings, then
you do not need to change the actual sources. The relevant options are
-M (number of threads) and -q (level of parallel proof checking). See
also Sect. 3.4 of the Isabelle System Manual, where these options are
described.

The failures you are experiencing might be a memory problem: Memory
usage grows with the number of cores used...

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.