Re: [isabelle-dev] segmentation faults
On Fri, 16 Jan 2015, Tobias Nipkow wrote: The AFP test has been failing for random entries with segmentation fault over the last few days. Now the same thing is happening when I test HOL locally on my Mac. My latest test run yielded Running HOL-IMPP ... /Users/nipkow/isabelle/lib/scripts/run-polyml-5.5.2: line 82: 473 Segmentation fault: 11 $POLY -q -i $ML_OPTIONS --eval $(perl $ISABELLE_HOME/lib/scripts/recode.pl $MLTEXT) --error-exit /dev/null HOL-IMPP FAILED I have seen such core dumps only very sporadically so far. If there is a known configuration where it happens reliably, it would help to figure out the reasons. Where is the AFP test configuration formalized? Moreover, when I rerun the build I get Running HOL-IMPP ... Finished HOL-IMPP (0:00:06 elapsed time, 0:00:07 cpu time, factor 1.16) Given the short execution times: have those theories really been tested? Probably not. The log.gz files should contain some information what really happened -- it might actually provide further clues about the above crash. As a quick workaround it might also help to use ML_OPTIONS=-H 1500 or even ML_OPTIONS=-H 2000. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
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# 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-polymlWed May 29 11:06:38 2013 +0200
+++ b/lib/scripts/run-polymlWed 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
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 poly_2013-05-28-145613_epicure.crash Description: Binary data On 29 May 2013, at 10:25, Makarius makar...@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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
On Wed, 29 May 2013, Lawrence Paulson wrote: 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. Where did you see that in the log? There is the following near the end, but it looks fine so far: Binary Images: 0x1000 - 0x56aff7 +poly (???) 7513623B-C8EF-B2EE-7AB8-86D56D558A10 /Users/USER/*/poly 0x59b000 - 0x5fbfeb +libpolyml.4.dylib (5) 2E0AD632-82FD-C839-A4EF-7C7D917E4C07 /Users/USER/*/libpolyml.4.dylib 0x110 - 0x1102fff +libsha1.so (0) F18686EA-3708-0005-8488-0829107C5FFB /Users/USER/*/libsha1.so Maybe /Users/USER/* is just some anonymized version of the real locations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Here for example: Thread 0:: Dispatch queue: com.apple.main-thread 0 libsystem_kernel.dylib0x99c998e2 __psynch_cvwait + 10 1 libsystem_c.dylib 0x984db280 _pthread_cond_wait + 833 2 libsystem_c.dylib 0x985610e0 pthread_cond_timedwait$UNIX2003 + 70 3 libpolyml.4.dylib 0x005b37a1 PCondVar::WaitFor(PLock*, unsigned int) + 113 4 libpolyml.4.dylib 0x005c3614 Processes::BeginRootThread(PolyObject*) + 852 5 libpolyml.4.dylib 0x005b7e18 polymain + 2392 The dynamic libraries had an earlier creation date from the other poly/ML libraries. Larry On 29 May 2013, at 14:18, Makarius makar...@sketis.net wrote: On Wed, 29 May 2013, Lawrence Paulson wrote: 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. Where did you see that in the log? There is the following near the end, but it looks fine so far: Binary Images: 0x1000 - 0x56aff7 +poly (???) 7513623B-C8EF-B2EE-7AB8-86D56D558A10 /Users/USER/*/poly 0x59b000 - 0x5fbfeb +libpolyml.4.dylib (5) 2E0AD632-82FD-C839-A4EF-7C7D917E4C07 /Users/USER/*/libpolyml.4.dylib 0x110 - 0x1102fff +libsha1.so (0) F18686EA-3708-0005-8488-0829107C5FFB /Users/USER/*/libsha1.so Maybe /Users/USER/* is just some anonymized version of the real locations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
From that crash log it looks as though the crash happened in ML code rather than the run-time system itself. The source of the crash, though, could be a bug in the run-time system resulting in some addresses being mangled. It's difficult to say more without being able to reproduce it. David On 29/05/2013 14:03, Lawrence Paulson wrote: 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Just had a crash on my (Mac) laptop too. Larry On 12 May 2013, at 12:24, David Matthews d...@prolingua.co.uk wrote: 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Larry, 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. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Segmentation faults
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? ~/isabelle/Repos/src/HOL: hg id cdc05fc4cd0d tip My Isabelle components are up-to-date. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
