Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory

On 04/02/16 07:40, Makarius wrote:
On Wed, 3 Feb 2016, Matthew Fernandez wrote:

Maybe I'm missing some context for this statement, but why is using 64-bit Poly/ML a mistake? This is what I use and,
as far as I'm aware, is the default configuration in the l4.verified proofs setup [0]. I don't have a deep knowledge
of the Poly/ML implementation but my understanding is that, while the 64-bit version uses more memory to accomplish
the same thing, you *must* use it if you want to use more than N bytes of RAM (for some N; 4GB?).

For more than 3 years big Isabelle applications are usually run in constant space of approx. 3.5 GB, i.e. the maximum on
32bit.  This applies to all of Isabelle + AFP, and is usually the most efficient way on small and big machines.

Applications that really need more GBs -- presumably l4.verified is the only one on the planet -- there is no other way
than to move on to bigger machines and the 64bit model.

What kind of hardware do l4.verified people use for that?

Raf Kolanski can probably provide details about our server, but for my own desktop machine I have an Intel i7 with 32GB
RAM. On my current proofs I regularly exceed 20GB.


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.