[isabelle-dev] Cannot execute Poly/ML in 32bit mode
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
> ### 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