Hi Cezary, Thanks for reporting that and producing a small example. It's always much easier to work with something like that. I've had a look at it and I think there are actually several different bugs that are showing up but it all seems to revolve around the very large array. The intention is that the heap should grow and indeed it does with other examples. I'll need to look into this in more detail and try and fix the bugs. In the meantime you may be able to work around the problems by using a different structure instead of the single array.
Regards, David
On 20/03/2013 05:40, Cezary Kaliszyk wrote:
Dear all,
I have a PolyML program (below), for which maxheap is ignored: The heap is kept at the minheap size and does not grow automatically.
For the three runs below the maxheap is set to the same amount (4GB):
If I run: polyml --maxheap 4G --gcthreads 1 --minheap 4G < polybug.ml Terminates in less than 1 sec.
If I run: polyml --maxheap 4G --gcthreads 1 --minheap 500M < polybug.ml It does not terminate (at least not in 15 minutes)
If I run: polyml --maxheap 4G --gcthreads 1 --minheap 50M < polybug.ml I get 'Run out of store' exception.
Does the heap not grow automatically up to maxheap? Is there a way to make PolyML automatically adjust the heap size?
Tested both with 64bit polyml-5.5.0 (from Isabelle2013). And with current repository version (r1702).
Regards,
Cezary