Getting Lean set up on Gitpod

Stream: general

[Arnav Sabharwal]

What's the procedure for getting Lean 4 set up on Gitpod? I tried following the procedure here and opening the workspace with the changes but it can't seem to recognize Lake. I may be doing something stupid, so some assistance would really help, thanks!

[Damiano Testa]

Mathlib already has a gitpod setup (in .docker/gitpod) and I used that to setup my project. Does that work for you?

[Arnav Sabharwal]

Ah, I see. I used that Dockerfile and ensured that gitpod.yml could see the Dockerfile. However, it now seems that docker itself can't be found (because I guess I changed from the default Dockerfile). Did you have to reinstall Docker when you performed your setup?

[Eric Wieser]

I don't think Damiano has the power to reinstall docker on gitpod :)

[Damiano Testa]

I thought that I had copied the Dockerfile and made some trivial modifications, but, looking at it, I think that the modifications were not just trivial, but actually non-existent.

This is what I use -- the link is to the repository for my course and my lectures happened entirely on gitpod, since I could not install Lean on the departmental computers.

[Arnav Sabharwal]

Hmmm, If you don't mind me confirming, all that needs to be done is point gitpod.yml to the Dockerfile, reopen the workspace (hopefully everything should take care of itself), and then follow the normal procedure towards creating the Lean project, right? Currently, the workspace doesn't build my changes when I reopen the workspace, so lake and elan cannot be found. However, these can be found when I run gp validate, except that now, docker cannot be found.

Additionally, Gitpod doesn't like me creating a Lean project within an existing Gitpod project, and the Lean Infoviewer seems to be completely blank when opened in the debugger workspace, complaining that the Gitpod project I have opened is not a valid Lean project. This occurs after I create a new Lean project within the Gitpod project, run gp validate, and then open a Lean file.

I haven't used Docker before and want to make sure I'm not doing anything stupid, so apologies if these questions seem too rudimentary! Thanks!

[Julian Berman]

Just to be sure, you have some new project you created right? You're not just trying to use Mathlib and/or Lean in Gitpod?

[Arnav Sabharwal]

I was trying to do the latter, but I suppose then that's not what I'm supposed to be doing? Alternatively, is this the right way to go about it:

1. create lean project locally
2. host it on github (although I can't seem to find instructions for this)
3. open the workspace in gitpod, add the dockerfile
4. build the workspace, and ideally everything should work?

[Julian Berman]

Good that's why I asked. If you want to do the latter that should take 13 seconds :) just go to https://gitpod.io/new#https://github.com/leanprover-community/mathlib4 and click new workspace, you shouldn't have to do any of this!