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



Am 20.07.2014 um 19:12 schrieb Makarius <makarius at sketis.net>:

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

I don't think there's an easy way. This code has to be as fast as possible. It currently runs in about 300 ms on my machine, which is good, but I can imagine that this number looks more like 3 s or worse for the L4.verified guys (due to inherent quadratic components). Sticking to pure functional data structure would add a logarithmic component and a whole lot of memory allocations in a tight loop. If the opposite of "archaic" means "slow", I'm siding with "archaic".

The only realistic alternative I see is to use an external C or C++ program and providing it as a component. I would rather avoid this.

> Independently of that, it would be nice if the reason of the crash could be isolated and sent to David Matthews.

Yes, I'll look into this once the Vienna Summer of Logic is definitely over.

It would be nice to be able to fix this before the Isabelle2014 release, but I'm currently working from the hypothesis that we won't make it on time.

Jasmin





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