cache on project with gitpod

Stream: Lean for teaching

[Damiano Testa]

Dear All,

I am teaching a course on formalisation and I created a project depending on mathlib. To allow lake exe cache get to work on gitpod, I very simply copied the files

.gitpod.yml
.docker/gitpod/Dockerfile

to my project and opened it in gitpod. Gitpod took a couple of minutes to set everything up. While it was setting up, I had the impression that several instructions were not actually working, but eventually, I could import Mathlib and it worked well.

Is this normal? Should I do something else? I am mostly concerned by the fact that this will be potentially used by all my students and I am wary of the fact that some of them might have problems and I will not be able to help them at all!

Note: it is the first time that I use gitpod, so if something looks wrong to you, it probably is!

[Adam Topaz]

@Damiano Testa you could alternatively use GitHub codespaces. Just copy the devcontainer folder from mathlib4 and it should work out of the box.

[Adam Topaz]

I don’t know about git pod, but with codespaces it does take a little while to set up, but everything should be automatic

[Damiano Testa]

Do you know what is the difference between codespaces and gitpod? Or why should I prefer one over the other?

[Adam Topaz]

Personally I prefer github codespaces because it's part of my github account. I don't have to worry about setting up anything separately with gitpod. But overall I think the two are quite similar.

[Patrick Massot]

You can copy the gitpod stuff from #mil

[Matthew Ballard]

• Codespaces has unlimited access for classes but the specs on the container are pretty low
• Gitpod has better default specs but is capped for free use

People generally get used to one and stay with it.

[Kevin Buzzard]

I set up both at https://github.com/kbuzzard/IISc-experiments and documented in the README what needed to be done to do this.

[Damiano Testa]

Great, thank you all very much! It seems that .gitpod.yml and .docker/gitpod/Dockerfile are some of those files that were never created but always copied along -- I hope that my students will not be the ones to cut this unbroken chain.

[Eric Wieser]

I think the slow gitpod setup time goes away if lots of people are opening the same repo; I see it on my own projects, but never on mathlib.