lean4-minimal-mode

Stream: Emacs

[Lua Viana Reis]

Hi all. I'm sorry to have missed the previous conversation, but I have a fork of lean4-mode that uses eglot, tries to be minimal and serves a browser infoview (the latter not finished yet).
https://github.com/estradilua/lean4-minimal-mode

@Mekeor Melire since you are also working on similar things, do you want to collaborate?

[Lua Viana Reis]

@Mekeor Melire I'm also somewhat busy finishing masters (need to write the dissertation :crying_cat:) but for personal reasons I'd really like to have the infoview (I don't want to leave my emacs).

Right now the RPC communication between browser and emacs via websocket is working well, but I don't know enough react to figure out why things are not updating in the browser view

[Lua Viana Reis]

Once I have the infoview and the fringe set up, I'll probably push to melpa.

[Mekeor Melire]

Thanks for your interest and engagement.

Personally, I'm not convinced that writing a React.js application, that is opened in the webbrowser and consumes data from Emacs via websockets, is the right approach. I'd prefer a solution in Elisp.

[Notification Bot]

4 messages were moved here from #Emacs > ✔ Development: Maintainership by Mekeor Melire.

[Lua Viana Reis]

@Mekeor Melire are you aware that the lean4-infoview itself is written in React?

[Lua Viana Reis]

in fact, there is no need to use React in my wrapper around the infoview, and I may just remove it. But unless you recreate the whole infoview, there is no escape from "using" React. Do you have another idea?

[Lua Viana Reis]

TBF, the question in the title of the topic you created is to some extend rethoric. Either you use lean4-infoview as an application in a browser, or you don't use the infoview or anything that supports widgets (since they are, by definition, React HTML applets).

[Lua Viana Reis]

whether this aforementioned browser is running inside or outside of your editor is a matter of support and taste. But it is a browser nevertheless.

[Mauricio Collares]

What does neovim do?

[Henrik Böving]

@Julian Berman can probably explain this better but it's basically a reimplementation of large chunks what the react application does but from within neovim as I understand. It does notably not support widgets but all the other good stuff like hovering in the middle of terms in the infoview and such just works.

[Mekeor Melire]

For a web application like VS Code, it's fine to implement the Info in React.js. Emacs Lean4-Mode already has an Info that is implemented in Elisp. It's not feature-complete or whatsoever, but we should work on it rather than using React.js, if you ask me.

@Yury G. Kudryashov is the official maintainer, if you want an official opinion or decision on this matter.

[Mekeor Melire]

And my argument is not only meant for React.js specifically but also generally on JavaScript, or even using an external web browser.

[Mekeor Melire]

(When Lean4-Mode has basic support for Eglot, we'll need to investigate whether we want to make the already existing lean4-info module to work with Eglot, too, that is in addition to lsp-mode. Or if we want to use Eldoc as an informational view for Eglot, because that's the default for it.)

[Mekeor Melire]

lean.nvim implements Infoview in Lua, just like Emacs Lean4-Mode uses Elisp in lean4-info.el: https://github.com/Julian/lean.nvim/blob/main/lua/lean/infoview.lua

[Lua Viana Reis]

What is the problem with javascript specifically?

[Lua Viana Reis]

Mekeor Melire said:

lean.nvim implements Infoview in Lua, just like Emacs Lean4-Mode uses Elisp in lean4-info.el: https://github.com/Julian/lean.nvim/blob/main/lua/lean/infoview.lua

My issue with this approach is that, while it has the advantage of working in a terminal-only environment, it cannot support more advanced widgets and is a burden to implement and maintain. Re-using lean4-infoview means that every new feature there is readily available in the Emacs package.

[Lua Viana Reis]

But even if you want to use terminal emacs remotely via SSH, you can just open the remote infoview webpage locally and it would work. You can even open the infoview in your tablet or phone if you want. I don't think supporting the unlikely situation where a browser is completely inaccessible is worth this much work...

[Julian Berman]

Henrik Böving said:

Julian Berman can probably explain this better but it's basically a reimplementation of large chunks what the react application does but from within neovim as I understand.

This is right, yeah, as you all linked. I will say a not-so-secret announcement is that more advanced widgets are also now working (some on main, some on a branch). Not all (i.e. we still don't render fancy animated JS which really does depend on having a browser) -- but reaching Mathlib things like conv? and unfold? and friends.

More generally I don't know that there's a fully objective "right" answer here between "reimplement in the host language [lua|elisp]" vs "use lean4-infoview via a Javascript engine". Yes it's nice to have to do the work (and it's a lot of work). On the other hand I certainly use neovim for many reasons, a small one of them is precisely not to have neither external windows (which are less integrated in the overall terminal [or emacs] centric workflow, powerful as it is) nor browsers (which besides the above come with extra baggage.)

To me a nice distant future has a third option emerge here, which is that those of us who care about this help build a layer which minimizes how much a browser really matters. In other words, only once someone really has a thing written in HTML+JS should it be needed to render HTML+JS -- the actual lingua franca to define widgets and the infoview more broadly could be something which is maybe more amenable to multiple rendering models. I have some ideas for what that looks like but not fully detailed ones, not until I finish with this last bit of widget work.

I should also say that I intend to some day get lean4-infoview also working, which should be easy (I'll have a Lua infoview API which is "externally managed" and just renders in the way you have it). But yeah for me this is a secondary option.

In short I have no advice :) it's a preference question, but I'm happy to help think it through.

[Lua Viana Reis]

a small one of them is precisely not to have neither external windows (which are less integrated in the overall terminal [or emacs] centric workflow, powerful as it is) nor browsers

I think it's helpful to add that in the case of Emacs, since it is commonly run in a gui frame, you can also open the served infoview as an Emacs window if you want (either using xwidgets/webkit — which is currently broken in some OSes, but that's another issue — or something else like EAF).

