[isabelle] Isabelle2016-1-RC3: responsiveness of interrupting continuous checking



In Isabelle2016-1-RC3, the time span between unchecking "continuous
checking" and stopping the processing theories tends to be much longer
than in Isabelle2016; for the latter this typically happens within 1
or 2 seconds, while for the former I'm observing times upwards of 5
seconds, up to perhaps 10 seconds. (There also seems to be a tendency
to finish theories whose processing has been started.)

I'm observing this with IsaFoR, but I expect that any proof development
of nontrivial size suffers from this phenomenon.

The increased delay is quite annoying, especially now that we're
updating theories to the RC. A typical workflow is to load a leaf
theory, watch the theory panel for errors, and then jump to the first
error that appears; this jump has a similar effect to disabling
"continuous checking", because everything up to the error point has
already been processed. But one cannot interact effectively with the
theorem prover before the continuous checking ceases completely, so the
increased waiting time matters.

As far as I can see, this is not a matter of the number of cores; I've
encountered the same behaviour with 6 threads and with just 2.

Cheers,

Bertram





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