Creating a common project

Stream: lean4

[Esteban Martínez Vañó]

Hi everyone.

Is it possible to have a common project on several computers?

I want to work with a couple of collegues in the same project, so we would like to have a common project uploaded to Github in such a way that:

• When someone wants to work on it, should be able to upload the project in its computer without having to clone the whole project again every time some other person makes a change.
• Any change, by any member of the team can be uploaded to the same Github repository (from different computers, of course)

Can this be done in some way?

Thanks in advance.

[Henrik Böving]

Isn't what you are describing exactly what git gets you?

[Edward van de Meent]

you can add collaborators/contributors to a github project, if that's what you mean...

[Esteban Martínez Vañó]

But, if someone else changes something in the project, how can I recover the changes with git in my own computer?

[Henrik Böving]

git pull

[Edward van de Meent]

they create commits locally, git push them to the repo, you checkout the branch, and git pull them to your local version.

[Henrik Böving]

If you're not so familiar with git maybe a git GUI client like Github Desktop might be sensible. If you want to stick to the git CLI I'd suggest you read some git tutorials, this is not a problem unique to Lean and has been solved many years ago.

[Esteban Martínez Vañó]

Okay, I'll look for it then and, if I have some specific doubt, I'll come back here. Thanks!