issue with emacs lean4-mode

Stream: lean4

[Tomas Skrivan]

For quite some time I'm having issues with Emacs lean4-mode. If I work with non-trivial file, very soon I run to an issue that I need to constantly call (lean4-refresh-file-dependencies) after almost anything I write as the file is not getting properly parsed. For example, I'm getting constantly errors of type unknown identifier 'byaesop' when I write by aesop.

I'm running Emacs 28.1, lean4-mode commit 43f5e2b, and lean version leanprover/lean4:nightly-2023-06-20.

Anyone experiencing something similar? If not, what versions are you running?

[Reid Barton]

Does your file have any non-BMP unicode characters?

[Tomas Skrivan]

Is 𝕜 non-BMP? How do I figure out if a character is non-BMP?

[Ruben Van de Velde]

It's in the BMP if it has at most four hexadecimal digits, so \bbk is in plane 1

[Ruben Van de Velde]

https://en.m.wikipedia.org/wiki/Plane_(Unicode) for background

[Tomas Skrivan]

From wiki "a plane is a continuous group of 65,536 (216) code points" and "Plane 0 is the Basic Multilingual Plane (BMP)"

[Tomas Skrivan]

So I think 𝕜 should be non-BMP and the compart site says that it is in "Supplementary Multilingual Plane, U+10000 - U+1FFFF"

[Tomas Skrivan]

Hah, even → is non-BMP, if non-BMP characters are causing this issue that this is really bad. They are practically unavoidable.

[Wojciech Nawrocki]

I have no idea whether this is related, but lsp-mode (which lean4-mode uses) is known not to handle Unicode properly.

[Mauricio Collares]

Did you try emacs 29? I know it's a prerelease, but it includes a bunch of Unicode improvements, and maybe this helps even if lsp-mode has problems. I don't think I've seen the same bug and I use emacs 29.

[Tomas Skrivan]

The odd thing is that I didn't use to have these problems. It was working just fine some time ago.

[Sebastian Ullrich]

Are you sure you had non-BMP characters at that point? → is in the BMP

[Tomas Skrivan]

Ohh ... now I'm looking at all the unicode characters I use most of the time and they are all in BMP

[Tomas Skrivan]

Ok I will remove all non-BMP characters and see if the issue persists

[Yury G. Kudryashov]

Usually I have this issue when I have a non-BMP character in the same line. I just restart lean server.

[Alexandre Rademaker]

In a Warnings buffer, I am getting a lot of messages like

:no_entry: Warning (lsp-mode): Unknown request method: workspace/inlayHint/refresh

Any idea? This is my configuration of the lean4-mode:

(straight-use-package 'dash)
(straight-use-package 'lsp-mode)
(straight-use-package 'magit-section)

(use-package lean4-mode
  :commands lean4-mode
  :straight (lean4-mode :type git :host github
            :repo "leanprover-community/lean4-mode"
            :files ("*.el" "data")))

I am using emacsclient to connect to a emacs daemon. The setup followed the ideas from http://yitang.uk/2023/02/09/emacs-as-service-in-macos/. I am running MacOS with the emacs-plus@30 (https://github.com/d12frosted/homebrew-emacs-plus) installed via Homebrew.

[Julian Berman]

See #Emacs > inlayHint I think for a workaround.