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

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?


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