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.

isabelle-dev mailing list

Reply via email to