## Stream: lean4

### Topic: Neovim support

#### Julian Berman (Feb 01 2021 at 11:36):

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 (Apr 06 2021 at 20:57):

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 (Apr 06 2021 at 21:06):

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

#### Julian Berman (Apr 06 2021 at 21:13):

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 (Apr 06 2021 at 21:13):

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

#### Julian Berman (Apr 06 2021 at 21:14):

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 (Apr 06 2021 at 21:15):

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

#### Julian Berman (Apr 06 2021 at 21:21):

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 (Apr 08 2021 at 02:07):

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 (Apr 08 2021 at 02:18):

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.

#### Brandon Bocanegra (Apr 09 2021 at 02:06):

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.

Last updated: May 07 2021 at 11:09 UTC