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 [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.

  -- Lars

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