Zulip Chat Archive

Stream: Lean for teaching

Topic: cache on project with gitpod

Damiano Testa (Oct 02 2023 at 23:08):

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


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 (Oct 03 2023 at 00:25):

@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 (Oct 03 2023 at 00:26):

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 (Oct 03 2023 at 00:30):

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

Adam Topaz (Oct 03 2023 at 01:44):

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 (Oct 03 2023 at 01:48):

You can copy the gitpod stuff from #mil

Matthew Ballard (Oct 03 2023 at 01:49):

  • 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 (Oct 03 2023 at 05:14):

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 (Oct 03 2023 at 06:13):

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 (Oct 03 2023 at 08:49):

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.

Last updated: Dec 20 2023 at 11:08 UTC