On Tue, 18 Oct 2011, Thomas Sewell wrote:
My email about PolyML and memory usage has generated some discussion,
perhaps I should give some more context.
The continuing improvements of Poly/ML statistics add important new
aspects to the overall performance monitoring of Isabelle performance,
On Tue, 18 Oct 2011, Thomas Sewell wrote:
We've been running PolyML in 32 bit mode on most of our machines. As
images grow beyond 4GB, we must switch to 64 bit mode, which roughly
doubles memory use to 8GB, which means replacing most of our laptops.
The jump from 32bit to 64bit has to be
My email about PolyML and memory usage has generated some discussion,
perhaps I
should give some more context.
The L4.verified project has been stuck at Isabelle-2009-2 for years. Our
proofs
seem to be compatible with newer Isabelle versions, but we're running out of
(virtual) memory. We've
