Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



On Tue, 22 Apr 2014, bnord wrote:


Am 22.04.14 14:28, schrieb Makarius:
 So far this does not disprove my reasing.
Wasn't meant to disprove anything.

 Just the standard game:

   * What is your hardware precisely?
Macbook Pro with 2.4GHz Core i5 (2 Cores with 4 Threads) and 8GB of Ram
   * What is your operating system?
OS X 10.9.2
   * What is your Isabelle version?
2013_2
   * What are your Isabelle options for "threads" and "parallel_proofs"?
0 and 2

That is a relatively weak CPU, but Intel makes it appear stronger via hyperthreading, thus it gets somewhat overloaded and burns a lot of CPU cycles (literally, by turning them into heat).

So lets try the following parameters:

  threads = 2

and in $ISABELLE_HOME_USER/etc/settings:

  ML_OPTIONS="-H 500 --gcthreads 2"

This requires a "reboot" of Isabelle.

The above will be morally the default in the next Isabelle release, because David Matthews now uses explicit information about virtual CPU cores.

For mobile systems it could also make sense to use only half of the number of real CPU cores, although for 2 cores that gives an unexciting 1 with
quite different interactive behaviour in sequential mode.


	Makarius




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