bug#66552: 30.0.50; Eglot feature request: handle quirky code actions

[Richard Copley]

On Tue, 17 Oct 2023 at 04:11, João Távora <joaotavora@gmail.com> wrote:
>
> On Sun, Oct 15, 2023 at 3:25 AM Richard Copley <rcopley@gmail.com> wrote:
> >
> > The language server for Lean 4 [1] provides code actions with a couple
> > of features that make it difficult to apply them from within Eglot.
> >
> > [1] https://github.com/leanprover/lean4
> >
> > Firstly, the textDocument version field has the value 0, which is
> > generally not equal to the version in `eglot--versioned-identifier',
> > resulting in the error "Edits on `%s' require version %d, you have %d"
> > from `eglot--apply-text-edits'.
> >
> > Secondly, all the suggestions have the same title ("Apply 'Try this'"),
> > which means an alist using the title as the key can't be used in
> > completing-read as in `eglot--read-execute-code-action'.
> >
> > Could you provide options to ignore the version, and to use the newText
> >  (JSONPath $.result[:1].edit.documentChanges[:1].edits[:1].newText)
> > instead of the title?
>
> I understand the problem, thanks for describing it nicely.

Thanks for reading it!

> Anyway, I don't think patching this in a client like Eglot is
> recommended.  Both these thinks are bugs in the language server
> and should be fixed there.  Eglot is an LSP client which works
> with tens, maybe hundreds, of servers, it can't bloat itself
> to work around every server's quirks.
>
> For the version field, servers don't _have_ to send one (if I
> remember correctly).

To judge from comments in the Lean 4 sources, the authors wanted to
send null, but found that VS code requires a version number (which it
ignores), so they send 0 as a workaround. It apparently didn't occur
to them to send the correct version, which it turns out is readily
available. Indeed, it's extra work to throw it away.

> If a servers sends no field, Eglot will
> ignore it.  If it sends a wrong one, Eglot won't.

> You could work around it with a monkey-patch by advising
> eglot--apply-text-edits to always have a null second argument.

I'll probably go with that. Thanks for the suggestion. It's a shame
that this will affect all languages. It would be nice if I could use a
defmethod dispatching on a subclass of eglot-lsp-server! But
eglot--apply-text-edits doesn't take a server, so it isn't generic.

> The second labeling problem is even more bizarre  Again, you
> can probably monkey-patch Eglot to work around it.

Here I'm not sure I agree. The title is only specified to be "A short,
human-readable, title for this code action". In this case the
suggestions are computed, and inventing unique friendly names for them
isn't feasible. "Apply 'Try this'" seems sensible. It refers to the
text of the corresponding diagnostic, "Try this : <newText>".

> But I really think you should report these two things to the
> language server authors.

I think so too, but raising issues against the core language doesn't
seem to be encouraged. They're going through a reorganisation, so
perhaps things will improve.

> João