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 .
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
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 http://isabelle.in.tum.de/components e.g. by claiming
it in $ISABELLE_HOME_USER/etc/settings like this:
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