Re: [isabelle] jEdit - slowdown on split-view of same buffer

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.


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