[isabelle-dev] performance problems

Makarius makarius at sketis.net
Fri Sep 7 20:18:37 CEST 2018


On 07/09/18 17:39, Lawrence Paulson wrote:
> What do you suggest for these on a 16 GB machine? I attach my file.
> Larry
> 
>> On 7 Sep 2018, at 15:01, Makarius <makarius at sketis.net
>> <mailto:makarius at sketis.net>> wrote:
>>
>> If you are using the 64-bit version of Poly/ML, you should give both
>> --minheap and --maxheap, otherwise it tends to overcommit a lot of memory.

I can't try it out, since theory "Explorer" is missing.

For 16 GB, I usually run Poly/ML in 32-bit mode, with --minheap 1500.


	Makarius



More information about the isabelle-dev mailing list