inconsistent lsp diagnostic locations

[ciaran-matthew-dunne]

I am confused about the locations of diagnostics reported by the LSP.

Consider the yellow underlines the image below.

In the symbol declarations, the name of the symbol and semicolon are annotated, with an 'OK' message on hover.

For rule, compute, type commands, etc., the entire line is annotated.

Is there any reason for this? Is it a bug?

[fblanqui]

Hi Ciaran. Which editor do you use?

[ciaran-matthew-dunne]

Sorry, I should have stated that I'm using Zed as my editor with the Lambdapi extension I'm working on.

After trying, I can see that the issue doesn't effect VS Code:

However, this is still a compatibility issue for those using the LSP with other editors that render diagnostics differently.

The 'over-reporting' can be seen from the RPC messages sent by the LSP:

// Receive:
{
  "jsonrpc": "2.0",
  "method": "textDocument/publishDiagnostics",
  "params": {
    "uri": "file:///home/ciaran/prog/pp2lp/lp/Rules.lp",
    "diagnostics": [
      {
        "range": {
          "start": { "line": 0, "character": 0 },
          "end": { "line": 0, "character": 64 }
        },
        "severity": 4,
        "message": "OK"
      },
      {
        "range": {
          "start": { "line": 1, "character": 0 },
          "end": { "line": 1, "character": 40 }
        },
        "severity": 4,
        "message": "OK"
      },
      {
        "range": {
          "start": { "line": 6, "character": 18 },
          "end": { "line": 6, "character": 25 }
        },
        "severity": 4,
        "message": "OK"
      },
      {
        "range": {
          "start": { "line": 6, "character": 48 },
          "end": { "line": 6, "character": 48 }
        },
        "severity": 4,
        "message": "OK"
      },
      {
        "range": {
          "start": { "line": 7, "character": 0 },
          "end": { "line": 8, "character": 32 }
        },
        "severity": 4,
        "message": "OK"
      },
....

Consider the two diangostics with ranges 6:18-6:25 and 6:48-6:48 respectively. They correspond to the underlining of to_list and ; in my editor (line indexing starts at 0 in the LSP, and 1 in my editor).

The next diagnostic below has a range from 7:0 to 8:32. This corresponds to the underlining of rule to_list ... in my editor.

So this issue is now reduced to:

1. Why does the LSP report two diagnostics for symbol declarations? (one for the name, one for the semicolon). Are there any cases in which these two diagnostics actually differ?

2. Why does the range of LSP diagnostic reports for rule, compute, etc., span the entire length of the command?

Thanks!

[ciaran-matthew-dunne]

btw, I am more than happy to investigate this issue myself and propose a PR. I just wanted to make sure there isn't a special reason things are like this, and that somebody isn't already working on it!

[NotBad4U]

It is a known issue, and it also affects VSCode, but in a less critical way than Emacs or Zed. If you look at your second screenshot, you can notice that there are a few grey dots below symbol names and semicolons. When the mouse is over the symbol, a pop-up window will display the message OK. I remember that @nicomarg has a fix for Emacs that he showed me at the last EuroproofNet.

[ciaran-matthew-dunne]

It is a known issue, and it also affects VSCode, but in a less critical way than Emacs or Zed. If you look at your second screenshot, you can notice that there are a few grey dots below symbol names and semicolons. When the mouse is over the symbol, a pop-up window will display the message OK. I remember that @nicomarg has a fix for Emacs that he showed me at the last EuroproofNet.

I believe that this is the intended behavior. If I understand correctly, the issue you are referring to is that the LSP is publishing diagnostics that only say 'OK', when you would rather to only have diagnostics in the case of warning/failure. But this is fine because the severity of the 'OK' diagnostics is 4, which according to the LSP specification is intended for 'hints'. If a user wants to hide these (seemingly redundant) diagnostics, their editor likely has an option to change the 'max diagnostic severity'. Though perhaps there is a performance-based argument for removing them altogether.

My issue here is with range field of the published diagnostics. This isn't so obvious in VSCode due to the fact VSCode only renders 'three little dots' at the location indicated by the start portion of the range field.

[ejgallego]

This was a design choice back in the day intended more to debug than to keep it stable.

In the evolved LSP implementation that we hope to use soon, feedback about this is handled differently, and more in the spirit of the LSP spec:

• for file progress, we follow's Lean's fileProgress notification
• messages are not translated to diagnostics, but returned with goals, see https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md#goal-display

[Alidra]

What if we remove all the OK diagnostics?

[ciaran-matthew-dunne]

What if we remove all the OK diagnostics?

Interactive use of LambdaPi within a code editor can be fairly unstable, so it is sometimes nice to have these OK diagnostics as a signal that everything is functioning correctly.

The LSP spec defines 4 levels of severity for diagnostics. Level 1 is for errors, 2 for warnings, 3 for information, and 4 for hints.

OK messages published by lambdapi lsp should continue to have severity level 4, but diagnostics sent in response to queries (i.e., assert, assertnot, type, compute, flag, print, search, proofterm) should be promoted to have severity 3.

This way, the client can make a more informed choice when deciding how/where to display diagnostics sent by the server.

[Alidra]

but diagnostics sent in response to queries (i.e., assert, assertnot, type, compute, flag, print, search, proofterm) should be promoted to have severity 3

Thx @ciaran-matthew-dunne . I am probably missing something but I am not sure to understand the benefit of diagnostics with "OK" message.

LP sends an error message when queries fail. This means that everything is OK if no error message.

Do you think it can be useful to have explicit messages saying that the query succeeded? In this case, maybe use a more informative message like the result of the query. But maybe this is "too much" of information for a diagnostic message ?

[ciaran-matthew-dunne]

LP sends an error message when queries fail. This means that everything is OK if no error message.

Unfortunately this is not the case. There are cases in which the instance of lambdapi lsp run by VScode (and other editors) can silently crash, and the editor will still display diagnostics (but they will be reported in the wrong locations, etc). The user can easily restart the LSP from within their editor, but it may take a while for the user to notice that something is wrong.

Do you think it can be useful to have explicit messages saying that the query succeeded? In this case, maybe use a more informative message like the result of the query. But maybe this is "too much" of information for a diagnostic message ?

As mentioned above, I propose that diagnostics published in response to queries should have severity 3. With the exception of assert and assertnot, all queries return some 'result'. The result should be the message carried by the severity-level-3 diagnostic. Because assert and assertnot do not return any result, the LSP should only publish severity-level-4 diagnostics with the message "OK".

If the user does not want any OK messages whatsoever, then they can set their "severity threshold" at 3 and never see them.

[Alidra]

Thanks Ciaran,

Could you have a look at PR https://github.com/Deducteam/lambdapi/pull/1317 ?