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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
