Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP



On 17.07.2014 00:00, Lars Noschinski wrote:
> On 16.07.2014 23:47, Lars Noschinski wrote:
>> On 16.07.2014 09:31, Lars Noschinski wrote:
>> d
>>> On 15.07.2014 23:47, Jasmin Christian Blanchette wrote:
>>>> Hi Fabian, Christian,
>>>>
>>>>> I noticed two problems, it could be that they are related but i don't know. Note that (especially the first one) might be related to the ML process crashing in thread [1].
>>>> Thanks for your reports. I will look more closely into them in the coming days. I actually ran into the second issue last Friday when demoing Sledgehammer to Daniel Matichuk but could not reproduce it afterward. I also experience the first issue once in a while, sometimes with Sledgehammer, sometimes without; it seems to be related to multithreading.
>>>>
>>>> I will disable MaSh for now -- it is the likely source of both problems, and I would rather play safe with the coming release. It's a pity, since the tool really does help Sledgehammer, but I don't want to see reports like this one about Isabelle2014 final if it can be avoided.
>>> Yesterday, PolyML crashed two times for me (once with a segfault, once
>>> with an illegal instruction). This happened, when I replaced a "by
>>> (metis ...)" by an "apply (metis ...)". The "by (metis ...)" was of
>>> course just inserted by sledgehammer, so this might have been an
>>> instance of the same problem.
>> Another segfault, this time triggered directly while using sledgehammer.
>>
>> ----
>> $ cat ~/.isabelle/Isabelle2014-RC0/etc/settings
>> ML_OPTIONS="-H 1000 --gcthreads 1"
>> JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss4m -Dactors.corePoolSize=4
>> -Dactors.enableForkJoin=false"
>>
>> init_component "$HOME/P/afp"
>> ----
>>
>> Following Makarius' suggestion, I'm leaving MaSh enabled for now, but
>> switch to poly 5.5.1-1 and will report on further possible crashes.
> Crashed again; even at the same position in the theory (with poly
> 5.5.1-1). I'll try tomorrow whether this can be reproduced reliably.
Since it is already tomorrow: I started the minimization process and
polyml indeed crashed reliably at the same place, again and again. Then
it suddenly stopped, and I haven't been able to reproduce it again (even
when going back to the original theory).

But I stumbled upon some interesting behaviour: Apparently, in this
proof, sledgehammer tries to use a theorem whose proof (in another
theory) failed. So, in the sledgehammer window, I don't see the output
of sledgehammer, but rather the error message belonging to the failed
"by" of said theorem.

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.