tutorials on web?

Stream: new members

[Sam van G]

Hi! I was wondering if the “tutorials” project is available to play on the web, too, for people who have not (yet) installed Lean?
(Apologies if this has been asked before, I found a mention online from 2020 that it wasn’t.)

[Henrik Böving]

https://github.com/leanprover-community/tutorials/ this one?

[Sam van G]

Yes, exactly. Is there a version that is playable in the browser, like the Natural Numbers Game?

[Alex J. Best]

I don't think there is such a version, it might be possible to load this project in gitpod (like https://gitpod.io/#https://github.com/ImperialCollegeLondon/formalising-mathematics-2022) but the user experience of using Lean and a supported editor on your own machine is much better than the natural number game so I'd really recommend installing if possible.

[Sam van G]

Thanks @Alex J. Best, doesn't quite work out of the box, but I guess one could make it work by putting the right gitpod configuration in the tutorials repo.
But already good to have the gitpod link to formalising-mathematics-2022, that is close enough to what I was looking for.
Completely agree that it is better to install - I was asking it so I could show some Lean "in action" to people who might not immediately want to install Lean on their own machine.

[Alex J. Best]

Yes indeed, I'd be in favour of merging a PR to the tutorials project to add the gitpod config used for the formalizing maths repo (https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/master/.gitpod.yml).
Actually this looks like its already almost done at https://github.com/leanprover-community/tutorials/pull/42

[Alex J. Best]

@Johan Commelin want to copy paste the gitpod.yml file from my previous message into that PR (I don't have push access)

[Sam van G]

Makes sense, thanks Alex!

[Johan Commelin]

@Alex J. Best @Sam van G gedaan

[Patrick Massot]

I'm traveling today but I can setup this later this week if someone reminds me to do it.

[Sam van G]

Very cool. For the record, it works for me now at https://gitpod.io/#https://github.com/leanprover-community/tutorials/tree/gitpod
@Patrick Massot @Johan Commelin
(And once the PR is merged into the main branch it should work without the /tree/gitpod in the link.)