[isabelle-dev] HOL-Proofs

[Tobias Nipkow]

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?

Tobias

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