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.
While sitting together at the "Heuriger" on Friday, Cezary mentioned in
passing that the machine-learning stuff uses a lot of archaic array
programming. That might well be a reason for Poly/ML vomiting: it has
happened occasionally over the years, but arrays are extremely rare these
days. A more recent incident was reported by Cezary on the thread
"[polyml] Heap does not grow up to --maxheap"
Maybe there is an easy way to avoid mutable data structures, and get
things back into proper shape for the Isabelle2014 release.
Independently of that, it would be nice if the reason of the crash could
be isolated and sent to David Matthews.
This archive was generated by a fusion of
Pipermail (Mailman edition) and