addDeclarationRanges eval taking forever

Stream: lean4

[Aurélien Saue]

The final #eval in this snippet is being processed forever

import Lean
open Lean

def name : Name := `name


def drs : DeclarationRanges :=
  { range :=
      { pos := { line := 0, column := 0 },
        charUtf16 := 0,
        endPos := { line := 0, column := 0 },
        endCharUtf16 := 0 },
    selectionRange :=
      { pos := { line := 0, column := 0 },
        charUtf16 := 0,
        endPos := { line := 0, column := 0 },
        endCharUtf16 := 0}
  }


#eval (addDeclarationRanges name drs : MetaM Unit)

[Aurélien Saue]

Actually it does work when executing in command line but not in VSCode

[Gabriel Ebner]

I wonder if this is related to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/can't.20print.20unit/near/234134267

[Sebastian Ullrich]

In Emacs I just get an empty message as expected

[Gabriel Ebner]

This is interesting. Apparently the server returns empty messages:

  {
    "params": {
      "version": 1,
      "uri": "file:///home/gebner/lean4/foo.lean",
      "diagnostics": [
        {
          "source": "Lean 4 server",
          "severity": 3,
          "range": {
            "start": {
              "line": 2,
              "character": 0
            },
            "end": {
              "line": 2,
              "character": 5
            }
          },
          "message": "",
          "fullRange": {
            "start": {
              "line": 2,
              "character": 0
            },
            "end": {
              "line": 2,
              "character": 5
            }
          }
        }
      ]
    },
    "method": "textDocument/publishDiagnostics",
    "jsonrpc": "2.0"
  }

[Daniel Fabian]

I wonder if it's related to a similar issue I'm facing with side-effecting MetaM Unit stuff.

[Daniel Fabian]

I seem to also get infinite loops if I don't print something using trace[Meta.debug] and make a pure side-effect.

[Gabriel Ebner]

The vscode extension then throws an exception (and doesn't update the diagnostics):

Notification handler 'textDocument/publishDiagnostics' failed with message: message must be set

[Sebastian Ullrich]

I see @Gabriel Ebner fixed it on the extension side, but I suppose we could still suppress empty messages from the server?

[Gabriel Ebner]

I'm not sure what the right solution here is. Empty messages are not forbidden by the LSP protocol AFAICT.

[Sebastian Ullrich]

Yeah, I just wonder what's the more helpful behavior. If people use it for side-effects, they probably don't want to see any empty message.

[Gabriel Ebner]

Yeah, suppressing the empty message is probably more helpful.

[Mario Carneiro]

I think that suppressing empty messages should be done on the extension side. I think it is difficult to find all the places where lean can possibly send an empty message, I've run into this problem in 3 or 4 places before

[Sebastian Ullrich]

I would have made it specific to #eval, I don't know about any other parts that could send empty messages. But even then, there is a single function in the code that actually writes out the diagnostics notification to the client, so we could also filter them there.