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

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

[Richard Copley]

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?

Here is an example request and reply. The reply is cut down from an
original list of over 200 suggestions.

[client-request]
(:jsonrpc "2.0" :id 777 :method "textDocument/codeAction" :params
          (:textDocument
           (:uri "file:///s%3A/projects/lean/float/Fl/Lemmas.lean") :range
           (:start (:line 50 :character 2) :end (:line 50 :character 8))
           :context (:diagnostics [])))

[server-reply]
(:result
 [(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
          (:documentChanges
           [(:textDocument
             (:version 0 :uri "file:///s%3A/Fl/Lemmas.lean")
             :edits
             [(:range
               (:start (:line 50 :character 2) :end (:line 50 :character 8))
               :newText "refine Nat.add_left_cancel ?_")])]
           :changes nil :changeAnnotations nil))
  (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
          (:documentChanges
           [(:textDocument
             (:version 0 :uri "file:///s%3A/Fl/Lemmas.lean")
             :edits
             [(:range
               (:start (:line 50 :character 2) :end (:line 50 :character 8))
               :newText "refine Nat.add_right_cancel ?_")])]
           :changes nil :changeAnnotations nil))
  (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
          (:documentChanges
           [(:textDocument
             (:version 0 :uri "file:///s%3A/Fl/Lemmas.lean")
             :edits
             [(:range
               (:start (:line 50 :character 2) :end (:line 50 :character 8))
               :newText "refine Nat.eq_of_mul_eq_mul_right ?_")])]
           :changes nil :changeAnnotations nil))
  (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
          (:documentChanges
           [(:textDocument
             (:version 0 :uri "file:///s%3A/Fl/Lemmas.lean")
             :edits
             [(:range
               (:start (:line 50 :character 2) :end (:line 50 :character 8))
               :newText "refine Nat.eq_of_mul_eq_mul_left ?_")])]
           :changes nil :changeAnnotations nil))]
 :jsonrpc "2.0" :id 777)



In GNU Emacs 30.0.50 (build 1, x86_64-w64-mingw32) of 2023-10-12 built
 on MACHINE
Repository revision: 90b4a7acb5332ed490cb2b456cfe8c11af8c9d4f
Repository branch: master
Windowing system distributor 'Microsoft Corp.', version 10.0.19045
System Description: Microsoft Windows 10 Pro (v10.0.2009.19045.3448)

Configured using:

'configure --config-cache --with-modules --without-pop
--without-compress-install --with-tree-sitter --without-libsystemd
--without-dbus --without-gconf --without-gsettings --without-mailutils
--with-small-ja-dic --with-native-compilation --prefix=/mingw64
--build=x86_64-w64-mingw32

Configured features:
ACL GIF GMP GNUTLS HARFBUZZ JPEG JSON LCMS2 LIBXML2 MODULES NATIVE_COMP
NOTIFY W32NOTIFY PDUMPER PNG RSVG SOUND SQLITE3 THREADS TIFF
TOOLKIT_SCROLL_BARS TREE_SITTER WEBP XPM ZLIB

Important settings:
  value of $LANG: ENG
  locale-coding-system: cp1252

Major mode: Lean 4

Minor modes in effect:
  eglot--managed-mode: t
  flymake-mode: t
  tooltip-mode: t
  global-eldoc-mode: t
  eldoc-mode: t
  show-paren-mode: t
  mouse-wheel-mode: t
  tool-bar-mode: t
  menu-bar-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  blink-cursor-mode: t
  minibuffer-regexp-mode: t
  line-number-mode: t
  transient-mark-mode: t
  auto-composition-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t

