Is web editor good-enough for IDE plugin?

Stream: general

[Daniel Donnelly]

Was wondering if I could make an IDE for Lean by just directing a browser widget to the lean prover address. Should I need to parse any of the language input by the user, I just grab the html of the browser widget. Or is the web editor version limited in some way?

Reason is all the complicated steps required to install Lean and its dependencies. Then you have to reverse-engineer the web editor anyway to see how the JSON communications work in server mode.

[Patrick Massot]

The Lean web editor is way too slow.

[Patrick Massot]

And installing Lean is not complicated.

[Daniel Donnelly]

@Patrick Massot okay, cool I will try making an installer then. :D

[Patrick Massot]

What is currently too complicated is installing mathlib tooling.

[Patrick Massot]

Installing Lean itself is as simple as downloading and extracting a zip file.

[Daniel Donnelly]

@Patrick Massot that's good. That would make it ideal for packaging in an app's installer.