[isabelle-dev] More context on Isabelle memory consumption

[Makarius]

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