[isabelle-dev] logging and debugging output
makarius at sketis.net
Fri Apr 11 12:51:33 CEST 2014
On Fri, 11 Apr 2014, stvienna wiener wrote:
> 2014-04-02 10:47 GMT+02:00 Makarius <makarius at sketis.net>:
>> On Wed, 2 Apr 2014, stvienna wiener wrote:
>> What is your OS and hardware platform (memory, number of cores)?
> I am running a 64-bit arch linux distribution, but without any 32-bit
> compatibility libraries.
Installing the 32-bit shared libraries for C/C++ usually helps a lot in
Poly/ML performance. It requires less memory and behaves better in
situations of non-termination of user tools.
It is one of the oddities of most Linux distributions that this is not
done by default, but it is in accordance to the general Linux attitudes of
not supporting genuine applications, i.e. things that are not installed as
part of the system itself. Thus "Linux on the desktop" somehow remains
unprofessional on purpose. I am myself a Linux user for a long time, and
I agree in this respect with Linus Torvalds himself.
64-bit is important for anything else around it, but Poly/ML works better
in 32-bit, ever since David Matthews made the wonderful online compaction
and sharing of immutable heap content.
More information about the isabelle-dev