Steven Obua wrote:
I am using poly ml 5 together with Isabelle. When I start poly with the "-H 500" option, my process will terminate with a "run out of store" message after these 500MB have been used up (I used "top" to monitor the heap usage). If I give "-H 8000", it will succeed. Is this behaviour to be expected?
Steven, No, that's not what I would expect. What should happen is that the -H option is used to compute the initial heap size. If that is exhausted additional segments of the same size as this are allocated until the allocations fail. That is usually because either there is no more swap space or because some other limit has been reached.
I don't understand why this isn't working for you. What sort of machine are you running this on? How much memory and swap space are available? Is this a shared machine? Regards, David.