PRs to FLT without local install

Stream: FLT

[Kevin Buzzard]

I never use gitpod or codespaces because I always develop FLT using a local clone of the project. As part of the docs for FLT I was thinking of saying "look how easy it is to play with the project, just go to this website" . But can I say "if you have a github account then look how easy it is to remove a sorry and make a PR whilst using this website and with no local installation of Lean"?

[Riccardo Brasca]

VS Code in gitpod has the github pull request extension installed, so creating a PR should be very easy.

[Riccardo Brasca]

I've created https://github.com/ImperialCollegeLondon/FLT/pull/49 via gitpod, it was indeed quite easy.

[Riccardo Brasca]

Note that opening the project in gitpod does not run lake build, so all files have the red bar. With the repo getting bigger and bigger I don't know what is best, but maybe hosting a cache somewhere is possible.

[Yaël Dillies]

Yes, I've set up cache in CI for some of my projects in the past, if you need some help

[Damiano Testa]

I also have such a gitpod setup in the repository for my module: I ran all my lectures via gitpod and it worked very easily.

[Damiano Testa]

This is the file, but I basically copied it from Mathlib and probably changed a couple of characters:

https://github.com/adomani/MA4N1_2023/blob/master/.docker%2Fgitpod%2FDockerfile

[Kevin Buzzard]

@Yaël Dillies please feel free to PR!

[Yaël Dillies]

Will do when I get time between two revision sessions!