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



2016-02-03 21:54 GMT+01:00 Makarius <makarius at sketis.net>:
> On Wed, 3 Feb 2016, C. Diekmann wrote:
>
>> I'm not getting the "bulky 64bit version" warning when i start jEdit or
>> build, so I guess that I'm using the 32bit library.
>
>
>> Is Isabelle2016 still issuing a warning on startup if the 64bit libraries
>> are used?
>
>
> Not any longer.  This warning usually showed up in unexpected situations,
> and did not show up when the standard Isabelle application wrapper was used.
>
> There were various changes in the auto-configuration of 32bit vs. 64bit
> platforms, both for the ML system and the JVM.  You now get this information
> in the title of the build dialog on the first startup, but it is possible to
> overlook it. (And sometimes people think that 64bit is always better than
> 32bit.)

Is there a way to check my setup after the first startup?

> I was thinking of an additional warning dialog for a situation where the
> option ML_system_64 is not set (i.e. the default of Isabelle), but the
> result forced to x86_64-linux due to lack of 32bit g++ libraries (i.e. the
> default of most Linux installations).  I did not do it, because it may cause
> puzzlement to new users or casual users, e.g. of introductory Isabelle
> tutorials.  The difference is only relevant to really big applications.
>
> Isabelle power users, especially on Linux, need to do some more fine-tuning
> to get various side-conditions right.  The details are listed here:
> http://isabelle.in.tum.de/website-Isabelle2016-RC3/installation.html

Where can I find the documentation how I can set the ML settings such
that I can build Collections again?

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

If the build of a session image fails with an out of memory error, is
it possible to do the build again with only one core/process to limit
the memory usage to 3.5GB?

Cheers,
  Cornelius




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