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 . 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