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

On 16.07.2014 09:31, Lars Noschinski wrote:
> 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

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.

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