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

Makarius makarius at sketis.net
Thu May 28 13:54:27 CEST 2015

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 

   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.


More information about the isabelle-dev mailing list