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



Hello all,

I have seen the same behaviour.

Step to reproduce:

(0. open isabelle/jEdit with two buffers.)

1. open List.thy
	 isabelle jedit -l Pure List.thy

2. in the second buffer switch to Ring.thy.

3. once Ring.thy is processed, add a line break. Look at the Theories panel 
how long it takes to restart the processing.

After bisecting, the first commit with this issue is: 
  http://isabelle.in.tum.de/reports/Isabelle/rev/9d2fae6b31cc

I have not investigated further.


Cheers,

Mathias


On mardi 22 novembre 2016 18:22:52 CET Bertram Felgenhauer via Cl-isabelle-
users wrote:
> 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


-- 
--
Mathias Fleury
ENS Rennes MIT3




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