Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
On 16.07.2014 23:47, Lars Noschinski wrote:
> 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 .
>>> 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.
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.
Welcome to Isabelle/HOL (Isabelle2014-RC0: July 2014)
84: 27780 Segmentation fault "$POLY" -q -i $ML_OPTIONS --eval
"$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit
This archive was generated by a fusion of
Pipermail (Mailman edition) and