setting up Gitpod

Stream: mathlib4

[Floris van Doorn]

I am giving a Lean tutorial at the Logic Colloquium this week, and I was planning to use Gitpod.
However, I realized that setting up Gitpod if you don't have a Github account yet is quite a hassle. I just tried it, and it requires both email and phone number validation, but it is quite confusing, and takes quite a few steps (it even routes you through some of the same pages twice - once before phone number validation and once afterwards).
I will also try Github codespaces, maybe that is a bit easier.

In any case, I would to have an alternative for people that prefer to install it locally. How hard would it be to make a Lean 4 bundle with VSCode(/VSCodium)+Lean4+my project (with the right mathlib4 dependency + oleans)? Something like the trylean bundles that we offer for Lean 3 on the website. I think that is a great way to quickly let people get Lean and work on a single project. Is that harder to do in Lean 4, or can I just adapt the script for Lean 3?

[Floris van Doorn]

I just tested Github Codespaces, and it is much friendlier to set up for people that still need to create an account with Github. You need to verify your email address, and are asked a few questions, but it's quite smooth.
An easy local installation would still be nice, but it's less urgent given how easy it is to set up Codespaces.

[Eric Wieser]

What extra steps did gitpod add? I though the setup was the same...

[Floris van Doorn]

When I tested it on a freshly created account, it required a phone number verification near the end of the process - and after this verification step you were sent back to the start of the process, and you had to re-answer "how did you learn about gitpod" and "how big is your organization" and things like that.

[Eric Wieser]

Weird. Maybe they've changed their sign-up flow since I signed up

[Kevin Buzzard]

You've had a github account for ages and might have told GitHub your phone number ages ago too

[Eric Wieser]

My reading was that Floris was saying that you had to give Gitpod a phone number too

[Floris van Doorn]

It was probably Github asking for a phone number, because Gitpod requested that information from Github via the app authorization.

[Sebastian Ullrich]

Floris van Doorn said:

How hard would it be to make a Lean 4 bundle with VSCode(/VSCodium)+Lean4+my project (with the right mathlib4 dependency + oleans)?

It should work pretty much the same I think

[Anand Rao Tadipatri]

@Floris van Doorn If you are planning to work on a single file in each session and don't have any imports, you can try the "Load from URL" option on the Lean4 Web Editor. I found this very convenient for a few talks that I gave recently since I was using only standalone files for the demonstrations.

[Floris van Doorn]

I did the (first part of my) tutorial, and it worked very well using Github Codespaces. I can definitely recommend codespaces for tutorials. It's easy to set up (a little harder if you don't have a Github account yet, but still very doable), and worked for 95+% of participants.

The tutorial I'm using is here: https://github.com/fpvandoorn/LogicColloquiumTutorial/ (or abbreviated as https://tinyurl.com/LeanTutorial ), and the careful observer will note it's just an adaptation of @Patrick Massot's Glimpse of Lean

[Eric Wieser]

Note that if you run the tutorial through GitHub classrooms, then the "students" get unlimited codespaces quota

[Eric Wieser]

I think you might get close to the hours cap for a week long tutorial otherwise

[Floris van Doorn]

Yeah, for a week long tutorial you're right. My tutorial is only 2x1.5 hours.