Features:
(shadow sort mail-extr emacsbug message mailcap yank-media puny rfc822
mml mml-sec epa derived epg rfc6068 epg-config gnus-util mm-decode
mm-bodies mm-encode mail-parse rfc2231 mailabbrev gmm-utils mailheader
sendmail rfc2047 rfc2045 ietf-drums mm-util mail-prsvr mail-utils
help-fns radix-tree cl-print files-x find-dired dired dired-loaddefs
grep time-date lean4-input quail comp comp-cstr cl-extra lean4-mode
lean4-fringe lean4-dev lean4-info magit-section format-spec
cursor-sensor compat lean4-syntax lean4-util lean4-settings f f-shortdoc
s lean4-eri eglot external-completion jsonrpc xref flymake thingatpt
project diff diff-mode easy-mmode ert pp ewoc debug backtrace filenotify
warnings icons compile text-property-search comint ansi-osc ring
url-util url-parse auth-source cl-seq eieio eieio-core cl-macs
password-cache url-vars imenu flycheck ansi-color json map byte-opt gv
bytecomp byte-compile find-func help-mode rx subr-x pcase dash
cl-loaddefs cl-lib cus-start cus-load rmc iso-transl tooltip cconv eldoc
paren electric uniquify ediff-hook vc-hooks lisp-float-type elisp-mode
mwheel dos-w32 ls-lisp disp-table term/w32-win w32-win w32-vars
term/common-win touch-screen tool-bar dnd fontset image regexp-opt
fringe tabulated-list replace newcomment text-mode lisp-mode prog-mode
register page tab-bar menu-bar rfn-eshadow isearch easymenu timer select
scroll-bar mouse jit-lock font-lock syntax font-core term/tty-colors
frame minibuffer nadvice seq simple cl-generic indonesian philippine
cham georgian utf-8-lang misc-lang vietnamese tibetan thai tai-viet lao
korean japanese eucjp-ms cp51932 hebrew greek romanian slovak czech
european ethiopic indian cyrillic chinese composite emoji-zwj charscript
charprop case-table epa-hook jka-cmpr-hook help abbrev obarray oclosure
cl-preloaded button loaddefs theme-loaddefs faces cus-face macroexp
files window text-properties overlay sha1 md5 base64 format env
code-pages mule custom widget keymap hashtable-print-readable backquote
threads w32notify w32 lcms2 multi-tty move-toolbar make-network-process
native-compile emacs)

Memory information:
((conses 16 230339 30888) (symbols 48 15071 0) (strings 32 50446 4052)
 (string-bytes 1 1546772) (vectors 16 36238)
 (vector-slots 8 716441 24950) (floats 8 77 40) (intervals 56 927 39)
 (buffers 992 18))

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

[Dmitry Gutov]

Cc'ing Joao.

