[isabelle-dev] Segmentation faults

Lawrence Paulson lp15 at cam.ac.uk
Wed May 29 15:03:10 CEST 2013


Following Dave Matthew's instructions, I downloaded a fresh copy of the sources and executed the following commands. Except the first one failed, presumably because I had a fresh copy.

make distclean
./configure --disable-shared
make
make install

I have just taken a look at the crash logs, and it's clear that some dynamic libraries from a previous installation had got loaded along with the latest ones. Maybe that was the problem. I wonder how they got loaded in the first place? I have just deleted them and I hope it will work now.

Larry
-------------- next part --------------
A non-text attachment was scrubbed...
Name: poly_2013-05-28-145613_epicure.crash
Type: application/octet-stream
Size: 24732 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130529/f66deeb6/attachment-0002.obj>
-------------- next part --------------


On 29 May 2013, at 10:25, Makarius <makarius at sketis.net> wrote:

> 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