On 01/03/2017 13:31, Makarius wrote:
On 01/03/17 13:55, David Matthews wrote:
On 24/02/17 13:26, Makarius wrote: My current guess is that it is a problem of compiled ML code that is no longer garbage-collected.
The current version does garbage collect code; it's just that it only happens at a major GC. Previously when code was part of the general heap a short-lived code cell would be garbage-collected by a minor GC. It could be that this is problem or it could be that there is a bug which is resulting in code not being properly collected.
I'm inclined to release the current version of git master as 5.7 and then look into this and other issues.
OK, it merely means that we need to skip this version for official Isabelle use. I will continue testing Poly/ML repository versions privately.
That's understandable. Adding support for interpretation is going to be a bit of work and until it's done and tested there's no way of being sure it will solve this problem. I'd prefer not to delay the release.
David