[isabelle-dev] Segmentation faults

Makarius makarius at sketis.net
Wed May 29 11:25:05 CEST 2013


On Tue, 28 May 2013, Lawrence Paulson wrote:

> 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.

Cqn you explain how this separate Poly/ML is compiled, and where it is 
installed?


> He thought perhaps the libraries could be interfering.

The Mac OS X crash report should tell you about the shared libraries that 
were used in the failed process.

There is also "otool -L" to check that statically on the executable, but I 
am unsure if it is exactly that.  E.g. for polyml-5.5.0-3/x86-darwin/poly 
from our Isabelle component it always shows the location where the binary 
was compiled originally, regardless of DYLD_LIBRARY_PATH at run-time.


 	Makarius




More information about the isabelle-dev mailing list