--server

Stream: lean4

[Reid Barton]

How hard would it be to reimplement Lean 3's lean --server interface for Lean 4?

[Mac Malone]

What is the significant difference between Lean 3's lean --sever and Lean 4's lean --server you would like to see reimplemented?

[Reid Barton]

The former is compatible with https://github.com/leanprover/lean-mode.

[Mac Malone]

And the later is compatible with https://github.com/leanprover/lean4-mode.

[Mac Malone]

i.e. I am a bit confused as to what you are looking for here

[Reid Barton]

lean4-mode basically doesn't work for me, so I would prefer to use lean-mode.

[Reid Barton]

In brief, lean-mode works too well!

[Mac Malone]

Ah, if I recall correctly, both @Sebastian Ullrich and Leo use Emacs and lean4-mode to develop Lean 4,s o I imagine they may be able to help debug any problems you may be having and/or advise in reimplementing any lost features from the transition (or explain why they were left out).

[Reid Barton]

I think most of my lean4-mode issues are results of its being built on top of Emacs's lsp-mode, so I don't have a lot of hope for fixing them

[Mac Malone]

Oh, I imagine that would be hard to fix considering how intimately the Lean 4 server and thus the language's interactivity features are tied into the LSP protocol.

[Reid Barton]

hence why I wanted to at least consider the option of starting with something that already works great (lean-mode) and sidestepping LSP entirely

[Henrik Böving]

Leo has switched to vscode by now, I also do emacs and lean4-mode, haven't really had issues in months. If you just tell us your issue I would imagine we could find a fix

Diverging from a standard like LSP just to accommodate conpatabolity with a software that we have a replacement for doesn't seems sensible to me

[Reid Barton]

There are many issues. Here is one: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/emacs/near/323963581

[Reid Barton]

Another is that messages in the minibuffer tend to appear for about 30 ms only, or flicker continuously

[Reid Barton]

I had to disable some parts of lsp-mode just to get something usable at all.

[Henrik Böving]

The issues in that thread are mostly people installing lean mode and lean4 mode at the same time or weird Unicode stuff that is fixable no?

The minibufger thing I can definitely not reproduce, works perfectly fine ootb for me.

[Mac Malone]

@Reid Barton As to your our original question, you would likely have to rewrite most of the Lean 4 server code to work with whatever protocol lean-mode was using. You would also likely have difficulty in porting many new interactive features like Widgets, which heavily exploit the LSP protocol structure to function.

[Reid Barton]

then there are a number of more minor functionality/predictability issues that I'm not sure whether to attribute to Lean 4 or to lsp-mode, e.g., error messages for unknown tactics are reported on the second character of the tactic name and so on

[Reid Barton]

I feel that lsp-mode tends to block emacs on server interactions much more than lean-mode did

[Reid Barton]

but again some of this might be difficult to separate from the Lean 3 vs Lean 4 difference

[Henrik Böving]

How about you give us your config and point to files where you are having issues so we can work towards a fix, because the default experience is really not anywhere close to as bad as you are describing.

[Sebastian Ullrich]

Reid Barton said:

Another is that messages in the minibuffer tend to appear for about 30 ms only, or flicker continuously

I can confirm this when the info view is open, haven't investigated it yet. It's hard not to think of time spent on Emacs as wasted time given the dearth of users

[Reid Barton]

Henrik Böving said:

The issues in that thread are mostly people installing lean mode and lean4 mode at the same time or weird Unicode stuff that is fixable no?

The Unicode stuff may be fixable but meanwhile it means I cannot edit files that contain non-BMP characters, e.g., all category theory files.

[Reid Barton]

Sebastian Ullrich said:

Reid Barton said:

Another is that messages in the minibuffer tend to appear for about 30 ms only, or flicker continuously

I can confirm this when the info view is open, haven't investigated it yet.

Aha, I hadn't figured out that this is connected--of course I've got the info view open a lot of the time.

[Reid Barton]

Henrik Böving said:

How about you give us your config and point to files where you are having issues so we can work towards a fix, because the default experience is really not anywhere close to as bad as you are describing.

I guess the experience depends a lot on what you are doing: writing a program, or doing a stand-alone formalization, or working on mathlib. I did AoC in December in Lean 4 and I don't remember having any issues with lean4-mode. I also wasn't using fancy unicode characters, the info view, or anything that took more than 1 second to typecheck.

[Sebastian Ullrich]

There were a few requests on the lean4-mode issue tracker about supporting eglot in addition to(/instead of?) lsp-mode. I have no idea how they compare, but it might be worth a look given that is part of Emacs 29.

[Reid Barton]

I haven't used eglot but from what I could learn about it, it looks closer to my preferences.

[Reid Barton]

One drastic option that nevertheless seems viable is to use emacs for editing only, and also open the file in VS Code. VS Code automatically rereads the file when it changes and sends the new contents to Lean.

[Johan Commelin]

I guess you could then run emacs inside a terminal pane inside VScode?

[Reid Barton]

should be possible provided VS Code doesn't steal any keybindings

[Johan Commelin]

yeah, I won't make any claims about that :see_no_evil: