--- Begin Message ---
|
Subject: |
30.0.50; Eglot feature request: handle quirky code actions |
|
Date: |
Sun, 15 Oct 2023 03:24:45 +0100 |
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))
--- End Message ---
--- Begin Message ---
|
Subject: |
Re: bug#66552: 30.0.50; Eglot feature request: handle quirky code actions |
|
Date: |
Wed, 10 Jan 2024 03:06:11 -0800 |
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.
--- End Message ---