lean4-mode on eglot

Stream: lean4

[Richard Copley]

The Emacs mdoe isn't in a great place. It has a few little bugs that make it hard to use out of the box. They can be fixed but @Sebastian Ullrich doesn't have the time. It's based on lsp-mode, which is generally very nice, but sadly doesn't compute character positions correctly, so that it crashes when editing files that contain characters outside the Unicode BMP, like 𝓝 (\nhds).

If these things don't get fixed it's no surprise that the Emacs mode doesn't have too many users. But it does have some users!

To do the Topology chapter of @Patrick Massot's #mil, I switched briefly to VS Code, but I didn't enjoy it. Hence my Eglot fork of lean4-mode. As @Siddhartha Gadgil implies, when you make the choice to use Emacs, you generally accept that fixing Emacs is your job now! :smile:

[Mauricio Collares]

Ooh, lean4-mode on eglot sounds amazing. Would be cool if that became the official version.

[Mauricio Collares]

There are a couple of typos in lean4-fringe.el: eglot-uri-to-path probably should be eglot--uri-to-path, and similarly eglot-range-region should likely be eglot--range-region.

[Richard Copley]

@Mauricio Collares The spellings were changed when Eglot moved to core Emacs (version 29?). I could use the obsolete aliases, but there would be warnings. Are you in a position to upgrade Emacs ([Edit:] or M-x package-delete RET eglot RET if you're already using Emacs 29)?

[Mauricio Collares]

I'm using Eglot from Emacs 29.1 (i.e. not from ELPA), but indeed I now see that this changed last month in emacs master. Thanks for the pointer! I think I will take the easy way out and just wait for eglot 1.16 to appear on ELPA.

[Notification Bot]

A message was moved here from #lean4 > normalising whitespace by Richard Copley.

[Notification Bot]

A message was moved from this topic to #lean4 > lean4-mode on eglot by Richard Copley.

[Richard Copley]

@Mauricio Collares In that case I should probably use the old names for now.

[Richard Copley]

Richard Copley said:

Mauricio Collares In that case I should probably use the old names for now.

Done.

[Mauricio Collares]

Thank you!

[Richard Copley]

Thanks for trying it out!

[David Thrane Christiansen]

Did eglot start supporting semantic tokens?

[Jannis Limperg]

Apparently not, and indeed when I just tried Richard's fork it didn't highlight correctly.

[Richard Copley]

There's also a PR for semantic tokens (#615 [Edit: #839]), which is moving slowly but doesn't seem to be forgotten.

[Richard Copley]

I have just pushed a fix for a mistake in my work-around for code actions.

[David Thrane Christiansen]

That's a shame - it's the only thing blocking me from getting everything over into eglot, which has nicer integration with the rest of the system.