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.

[Jeremy Avigad]

Has anyone used Lean / Mathlib with Codespaces recently? This course repository worked in Codespaces last year, but no longer does: https://github.com/avigad/lamr. VS Code starts, but it does not fetch Lean. Moreover, Gitpod has been replaced by Ona, which seems to be something else entirely.

[Jeremy Avigad]

Strange, GlimpseOfLean started fine in Codespaces, though it looks like the same setup.

[Jeremy Avigad]

Also success with Formalization of Mathematics in Lean (@Bhavik Mehta). I'll investigate more tomorrow.

[Bhavik Mehta]

Did you get this error? #general > musl-based elan @ 💬 As I mention there, it's seemingly random whether it happens or not, so perhaps you could have gotten unlucky with lamr and lucky with GlimpseOfLean and my notes

[Jeremy Avigad]

Curiously, I got no error message at all. Codespace started, but when I opened a Lean file, nothing was syntax highlighted. But maybe I didn't wait long enough. I'll try again tomorrow.

[Bhavik Mehta]

I think that means Lean didn't start, and might be consistent with what I had; perhaps the output window contained the error message?

[Yaël Dillies]

Something we might want to try is rebuilding the community-maintained docker images

[Riccardo Brasca]

For me codespaces works much better with chrome than with firefox, I've never understood why.

[Jeremy Avigad]

Debugging this was a nightmare, because testing any change meant waiting 10 minutes to start up codespaces again, and I finally decided there is a random element to whether or not the Lean extension installs. Some things that may or may not make a difference:

• I updated the image from jammy to noble in the Dockerfile.
• Adding && lake build here seemed to make the installation hang (even though lake build only takes a few seconds on this repository). Doing it as a postAttachCommand seemed to be less problematic, but I couldn't tell whether it was having an effect on installing the extension.

Ultimately, I added instructions to the README to install the Lean 4 extension and call lake build manually.

[Shreyas Srinivas]

This is not surprising. I don’t think codespaces ever worked for me on mathlib. I have always had to install the lean extension, get permission errors while the extension tries to install the toolchain, and then run the installation command in the shell, with some chmod stuff.

[Shreyas Srinivas]

This is unlike gitpod where mathlib opens and you can already see the cache being fetched

[Eric Wieser]

Gitpod sometimes failed to install the extension (or rather, any extensions at all) too, and conversely, I've not seen the behavior on codespaces.

[Eric Wieser]

So I think things are just flaky in general

[Joscha Mennicken]

I'm currently trying to understand why codespaces sometimes fails. If anyone has a broken codespace and some time to help me experiment, please let me know. (Bhavik Mehta and I have already done a bit of experimenting, and I have some suspicions, but so far I have not yet been able to create a broken codespace myself.)

[Joscha Mennicken]

My current hypothesis is that opening a codespace on a PR/branch that's using the same toolchain as mathlib master should succeed while opening a codespace with mismatching toolchains will usually fail. I'll continue to investigate tomorrow.

[Joscha Mennicken]

The result of the investigation: #34615

@Jeremy Avigad Trying out the codespaces setup in https://github.com/avigad/lamr, it seems to run into the same problem as described in the PR. Copying over the .devcontainer/ directory from my PR into your repo unchanged resulted in a working codespace for me (test it yourself in my fork).

[Joscha Mennicken]

Jeremy Avigad said:

Strange, GlimpseOfLean started fine in Codespaces, though it looks like the same setup.

It does not use the same setup. Instead it uses a setup very similar to my PR. My PR mainly resurrects what Mathlib did a while ago, before it switched to the gitpod prebuilt docker image, so presumably GlimpseOfLean just copied mathlib's setup at a different point in time.

[Joscha Mennicken]

Oh, by the way, you don't need to copy any of .docker/ into your own projects, just .devcontainer/, even if you're using the current mathlib setup, since it uses mathlib's pre-built gitpod image and doesn't build it itself.