Re: [isabelle] Isabelle2021-1-RC3: excessive Poly/ML heap requirements




I haven't had a chance yet but it turns out that setting --max-heap to 4G allows me to work without interruption. I will try other Poly/ML next.

I have tried to build HOL-Analysis on a 4GB Mac and it completely failed (i.e., did not finish within a day or two, probably stuck due to constant swapping). Setting --max-heap to 2G made it work in a few hours (it was an old system). So it seems that the polyml defaults do not necessarily use the machine optimally. Maybe you had a similar situation, just scaled up by a factor of two.

Best wishes,
Dominique.






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