Zulip Chat Archive

Stream: lean4

Topic: issue with emacs lean4-mode


Tomas Skrivan (Jul 11 2023 at 15:48):

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 (Jul 11 2023 at 15:49):

Does your file have any non-BMP unicode characters?

Tomas Skrivan (Jul 11 2023 at 16:02):

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

Ruben Van de Velde (Jul 11 2023 at 16:04):

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

Ruben Van de Velde (Jul 11 2023 at 16:05):

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

Tomas Skrivan (Jul 11 2023 at 16:06):

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 (Jul 11 2023 at 16:07):

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 (Jul 11 2023 at 16:19):

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

Wojciech Nawrocki (Jul 11 2023 at 16:34):

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

Mauricio Collares (Jul 11 2023 at 16:55):

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 (Jul 11 2023 at 17:44):

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

Sebastian Ullrich (Jul 11 2023 at 17:50):

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

Tomas Skrivan (Jul 11 2023 at 17:57):

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

Tomas Skrivan (Jul 11 2023 at 17:58):

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

Yury G. Kudryashov (Jul 11 2023 at 20:32):

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


Last updated: Dec 20 2023 at 11:08 UTC