[Julian Berman]

Yeah this is possible in Neovim too these days (and in fact that's the case even in a terminal now, given there are simple browsers like awrit which I'd bet could render lean4-infoview inside a Neovim :terminal window). I still don't personally like that solution, because every application of course has its own UX and one of the nice things about being inside Neovim (and emacs, in my small amount of emacs life) is that all of what you're doing "feels" the same, and this isn't the case if you have 2 applications you're switching between.

[Julian Berman]

A silly example perhaps just because coincidentally I was thinking about this morning before seeing this thread is I want to implement a text motion for moving to the next/previous subexpression in the infoview goal state. Of course as long as everything is within the editor it's all fair game to do so, and of course if you're in some other application, you're on your own (and you're going to be figuring out whether or how to add that to lean4-infoview).

[Lua Viana Reis]

I see, and I think that's a very valid point. In my case, I'm just frustrated with how Emacs is lagging behind in terms of good support, and I think having the same infoview as VSCode (which is the main editor for Lean user, nowadays) would go a long way. Part of the "UX" niceties can be achieved with CSS, and you can also implement and send custom RPC commands to the webpage if you want.

[Lua Viana Reis]

It's certainly more mouse-oriented and not "native" to the editor. But it solves my problem which is that I want to have my Emacs environment while editing Lean, without the need to keep another VSCode window open.

[Mekeor Melire]

Julian Berman said:

To me a nice distant future has a third option emerge here, which is that those of us who care about this help build a layer which minimizes how much a browser really matters.

That'd be really great!

[Mekeor Melire]

Lua Viana Reis said:

