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

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

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:


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