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 made at some point, and it will
cost a bit of memory, but not runtime. 64bit is already faster for usual
practical situations, I always use it by default for 1 year or so.
Another aspect is the ongoing replacement of TTY / Proof General
interaction with the new Prover IDE. This will cost further resources,
and it is unlikely that the result of two big processes (ML and JVM) can
support a big application on a small 4 GB laptop. (For me the bottom line
for small/medium Isabelle/PIDE applications is 2 cores, 4 GB, i.e. typical
Mac Book Pro from 2 years ago.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