open the served infoview as an Emacs window if you want (either using xwidgets/webkit — which is currently broken in some OSes, but that's another issue — or something else like EAF).

Note that only a fraction of Emacs users have built Emacs with Xwidgets support and EAF is a pain to install.

[Lua Viana Reis]

Yes, I'm not counting on that (but I hope that xwidgets is brought back soon!)

[Mekeor Melire]

Would it be possible and make sense to put a process in between the LSP server and Emacs, which does not only forward the communicated data, but also forwards infoview-relevant data to the infoview-rendering web application? That way, we wouldn't put another burden on single-threaded Emacs that is already struggling with incoming LSP data; and also, we wouldn't touch Lean4-Mode code at all.

[Lua Viana Reis]

in case you have a tablet, it's also a nice experience to open the infoview there :) it makes it look like a "leanpad". I'll send a video when I make it pretty

[Lua Viana Reis]

(not claiming that it's actually useful, though :p but perhaps it could be)

[Mekeor Melire]

Lua Viana Reis said:

I'm just frustrated with how Emacs is lagging behind in terms of good support

I'm also frustrated by that. We're all! :(

[Mekeor Melire]

By the way, I don't find lean4-minimal-mode a fair naming of your fork, since it arguably introduces many, many external dependencies.

[Lua Viana Reis]

Mekeor Melire said:

Would it be possible and make sense to put a process in between the LSP server and Emacs, which does not only forward the communicated data, but also forwards infoview-relevant data to the infoview-rendering web application? That way, we wouldn't put another burden on single-threaded Emacs that is already struggling with incoming LSP data; and also, we wouldn't touch Lean4-Mode code at all.

If Lean had working HTTP and websocket implementations, I would have done this directly there (so it would work in any editor!).

[Lua Viana Reis]

Mekeor Melire said:

By the way, I don't find lean4-minimal-mode a fair naming of your fork, since it arguably introduces many, many external dependencies.

minimal as in: easy to maintain and I'm doing as little work as possible. And I'm not sure what external dependencies you are talking about. Probably "the browser" but welp, isn't that already installed?

[Mekeor Melire]

The NPM package dependencies are listed here: https://github.com/estradilua/lean4-minimal-mode/blob/main/infoview/package-lock.json
But more importantly, it introduces another language and framework, that maintainers must be familiar with.

[Mekeor Melire]

Lua Viana Reis said:

If Lean had working HTTP and websocket implementations, I would have done this directly there (so it would work in any editor!).

Maybe it's possible without websockets.

[Lua Viana Reis]

You must communicate with the browser window somehow. The alternative I see would be a REST API, I think it would also work

[Lua Viana Reis]

but the problem with a REST API is that afaik there is no straightforward way for the server to send a request to the webpage, so I think it would involve some polling and therefore probably would be slower

[Lua Viana Reis]

Mekeor Melire said:

The NPM package dependencies are listed here: https://github.com/estradilua/lean4-minimal-mode/blob/main/infoview/package-lock.json
But more importantly, it introduces another language and framework, that maintainers must be familiar with.

I see. But these are transitive dependencies of lean4-infoview, so again, it's a requirement if you are working with it.

[Mekeor Melire]

Perhaps you could just read the data from the LSP server from its socket or via standard input/output, and provide websockets to the webbrowser. And you'd need to bidirectionally forward data between the LSP server and Emacs.

[Lua Viana Reis]

Mekeor Melire said:

Perhaps you could just read the data from the LSP server from its socket or via standard input/output, and provide websockets to the webbrowser. And you'd need to bidirectionally forward data between the LSP server and Emacs.

I think that's what I've done currently, basically?

[Lua Viana Reis]

or do you mean, with a process in the middle outside of emacs? (like something in Rust?)

[Mekeor Melire]

Yes, I meant a process in the middle, outside of Emacs.

[Mekeor Melire]

Node.js should also work, but is also single-threaded at its core.

[Mekeor Melire]

(But that'd be fine because the main objective is to relieve Emacs.)

[Lua Viana Reis]

it's possible, but personaly I have not felt that having emacs be the process in the middle made it slower in any noticeable way. I see the advantage of doing it directly in Lean, but if performance is not an issue at first, then I would prefer to stick with Emacs

[Luke Naylor]

Has anybody made such a process in the middle since this conversation?

[Lua Viana Reis]

@Luke Naylor what would be your use case for it? (to see if I could help)