Re: [isabelle-dev] segmentation faults

2015-01-17 Thread Makarius
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-po

[isabelle-dev] segmentation faults

2015-01-16 Thread Tobias Nipkow
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 fau

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread David Matthews
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

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread Lawrence Paulson
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$UNIX

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread Makarius
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 fin

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread Lawrence Paulson
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

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread 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

Re: [isabelle-dev] Segmentation faults

2013-05-29 Thread Makarius
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 P

Re: [isabelle-dev] Segmentation faults

2013-05-28 Thread 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 wor

Re: [isabelle-dev] Segmentation faults

2013-05-27 Thread Makarius
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? Th

Re: [isabelle-dev] Segmentation faults

2013-05-12 Thread Lawrence Paulson
Just had a crash on my (Mac) laptop too. Larry On 12 May 2013, at 12:24, David Matthews 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

Re: [isabelle-dev] Segmentation faults

2013-05-12 Thread David Matthews
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'

Re: [isabelle-dev] Segmentation faults

2013-05-11 Thread Tjark Weber
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. >

[isabelle-dev] Segmentation faults

2013-05-02 Thread Lawrence Paulson
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: