Lean4 on google colab

Stream: new members

[Baran Zadeoglu]

Is it possible to run Lean4 on google colab? I tried googleing a bit but nothing came out of it.

[Eric Wieser]

Making this a pleasant experience would amount to embedding a full lean editor inside a single google colab cell

[Eric Wieser]

Of course, the other end of the spectrum is "yes, use subprocess.run(["lean", "some_lean_file.lean"])

[Baran Zadeoglu]

I see. Not quite what I hoped for. Perhaps I should reformulate. I am hoping for a way to share lean code online in "blocks". Something like an online Jupyter notebook was the first thing that came to my mind. But as far as I understand, Jupyter notebooks don't work for lean to begin with.

[Christian K]

You might already know this, but there is a lean4 webeditor which stores the code in the url, so you can share code like this

[Baran Zadeoglu]

Thank you! It may work. I will keep this question open for now in case someone else has a better idea.

[Christian K]

What's your concern with the webeditor/what features are you missing?

[Baran Zadeoglu]

we would need to recommunicate links after each itteration. Plus I was hoping to collapse the blocks of code. I had in mind hundreds of small examples where someone can hopefully browse through with some relative ease.

[Christian K]

Baran Zadeoglu said:

we would need to recommunicate links after each itteration.

Yeah, i had this problem too. I built a modified version of the webeditor which clones a copy of the github repo to the language server which also allows importing from your own files. The links are also static (They store the file path, not the code). But this version isn't currently running on a public server but it could be released after some cleanup

[Baran Zadeoglu]

I would be happy to use it if you were to release it. I am not literate enough to help you clean it up I am afraid.

[Christian K]

No problem, it would be amazing though to find some community members to help developing this, especially in regards to safety.

[Eric Wieser]

I think you might be interested in Verso, which lets you do 'literate programming', and compiles to interactive (but non-editable) html for sharing.

[Eric Wieser]

I think at one point @Julian Berman built a Jupyter kernel for Lean, but it might have been an old version?

[Jon Eugster]

Christian K said:

Baran Zadeoglu said:

we would need to recommunicate links after each itteration.

Yeah, i had this problem too. I built a modified version of the webeditor which clones a copy of the github repo to the language server which also allows importing from your own files. The links are also static (They store the file path, not the code). But this version isn't currently running on a public server but it could be released after some cleanup

You could also see what you could integrate back into the webeditor, and create PRs! I think it would be quite cool to add more functionality alongside the option to store the code in the URL (which was primarily inteded for short code snipets from Zulip).

Of course then one needs to think about garbage collection, safety, and also a few other things...

Christian K said:

No problem, it would be amazing though to find some community members to help developing this, especially in regards to safety.

I don't intent to spent lots of time on developing anything around the web editor, but I generally have a bit of time allocated for maintaining that code (i.e. don't hesitate to DM me:blush:)

[Christian K]

Nice, but I'm not really sure if this would really make sense on the public lean4 web severs. The workflow is, that the server has a local copy of the github repo. On the website, the user has a filepicker to select a file (or just inputs a url with the path directly). The user can then view the code of the file, but the changes are only committed to the github repo if the user is logged in. The question is if it would be more viable to have this tool avaible so big projects could host it themselves for their project or if the lean4 web servers should have the ability to clone github repos etc.