Access to gitpod or codespaces

Stream: general

[Patrick Massot]

Can anyone update me on what is currently required to use either GitPod of CodeSpaces? I thought one of them allowed to avoid creating a GitHub account but I just tried and it seems they both want a GitHub account. Am I missing something?

[Yaël Dillies]

gitpod requires some account between github, gitlab and bitbucket

[Patrick Massot]

I saw only github

[Patrick Massot]

@Floris van Doorn I think you tried this recently?

[Yaël Dillies]

I see this when trying to connect

[Patrick Massot]

Very weird. I just tried on the computer of a colleague and saw only GitHub.

[Patrick Massot]

And then it asks a lot of annoying questions.

[Patrick Massot]

I think I will try using CodeSpaces today (I’m giving a GlimpseOfLean session).

[Floris van Doorn]

Both require a Github account. In my experience Gitpod also asks you (or maybe only new Github users) to verify their phone numbers.
Here are the instructions I've written for using either: (bottom of the README)
https://github.com/fpvandoorn/LeanCourse24?tab=readme-ov-file#temporary-ways-to-use-lean

[Patrick Massot]

I ended up using CodeSpaces to avoid having phone calls (indeed I tried with a colleague this morning and he had to get a phone call with a code to type). CodeSpaces was a nightmare. It was very slow and unreliable.

[Patrick Massot]

It would be really nice to have a usable alternative to all this.

[Floris van Doorn]

Oh, that surprises me. In my experience it was quite good. But that was more than a year ago.