Re: [isabelle] Questions about speed and CPU usage



On Wed, 21 Jul 2010, Peter Lammich wrote:

I have a related Problem with the new 2009-2 release. While 1GiB of RAM have always been enough for the 2009-1 release, the new version very quickly allocates more than 1GiB, and starts thrashing. Switching of "parallel proofs" makes things a bit better, but still my computer is nearly unusable during running larger proofs.

Have you changed any memory-related configurations in the new release, and is it possible to set them back again?

Initial heap size of Poly/ML is configured by ML_OPTIONS="-H 200", which is the same default as for Isabelle2009-2. The options for parallel checking are also the same.

What did change in Isabelle2009-2 is the overall bloat factor of main Isabelle/HOL. With as little as 1 GB it is unlikely that you will be able to process big sessions.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.