online code editor for Lean

Stream: general

[shanek]

Hi all,

Would anybody be interested in an online replit-style code editor for Lean? This would make the barrier to entry easier since you wouldn't have to download anything -- sort of similar to Overleaf versus a local LaTeX editor. I'm a math student playing around with building webapps, and was thinking that could be an interesting side project. Just curious, thanks!

[Eric Wieser]

Are you aware of https://live.lean-lang.org?

[shanek]

Eric Wieser said:

Are you aware of https://live.lean-lang.org?

I wasn't, but that's cool!! The webapp I was thinking would be a step further than that one. You would be able to login to it and have your previous work (among other customized things).

[Eric Wieser]

For that end, I find gitpod or GitHub codespaces to be pretty good

[Eric Wieser]

Neither is free for unlimited use, but after all you are running arbitrary code on some else's server and most companies aren't infinitely generous!