adding codespaces link to main mathlib4 website

Stream: general

[Alex Kontorovich]

I'm supposed to run a PEP ("professional enhancement program") at the upcoming JMM ("joint math meetings") on getting mathematicians new to formalization to use Lean/Mathlib, and had planned to have the participants start by clicking the "Open in Gitpod" link on the main site. @Heather Macbeth alerted me that Gitpod may be going away soon as a free/easy resource, and that codespaces is the new site we should use. (E.g., I see that in @Patrick Massot's Glimpse of Lean site, there are links to both a codespaces page and gitpod page.) Might it be possible to please add a Codespaces link to the main mathlib4 page? (Hopefully this isn't a big ask?) Thank you!

[Patrick Massot]

Please be aware that creating a Codespaces account is really annoying. It requires answering a lot of really irrelevant annoying questions.

[Patrick Massot]

What do you intend to do exactly?

[Rob Lewis]

This is built into the GitHub interface:
image.png

[Alex Kontorovich]

Patrick Massot said:

Please be aware that creating a Codespaces account is really annoying. It requires answering a lot of really irrelevant annoying questions.

Really? I clicked the one on your site, and it opened just as easily as gitpod does...?

[Rob Lewis]

Patrick Massot said:

Please be aware that creating a Codespaces account is really annoying. It requires answering a lot of really irrelevant annoying questions.

Does it? If you have a GitHub account it should be a single click, no?

[Rob Lewis]

This is built into the GitHub interface:

Oh, I see what you mean about adding it to the readme though!

[Alex Kontorovich]

Rob Lewis said:

This is built into the GitHub interface:
image.png

I'm trying to remove as much friction as possible from people who don't know what github is to start using Lean.

[Alex Kontorovich]

Rob Lewis said:

This is built into the GitHub interface:

Oh, I see what you mean about adding it to the readme though!

Yes exactly!

[Alex Kontorovich]

This is the link it takes me to when I click "Create codespace on master": https://expert-space-adventure-5r5jxggg9gv2vx4x.github.dev/ Is that the one everyone should be taken to, or is that generated by some procedure?

[Alex Kontorovich]

(If that's all it is, even an idiot like me should be able to PR the change to ReadMe...)

[Patrick Massot]

Sorry, I mixed them up. I just checked at #general > Access to gitpod or codespaces and it’s GitPod that is a nightmare to setup.

[Patrick Massot]

Creating a GitHub account is also not fun, and some people are bound to complain, but it’s the best we have.

[Patrick Massot]

Unless what you want to do is doable on https://live.lean-lang.org/

[Alex Kontorovich]

For "Glimpse of Lean", you have a nice looking site name: https://github.com/codespaces/new/PatrickMassot/GlimpseOfLean -- is it easy to implement the same for Mathlib master?

[Patrick Massot]

https://github.com/codespaces/new/leanprover-community/mathlib4 should work.

[Alex Kontorovich]

Patrick Massot said:

Creating a GitHub account is also not fun, and some people are bound to complain, but it’s the best we have.

I'm going to ask the participants to arrive having created a github account. If that's too hard for them, then they're probably a lost cause...

[Patrick Massot]

The question is not whether it’s too hard. The question is whether people will want to answer questions about their private life to Microsoft.

[Rob Lewis]

#19927

[Rob Lewis]

Unfortunately the badge size doesn't match the others

[Alex Kontorovich]

I'm not so keen on the badge, but rather on the "Installation" section, where there's a big standalone button to "Open in Gitpod"...?

[Niels Voss]

I thought only the cloud version of GitPod was going away? My understanding is that you can still self-host it if you want. I'm sure there are also alternatives. That being said, I can still think of several reasons why you might not want to self-host it (the most obvious being added complexity for whoever maintains it)

[Alex Kontorovich]

Question: with gitpod, it saves previous workspaces (https://gitpod.io/workspaces) and I can pick up where I previously left off. It seems that if I start a codespace and leave, it's all lost, and when I click the link again (now on the main site, thanks!), it generates a brand new codespace -- is that right? Or is there a way to return to previous codespace work? Thanks!
Nevermind, found it!

[Alex Kontorovich]

PS: Given that codespaces run on github itself, is there a way to turn on the (github) Copilot functionality in the web app? (The way the copilot extension runs seamlessly in VS Code?) Thanks!