Neovim support

Stream: lean4

[Julian Berman]

It's kind of similar to the emacs situation I suspect. In theory it's possible for people who're running neovim in a browser, otherwise slightly less so

[Julian Berman]

Mwahaha I have something resembling a persistent goal state / infoview working: https://asciinema.org/a/wRxhTBpr6sPt1Y9w7x2dBCzRZ (the annoying part is mostly now figuring out how to make it work for lean 3 and lean4 simultaneously)

[Patrick Massot]

Being able to use Lean in vim would be so awesome! But I'm afraid Ed's widgets killed that hope...

[Julian Berman]

So I still have not looked at how widgets are implemented, nor certainly talked to Ed, so I could be talking total nonsense (in fact that's likely). But to get something like widgets working outside of a browser I think basically they'd need to have their own DOM essentially

[Julian Berman]

What I know from Python-land is we have things like urwid: http://urwid.org/

[Julian Berman]

Which is a library you can use to basically support layout of dynamic elements. And when you render those in a browser they render via the DOM in that environment, but then they can be asked to render in other environments, like terminals, and when you render them there you get alternate implementations

[Julian Berman]

But yeah that's way beyond anything I've looked at so far certainly.

[Julian Berman]

Clearly also I haven't implemented the most important feature, my thing still says no goals instead of goals accomplished <giant boom>. I guess I should fix that before v1.0.0.

[Brandon Bocanegra]

What are widgets? Is this a Lean 4 specific feature?

I've used lean-mode in Emacs with little hassle thankfully, and I hope it remains this way when mathlib moves on to Lean 4.

[Julian Berman]

They're actually Lean 3 only at the minute I think. As for what they are, there's a good talk on them at I think the last Lean Together, one sec lemme see if I can find it.

[Julian Berman]

Here: https://www.youtube.com/watch?v=8NUBQEZYuis

[Brandon Bocanegra]

I see, thanks. I'd just like to comment on the remarks made around 5:53 of the video.

For an emacs solution: Emacs 28 has support for xwidgets, which allows you to essentially embed modern web browsers. Version 28 is not a stable release yet, but it should be out sometime this year.

Neovim support sounds tricky, but it's probably doable with great effort.