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



On 03/02/16 09:35, Makarius wrote:
On Tue, 2 Feb 2016, Peter Lammich wrote:

Have you used 64bit poly? What happens on 32bit poly?

Using Poly/ML with x86_64 is actually a common mistake -- it is the default on most Linux installations, but the
Isabelle installation instructions say explicitly that 32bit libraries should be installed.

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?). If this is not the case, I
would love to be enlightened as to how to better configure my system.

  [0]: https://github.com/seL4/l4v/blob/master/misc/etc/settings#L19

We are back to the question how much documentation people want to use. Anybody with higher-than average requirements
should peek at advanced texts occasionally.


What also helps under tight ML heap conditions to is vary the ML_OPTIONS a bit, concerning the initial heap size.  This
changes the way how Poly/ML grows and shrinks the heap, and sometimes it makes a difference.


     Makarius



________________________________

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.