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



The options -M and -q in isabelle usedir govern the settings for multithreading.

Putting in your ~/.isabelle/etc/settings

ISABELLE_USEDIR_OPTIONS="-M 1 -q 0"

should do what you want. Random crashes on HOL are still disconcerting, though.

Cheers,
Gerwin


On 24/02/2010, at 1:01 PM, Thomas Sewell wrote:

> 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.
> 
> Multithreading seems to be mildly useful on my desktop machine at work, with cpu usage of 110-150% of one core being reported. On my desktop machine at home, though, it seems to cause random and unrepeatable build failures. More than 5  different attempts to build the HOL image failed 5 different ways, sometimes with a meaningful but unexpected exception being reported and sometimes with no explanation.
> 
> I've discovered the way to make progress is to tie up the other cores with useless work. These days I use a busy loop written in 10 lines of C code, although the original discovery involved Unreal Tournament. Interestingly PolyML's CPU usage still peaks at around 120% of one core - it must be getting CPU quota for 2 or 3 threads while my busy loop gets less. Curiously, this does not seem to create a problem, or at least, it's not so likely.
> 
> Anyway, is there an environment variable or ML reference I can tweak to disable threading for more reliable builds?
> 
> Yours,
>    Thomas.
> 






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