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