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.

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" http://lists.inf.ed.ac.uk/pipermail/polyml/2013-March/001181.html

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.


	Makarius




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