[isabelle-dev] Cannot execute Poly/ML in 32bit mode

[Makarius]

On Thu, 28 May 2015, Peter Lammich wrote:

> When I start Isabelle, I get the following warning message on the
> console:
>
> ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)
> ### Using bulky 64bit version of Poly/ML instead
>
> Is it a problem to use the bulky 64bit version?

Usually none, apart from wasting about a factor 2 of ML heap space.
On http://isabelle.in.tum.de/installation.html there is snippet of 
explanation:

   32-bit C/C++ standard libraries on 64-bit Linux (optional, for improved
   performance of Poly/ML)

It depends on the Linux distribution which packages provide the 32-bit 
C/C++ standard libraries mentioned above.


 	Makarius