Email Gateway (Aug 22 2022 at 14:26): Email Gateway (Aug 22 2022 at 14:26):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:26):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello all,
I have seen the same behaviour.
Step to reproduce:
(0. open isabelle/jEdit with two buffers.)
open List.thy
isabelle jedit -l Pure List.thy
in the second buffer switch to Ring.thy.
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:
--
--
Mathias Fleury
ENS Rennes MIT3
Email Gateway (Aug 22 2022 at 14:26):From: Makarius <makarius@sketis.net>
Thanks for trimming it down and making the bisection.
9d2fae6b31cc changes the overall timing of editing/painting, which
apparently leads into situations where the main editor input queue is
overloaded with events and thus requires very long to fire eventually.
In
https://bitbucket.org/isabelle_project/isabelle-release/commits/1aef5a0e18d7
I have added a dalay_first element to improve this, but it also changes
the overall timing behaviour PIDE. So it is important to keep an eye on
this within the few remaining weeks before the final release.
Right now it is possible to continue testing with the above repository
version, or with http://isabelle.in.tum.de/devel when updated in approx. 8h.
Makarius
Email Gateway (Aug 22 2022 at 14:27):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Makarius wrote:
Thanks, that has improved the behavior a lot. The response time feels
very close to Isabelle-2016 with this change.
Cheers,
Bertram
Last updated: Nov 21 2024 at 12:39 UTC