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