[isabelle-dev] HOL-Proofs

[Makarius]

On Wed, 14 May 2014, David Matthews wrote:

> I don't know why it should be different when you run it interactively.

That is just because an interactive PIDE session is quite different from a 
batch build session it what it does.  I've tries for years to unify that 
further, but we are actually moving away from it.

Normally PIDE interaction requires more resources than batch build.  For 
HOL-Proofs I suspect that Tobias did not have the proofs enabled, because 
that requires some special tricks in its bootstrap.  In contrast, using 
isabelle jedit -l HOL-Proofs or equivalent should to the right thing, and 
enable the proof terms, but the critical phase is already over at that 
point.


> I would assume that you are running in 32-bit mode.  Have you tried in 
> 64-bit mode with a larger heap?

Our usual defaults are for 32-bit mode, which normally works thanks to the 
online heap sharing.

The move to 64-bit will be inevitable at some point, especially for bigger 
applications that live on the edge of what is possible -- although main 
HOL itself is already close to that. 64-bit means that people cannot use 
small mobile devives anymore, with only 4-8 GB, but require a real machine 
with 16 GB or more.

See also this related thread 
http://www.mail-archive.com/isabelle-dev%40mailbroy.informatik.tu-muenchen.de/msg04536.html

In fact, polyml-5.5.2 from Isabelle/e7bf30290627 might already circumvent 
that particular problem from last September, although but I have seen 
other situations of hitting the wall for AFP/Collections and related 
sessions with 5.5.2 as approximated from the SVN version in the past few 
months.


 	Makarius