[isabelle-dev] Segmentation faults

[Makarius]

On Wed, 29 May 2013, Makarius wrote:

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

Here is another approach to get this information: 
DYLD_PRINT_LIBRARIES=true before the executable is run.

See the included ch-test to change lib/scripts/run-polyml accordingly. The 
result looks like this on my Mountain Lion:

   $ isabelle tty
   dyld: loaded: /Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin/poly
   dyld: loaded: /Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin/libpolyml.4.dylib
   dyld: loaded: /usr/lib/libSystem.B.dylib
   dyld: loaded: /usr/lib/libstdc++.6.dylib
   dyld: loaded: /usr/lib/system/libcache.dylib
   dyld: loaded: /usr/lib/system/libcommonCrypto.dylib
   dyld: loaded: /usr/lib/system/libcompiler_rt.dylib
   ...


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1369820188 -7200
# Node ID 6c3763f05f59feecc81f31f4818abdbbe9468cd9
# Parent  c8ee9c0a3a648eee62f7f25b541a8cdf38cd1c96
test;

diff -r c8ee9c0a3a64 -r 6c3763f05f59 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed May 29 11:06:38 2013 +0200
+++ b/lib/scripts/run-polyml	Wed May 29 11:36:28 2013 +0200
@@ -41,7 +41,6 @@
 
 librarypath "$POLYLIB"
 
-
 ## prepare databases
 
 if [ -z "$INFILE" ]; then
@@ -74,7 +73,7 @@
 fi
 
 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+  { read FPID; env DYLD_PRINT_LIBRARIES=true "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
 RC="$?"
 
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"