[isabelle-dev] logging and debugging output

[Makarius]

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.


 	Makarius