Search command that shows many results is extremely slow

[RalfJung]

For teaching Coq, it is quite useful to first introduce commands like Search as things you type into the buffer, so that there's not yet another element of the UI that needs to be introduced -- and so that recommended commands can be included directly in the proof script, which is much easier than telling students "now press these shortcuts and enter this thing to run a search query".

However, when a Search command produces hundreds of results, it can take 10s and more until there is any feedback in the UI. That's extremely confusing, and it is hard to even tell that something is processing in the background. It's also a lot slower than CoqIDE or ProofGeneral. I don't know why it is so slow; I think what happens is that every single search result is added as an "information" annotation (not sure what vscode calls them -- the things that cause blue underlines, as opposed to red for "error" and orange for "warning") to the current line and creating 1000 or so of these annotations takes a while -- and nothing at all is shown in the UI until they are all added.

So maybe it'd be better to make this all just one single annotation instead of one per result -- or would that just explode vscode in other ways since the text associated with the annotation becomes too big? Or maybe it should just stop after 100 results or so and discard the rest (and indicate that things were discarded), since such a long list is rarely useful? But sometimes it's probably nice to get the entire list and Ctrl-F in it, I've definitely done that in ProofGeneral.

[SkySkimmer]

Search sorts the results (search.ml prioritize_search) so it can't output anything until it has seen the full result list

[RalfJung]

I think Coq produces the results fast enough, it's getting them to VsCoq and the UI which slows things down. So Coq can keep sending the entire thing as one answer, it's just about how the IDE processes that answer.

[rtetley]

I think you are probably right and this could be fixed by something that @Durbatuluk1701 suggested here

[RalfJung]

Oh yeah if this also affects Set Typeclasses Debug, where I sometimes wade through traces of many 10k lines, then finding some solution that doesn't take a long time to display the trace is quite crucial.

[rtetley]

The question I am asking myself is should this be a diagnostic ? (What you refer to as a information annotation). We could make so that it isn't ?

[rtetley]

However I assume the line that you just executed if you are in manual mode should be blue until it is fully processed ?

[RalfJung]

The question I am asking myself is should this be a diagnostic ? (What you refer to as a information annotation). We could make so that it isn't ?

Absolutely. I only expected it to be shown in the proof view. I just observed that it is a diagnostic currently and that's likely part of the problem.

[RalfJung]

However I assume the line that you just executed if you are in manual mode should be blue until it is fully processed ?

No. It turns green pretty much immediately (after maybe 0.1s), and then it takes a few seconds until the results are shown.

If it stayed blue until the proof view is updated, that would help to make this behavior less confusing.

[rtetley]

However I assume the line that you just executed if you are in manual mode should be blue until it is fully processed ?

No. It turns green immediately, and then it takes a few seconds until the results are shown.

If it stayed blue until the proof view is updated, that would help to make this behavior less confusing.

I guess that makes since. From the server point of view the command has been executed. It is sending through all the results that takes time. I suppose we should remove it from diagnostics. It would be nice to have some other user feedback on this. @gares WDYT ?

[Durbatuluk1701]

Should maybe it be the case that the highlight event is sent last? Might help with #859 as well

I do not first look for Search results in the diagnostic annotation, but one workflow I have done (quite infrequently) is:

Search X.
other_stuff.|
utilize_result_from_search.

And look back at the search results with a hover, otherwise they disappear from the messages section of the goal panel when you have interpreted up to other_stuff.. I would personally be willing to trade this for speed though.

[RalfJung]

And look back at the search results with a hover

Ah, that's neat that this works! The other editors I used can't do this.

Arguably this feature is also provided by the dedicated search panel, where results stick around even as you move on in the proof. Maybe there should be an easy way to turn a manually entered Search query. into a result shown in the panel?