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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and