Zulip Chat Archive

Stream: lean4

Topic: Neovim support


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Julian Berman (Apr 06 2021 at 21:13):

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

view this post on Zulip 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

view this post on Zulip Julian Berman (Apr 06 2021 at 21:15):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julian Berman (Apr 08 2021 at 02:18):

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

view this post on Zulip 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