Pull diagonostics

[Alizter]

Diagnostics should be pulled on demand rather than all given at once.

Unlikely to solve general performance issues around them however.

Problems with current setup:

• VsCode limits to around 1000 diagnostics
• Our algorithm can become cuadratic if we enable the ok_diagnostics
• Diagnostics are not a good way to convey checking progress

[ejgallego]

What are the general performance issues?

[Alizter]

Having lots of diagnostics around is generally quite slow for vscode. You are the original author of the performance issues comment however here. :-)

[ejgallego]

I was asking because there are a few different concerns w.r.t. performance.

Pull diagnostics solve quite a few other general performance issues related to diagnostics, and I think indeed it does help vscode too.

@corwin-of-amber , @Alizter , actually it is a pity that https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_diagnostic doesn't include a document point in the request, that would actually be almost enough as to have an idea of what the viewport is, and only check that part of the document.

Maybe we should open an issue upstream?

I've commented on microsoft/language-server-protocol#737

[ejgallego]

To give an idea of what eager_diagnostics=true is costing us, even after #104 here are timing for Pff with and without:

[end check]: document fully checked File "file:///home/egallego/research/coq-lsp/examples/Pff.v", line 27790, characters 0-1
[cache]: hashing: 0.369962 | parsing: 2.169005 | exec: 74.997016
[cache]: cache hit rate: 0.00

[end check]: document fully checked File "file:///home/egallego/research/coq-lsp/examples/Pff.v", line 27790, characters 0-1
[cache]: hashing: 0.243913 | parsing: 1.468305 | exec: 64.425011
[cache]: cache hit rate: 0.00

take them with a grain of salt, as all informal timings, but that seems significative.

[ejgallego]

I was trying to understand how partial Pull Diagnostics work, but I couldn't really figure out from the spec :/