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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
