[isabelle-dev] Remaining uses of Proof General?

[Thomas Sewell]

>
> Back to the actual technical questions.  What are the main performance 
> bottle-necks here? Printing of intermediate goal states?  Or applying 
> intermediate steps repeatedly?
>

I suspect that the problem is not that the printing or the intermediate 
calculations are taking too long. It's that printing the output the user 
wants to see is waiting on some other computation finishing, creating 
the sensation of lag.

Some evidence to back this up: I tried an adjustment a while ago in 
which I had the goal state print incrementally. Even if some of the 
subgoals took a while to print, you'd see the line with "goal (12 
subgoals)" immediately, and then the subgoals as they were formatted. 
The short summary is that this helped a little sometimes, but I often 
still saw an empty Output panel for seconds after moving the cursor to a 
line that the continuous checker had already processed.

I strongly suspect that the print request was waiting in a queue 
somewhere. The system would become responsive again once it finished 
doing something else. I don't think that this is to do with garbage 
collection or heap sharing - I don't recall a specific instance, but I'm 
sure I've seen this behaviour when there's been plenty of spare memory. 
Sometimes there would be purple lines in the buffer, suggesting that 
some of the worker threads were busy on other tasks, but not always.

On incremental printing: it's easy to implement by generalising a couple 
of the relevant Pretty operations to produce a Seq.seq internally rather 
than a list. It looked promising initially, but then became really 
annoying, because Isabelle/jEdit or PIDE resets the Output buffer each 
time it gets more to display. So if you scroll down to look for 
something, you get scrolled back up for each time a subgoal prints, 
which can give the sensation that the editor is fighting you. That's why 
I didn't make any effort to suggest it upstream.

I don't know if that helps. Perhaps if I run across a good demonstrative 
example I'll send it across.

Cheers,
     Thomas.