nipkow at in.tum.de
Wed May 14 16:09:39 CEST 2014
On 14/05/2014 16:06, Makarius wrote:
> 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.
This is what I did interactively: starting from Pure I loaded Proofs.thy first
and then Main.thy. Maybe this did not really switch proof terms on?
>> 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
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev