[isabelle-dev] Cannot execute Poly/ML in 32bit mode
Hi list, 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? -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode
I think the main (and only) problem is that it uses significantly more memory. On 28/05/15 11:21, Peter Lammich wrote: Hi list, 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? -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
