Infoview doesn't show errors when lake fails about vscode-lean4

[lovettchris]

@gebner - interesting, I see a red squiggly on import A and the tool tip matches what you see below, this message flashes real quick in the infoview then it disappears.

and I think it is because the call to 'Lean.Widget.getInteractiveDiagnostics' returns [] which clears the infoview. So the infoview must be showing the red squiggle info first, then calls getInteractiveDiagnostics and that wipes the message. Is this a Lean LSP bug ?

[gebner]

Is this a Lean LSP bug ?

In some sense, maybe. I guess you could argue that they are not "real" Lean diagnostics, and getInteractiveDiagnostics should only return diagnostics created by the Lean compiler. In either case, this part of the RPC API is underspecified.

[leodemoura]

@gebner Is it clear to you what needs to be done to address this issue?

[gebner]

Yes, I just need to close it. 😄 Mariana fixed this in #173.