Email Gateway (Aug 19 2022 at 11:41): Email Gateway (Aug 19 2022 at 11:41):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
Hi all,
With jEdit, I've been experiencing some weird, massive slowdowns
occasionally when I'm editing, and finally figured out why it happens. I
have a habit of sometimes viewing the same buffer in two split frames.
If I edit in the frame viewing a later part of the buffer, all is well.
But if I start editing in the frame viewing an earlier part of the
buffer than the other frame, it seems that every time I change something
in that frame, the parser will immediately try to re-process the file up
to the frame with the latest view of the buffer, causing a massive
slow-down.
Naturally, the larger the space between the two viewing frames, the
worse it gets.
Knowing this, it's pretty easy to work around, but it would be nice not
to have to worry about it. Maybe it's just a question of having it
process only up to the frame that has focus, instead of the
latest-viewing frame?
Regards,
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
On Fri, 23 Aug 2013, Palle Raabjerg wrote:
With jEdit, I've been experiencing some weird, massive slowdowns
occasionally when I'm editing, and finally figured out why it happens. I
have a habit of sometimes viewing the same buffer in two split frames.
If I edit in the frame viewing a later part of the buffer, all is well.
But if I start editing in the frame viewing an earlier part of the
buffer than the other frame, it seems that every time I change something
in that frame, the parser will immediately try to re-process the file up
to the frame with the latest view of the buffer, causing a massive
slow-down. Naturally, the larger the space between the two viewing
frames, the worse it gets.
Note that is not "the parser", but the actual prover doing work in the
background. It does many things apart from parsing, and it is surprising
to see how well that mode of "continous proof checking" already works in
Isabelle2013 with and most applications that I have seen. Sometimes there
are very "slow" theories that spoil the game, though.
Generally, the system tries to process the visible parts of the overall
collection of theories, and what is required as imports for that. There
are also some implicit policies about printing results depending on
visibility -- often printing takes more time than proving.
Knowing this, it's pretty easy to work around, but it would be nice not
to have to worry about it. Maybe it's just a question of having it
process only up to the frame that has focus, instead of the
latest-viewing frame?
The idea is indeed that the system takes care of the scheduling such that
the user has as little to worry. This will be again refined in the next
release (coming within the next few months, before the winter). There
will be also a few flags to switch off parts of the checking
declaratively, but it needs further experimentation how many "controls"
the user can manage. The system is no longer driven like a handcart as in
the TTY / Proof General ago, but runs on its own at very high speed.
I would rather not include window focus in any of the implicit policies,
since this is not well-defined in the Java/Swing GUI framework. Maybe
Sun/Oracle had something specified in mind, but empirically focus is very
unreliable, sometimes lack of focus even locks-up the application.
Makarius
Last updated: May 18 2024 at 20:16 UTC