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

On Tue, 15 Jul 2014, Jasmin Christian Blanchette wrote:

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.

A segfault is ultimately a problem in the ML runtime system, but if there is a clearly defined ML component that triggers the problem, David Matthews can probably make educated guesses what is wrong.

We have had spurious crashes of this kind since last winter, but they were so rare that it was hard to guess anything. The problem (if it is the same) seems to be specific to parallel Intel hardware, but not AMD.

If anybody observes any such segfaults on AMD, please report this.

Another possibility for further testing is to downgrade to an older Poly/ML version from e.g. by claiming it in $ISABELLE_HOME_USER/etc/settings like this:

  init_component "$HOME/.isabelle/contrib/polyml-5.5.1-1"

Then use "isabelle components -a" on the command-line to resolve missing components, and restart the Isabelle application.


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