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