[isabelle-dev] Segmentation faults

[Lawrence Paulson]

It clearly isn't a hardware failure. For one thing, it happens in the same way on two separate machines, and anyway, a hardware failure wouldn't affect only one specific program. David Matthews thought the problem may be the presence of a separate Poly/ML compiler, which I use for MetiTarski work. He thought perhaps the libraries could be interfering.

I recompiled Poly/ML with shared libraries off and it seems to be a bit more stable.

Larry

On 27 May 2013, at 15:25, Makarius <makarius at sketis.net> wrote:

> On Thu, 2 May 2013, 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.
> 
> Does this still happen?  There have not been any changes of our Poly/ML compilation since the Isabelle2013 release.
> 
> From a distance I would guess it is either a hardware failure, or something that Apple put on your machine as OS update, which now breaks the Isabelle polyml component.  (It is compiled on old Snow Leopard, and expected to work on Lion and Mountain Lion, but that is just an empiric guess.)
> 
> 
> 	Makarius
>