[isabelle-dev] Segmentation faults

David Matthews dm at prolingua.co.uk
Sun May 12 13:24:06 CEST 2013


On 11/05/2013 12:21, Tjark Weber wrote:
> On Thu, 2013-05-02 at 16:18 +0100, Lawrence Paulson wrote:
>> I am getting a lot of poly/ML segmentation faults, and they are making
>> it very difficult to do my work, especially as my theories take at
>> least 15 minutes to load. If it then simply crashes then I'm not
>> getting anywhere.
>>
>> Has anybody else had this problem with Poly/ML?
>
> Since nobody else replied: I do get occasional segfaults from Poly/ML
> (not only running Isabelle, but also other ML code). David Matthews is
> usually quite responsive to bug reports.

That's interesting.  Is there any way to establish a pattern to this? 
Does it happen with particular hardware/operating system?  It's almost 
impossible to debug problems like this unless there's some way I can 
reproduce them.

I notice you said you run "other ML code" since Larry also has both 
Isabelle and the Poly/ML distribution installed.  I had wondered if 
there could be some conflict; in particular the Isabelle version could 
be picking up the shared library from the Poly/ML distribution instead 
of its own.  The reverse is unlikely.

Anyway the more information I have the more likely I can do something.

David



More information about the isabelle-dev mailing list