Intellij Plugin?

Stream: lean4

[Matt Yan]

is there Intellij support?

[Henrik Böving]

Not at the moment...I also dont think there ever will be, for programming and proving in Lean you will definitely want to use the goal window etc. so it would most likely be a very non trivial intellij extension to make and right now most people are happy with just the vscode plugin and the emacs one and the community is quite small as well right now.

[Patrick Stevens]

Though if you're wedded to JetBrains and are interested in this kind of thing, you could give their Arend a try (it's HoTT-based, and completely unrelated to Lean).

[Matt Yan]

LEAN looks too good to be given up, I'll maybe just use intellij key bindings in vs code :stuck_out_tongue_closed_eyes:

[Reid Barton]

(BTW, the correct spelling is just "Lean".)

[Arthur Paulino]

I wonder if it's possible to make a plugin for Atom though. Lot's of people like Atom

[Henrik Böving]

I mean it's definitely possible to make plugins for Atom Intellij etc., its just that nobody has done it yet. And since most people are simply happy with the extensions there are and Lean 4's user base will (at least for a while) mostly consist of mathematicians who (mostly) dont care about editors anyways nobody has done it yet.

[Arthur Paulino]

It's true, but Lean 4 has potential to attract developers of all sorts (who like functional programming :smiley: )

[Joachim Breitner]

mostly consist of mathematicians who (mostly) dont care about editors

unless they are editors of their favorite journal, of course ;-)

[Alex J. Best]

Its also much harder to get a good lean plugin than for most languages of course, you need something that not just does syntax highlighting and jump to definition etc but rendering widgets in the goal state and all this other fanciness for the full user experience. Given that lean 3 wasn't based on LSP this was an even bigger barrier to people adding other extensions, with lean 4 this may indeed be easier than lean 3 for that reason.

[Arthur Paulino]

Yeah it requires an great amount of work

[Julian Berman]

FWIW there is already a fourth editor working on Lean support, I think by.. @Anders Christiansen Sørby

[Julian Berman]

It's helix: https://github.com/helix-editor/helix

[Julian Berman]

But still not something in the "Enterprise My Editor" space :P

[Anders Christiansen Sørby]

Yep, thanks to the tree-sitter-lean a lot of editors can do syntax highlights