On 15/10/2023 05:24, Richard Copley 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?
> 
> Here is an example request and reply. The reply is cut down from an
> original list of over 200 suggestions.
> 
> [client-request]
> (:jsonrpc "2.0" :id 777 :method "textDocument/codeAction" :params
>            (:textDocument
>             (:uri"file:///s%3A/projects/lean/float/Fl/Lemmas.lean") :range
>             (:start (:line 50 :character 2) :end (:line 50 :character 8))
>             :context (:diagnostics [])))
> 
> [server-reply]
> (:result
>   [(:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
>            (:documentChanges
>             [(:textDocument
>               (:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
>               :edits
>               [(:range
>                 (:start (:line 50 :character 2) :end (:line 50 :character 8))
>                 :newText "refine Nat.add_left_cancel ?_")])]
>             :changes nil :changeAnnotations nil))
>    (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
>            (:documentChanges
>             [(:textDocument
>               (:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
>               :edits
>               [(:range
>                 (:start (:line 50 :character 2) :end (:line 50 :character 8))
>                 :newText "refine Nat.add_right_cancel ?_")])]
>             :changes nil :changeAnnotations nil))
>    (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
>            (:documentChanges
>             [(:textDocument
>               (:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
>               :edits
>               [(:range
>                 (:start (:line 50 :character 2) :end (:line 50 :character 8))
>                 :newText "refine Nat.eq_of_mul_eq_mul_right ?_")])]
>             :changes nil :changeAnnotations nil))
>    (:title "Apply 'Try this'" :kind "quickfix" :isPreferred t :edit
>            (:documentChanges
>             [(:textDocument
>               (:version 0 :uri"file:///s%3A/Fl/Lemmas.lean")
>               :edits
>               [(:range
>                 (:start (:line 50 :character 2) :end (:line 50 :character 8))
>                 :newText "refine Nat.eq_of_mul_eq_mul_left ?_")])]
>             :changes nil :changeAnnotations nil))]
>   :jsonrpc "2.0" :id 777)

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

[João Távora]

On Tue, Oct 17, 2023 at 12:22 AM Dmitry Gutov <dmitry@gutov.dev> wrote:
>
> Cc'ing Joao.

Thanks for pinging me:  I'll reply to the original message.

João

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

[João Távora]

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.

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).  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.

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

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

João

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

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

[João Távora]

On Tue, Oct 17, 2023 at 8:08 PM Richard Copley <rcopley@gmail.com> wrote:

> > 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.

For eglot--apply-text-edits to become a generic, it would first
have to be promoted to Eglot's user API (losing the --), and I
don't see a very good reason to do that right now.

However, if you wanted a fully "legal" solution, I think you could
place a server-specific method on

  eglot-handle-request (server your-server) (method workspace/applyEdit)

which removes or massages the `version` cookie in the `edit` keyword
argument.

And even with the monkey-patching approach, you can make something
server specific by checking the return value of `eglot-current-server`
before tweaking the value.

Another possibility is for Eglot to start interpreting version 0 as
"any version".  It should be feasible since Eglot controls the
start of the numbering, which right now is 0 but be increased to 1,
hopefully without any negative consequences.

> > 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>".

This newText is hidden deep inside the `edits` field of such messages.
There's no guarantee it's a 1-element array or even that the edit
is just an insertion.  So grabbing it consistently to craft a
user-visible message is just a bad idea

It doesn't make sense for a language server to provide a bunch
of actions with identical labels.  It isn't something the client
should have to deal with.  A label, to me, is a piece of information
for telling one object apart from another object.  If the text of the
corresponding diagnostic is (presumably unique), why can't
the label be unique as well?

João

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

[Richard Copley]

On Tue, 17 Oct 2023 at 22:38, João Távora <joaotavora@gmail.com> wrote:
>
> On Tue, Oct 17, 2023 at 8:08 PM Richard Copley <rcopley@gmail.com> wrote:
>
> > > 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.
>
> For eglot--apply-text-edits to become a generic, it would first
> have to be promoted to Eglot's user API (losing the --), and I
> don't see a very good reason to do that right now.
>
> However, if you wanted a fully "legal" solution, I think you could
> place a server-specific method on
>
>   eglot-handle-request (server your-server) (method workspace/applyEdit)
>
> which removes or massages the `version` cookie in the `edit` keyword
> argument.

In my case the reply to the textDocument/codeAction client request
contains the full WorkspaceEdit, so there is no workspace/applyEdit
server request involved. The edits are applied directly
(eglot-code-actions (interactive) -> eglot--read-execute-code-action
-> eglot-execute -> eglot--apply-workspace-edit). I'm using :before
advice on eglot--read-execute-code-action to massage the list of
actions (both the version number and the title text).

> And even with the monkey-patching approach, you can make something
> server specific by checking the return value of `eglot-current-server`
> before tweaking the value.

I will do that, thanks.

> Another possibility is for Eglot to start interpreting version 0 as
> "any version".  It should be feasible since Eglot controls the
> start of the numbering, which right now is 0 but be increased to 1,
> hopefully without any negative consequences.
>
> > > 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>".
>
> This newText is hidden deep inside the `edits` field of such messages.
> There's no guarantee it's a 1-element array or even that the edit
> is just an insertion.  So grabbing it consistently to craft a
> user-visible message is just a bad idea

That's true.

> It doesn't make sense for a language server to provide a bunch
> of actions with identical labels.  It isn't something the client
> should have to deal with.  A label, to me, is a piece of information
> for telling one object apart from another object.  If the text of the
> corresponding diagnostic is (presumably unique), why can't
> the label be unique as well?

But these aren't labels, they're titles, and given the specification,
the authors providing code actions won't necessarily foresee their use
as labels, as sensible as it is from the client's point of view. The
message from the diagnostics *could* be used as the title, but I'd
find it hard to argue to the developers that it *should*. That's no
help to you, of course! I agree that my suggestion of building a label
from the newText is a non-starter in the general case. For the time
being it will work for my case, but if Lean 4 starts providing
refactoring support, for example, I'll have to think again.

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:

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

The issue with the incorrect version number in server edits will be
fixed soon. Thanks for the encouragement!

Core Lean 4 language: #2721 [1]
Standard library: #306 [2]
Mathematics library: #7812 [3]

[1] https://github.com/leanprover/lean4/pull/2721
[2] https://github.com/leanprover/std4/pull/306
[3] https://github.com/leanprover-community/mathlib4/pull/7812

I will need to rest and recuperate before advocating for the other
thing to be fixed.

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

[Stefan Kangas]

Richard Copley <rcopley@gmail.com> writes:

> On Tue, 17 Oct 2023 at 04:11, João Távora <joaotavora@gmail.com> wrote:
>
>> But I really think you should report these two things to the
>> language server authors.
>
> The issue with the incorrect version number in server edits will be
> fixed soon. Thanks for the encouragement!
>
> Core Lean 4 language: #2721 [1]
> Standard library: #306 [2]
> Mathematics library: #7812 [3]
>
> [1] https://github.com/leanprover/lean4/pull/2721
> [2] https://github.com/leanprover/std4/pull/306
> [3] https://github.com/leanprover-community/mathlib4/pull/7812
>
> I will need to rest and recuperate before advocating for the other
> thing to be fixed.

Thanks for reporting that upstream.  Meanwhile, I don't think it makes
sense to keep this bug report open, so I'm closing it now.