Alternative ways to use Lean4 outside of VSCode?

Stream: lean4

[Phillip]

I am currently new to Lean, and am playing around in Lean4. I am yet to understand, but playing around is fun. Currently, I have Lean on my home PC, and I use VS Code. I pulled the nightly release, and all has been well (since I am yet to do anything beyond proving true != false haha).

I wondered if there is any other way I can use lean, other than in VS Code. I am a uni student and spend a lot of time on my iPad, and I would enjoy having some way to access a Lean environment. I don't suppose there are any notebook tools or anything?

I have heard of Code-Server, and use it on and off; however, it doesn't have the lean4 extensions, so it doesn't work (afaik). Any suggestion on alternate ways I can continue to play around while not on my main PC? Thanks!

[Matthew Ballard]

If you can find the vsix, you can install the extension directly on code-server similar to vs code. (There is some hesitancy about whether the terms of use of the vs code extension library prohibit downloading vsix files for use in non-vs code editors or just to keep non-vs code editors from using the vs code extension library as a back-end.)

Another option is GitPod. I believe there are people with Lean4 GitPod experience around here: eg https://github.com/IPDSnelting/tba-2021/blob/master/.gitpod.yml The PWA experience with GitPod is not great YMMV.

[Mac]

@Matthew Ballard Both the lean and lean4 extensions are available through Open VSX, which is specifically designed not to have the licensing concerns you mentioned.

[Matthew Ballard]

Thanks. Last I checked. This wasn’t the case.