Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and