Collaborative editing#

Remote repositories#

Git is a distributed VCS: several copies of the same repository may exist and exchange with one another.

Multiple instances of a project may exist:

locally on a machine
over a network, communicating through various protocols (ssh, git, https)

From the perspective of a given repository, other repositories of the same project are called remotes.

Note

Once remotes are set up, the workflow is identical whether the repository copies are on the same hard-disk or on a different machine.

Typically, one keeps a repository as an “official” source for the project. This official repository must be a bare one: there are no checked out files in it.

Example:

two repositories cloned from project
project_1 is a remote of project_2, named extra
all repositories are “local”, i.e. on the same disk

Clean up

cd ../
rm -rf project

Initialize a bare “official” repository in the project folder and clone two copies

git init --bare project
git clone project project_1
git clone project project_2

Initialized empty Git repository in /home/coslo/teaching/tools/docs/project/

Add project_1 as a remote of project_2

cd project_2
git remote add extra ../project_1

The syntax is

git remote add <remote_name> <remote_path>

where:

<remote_name> is a name for the remote
<remote_path> is the path to the remote (can be over the network, see below)

Have a look at the remote repositories we have access to

git remote -v

extra       ../project_1 (fetch)
extra       ../project_1 (push)
origin      /home/coslo/teaching/tools/docs/project (fetch)
origin      /home/coslo/teaching/tools/docs/project (push)

By default, the origin remote is the one we cloned the project from.

We can now check out any branch of the project_1 remote repository, inspect or grab files from them, merge them into our own branches.

Example: the master branch of project_1 contains some interesting new commits and we want to merge them in our code:

git fetch extra
git checkout extra/master
# ... look at code here
git checkout master
git merge extra/master
# To keep a flat commit history use instead
# git rebase extra/master

Remember to add some commits first in the extra remote!

Remote collaboration#

To collaborate remotely, users must have access to a git server. A git server may boil down to a simple ssh server, to which you and your collaborators have access to, or using a proper git server (with git protocol).

The power of git allows you to deal with multiple remote repositories on different servers. Say Alice and Bob both cloned a project from a server. They can push this project to their respective git servers (github and gitlab).

Then, Alice adds Bob’s repository, which is stored on github, as remote…

# On Alice PC
git remote add bob https://github.com:bob/project.git

…and viceversa!

# On Bob PC
git remote add alice https://gitlab.com:alice/project.git

Pushing and pulling each others’ project can then be done with the same commands seen above for local remotes. For instance, on Alice pc

git pull --rebase bob master # fetch and rebase remote master into local master

Github, gitlab and all that#

git is a decentralized VCS: no central server, every repository can share with any other.

However, git servers have undergone a coarsening process and a few big centralized servers (“silos”) have emerged.

Along this process, web applications grew around git servers, adding functionalities that allow users to browse repositories and collaborate on software:

github: centralized, closed source, owned by Microsoft (https://github.com/explore)
gitlab: centralized, open-source edition (https://gitlab.com/explore/projects/trending)
self-hosted instances of gitlab: ex. framagit (https://framagit.org/)
gittea (https://gitea.io/en-us/), gogs (https://gogs.io/): self-hosted
codeberg (https://codeberg.org/): based on forgejo, which is itself a fork of gittea
ActivityPub for federation
…

Features:

issue tracking: report bugs or ask for new features
pull requests: facilitate merging of new features and bug fixes
continuous integration: automatic testing and deployment of code on multiple platforms
web page hosting: host static web pages (ex. documentation)
social networking: collaborate and discover new projects

Anti-features:

social networking (!)
walled gardens
over-engineered

Creating an account#

Both gitlab and github have free plans for private and public repositories. Here I create an account on gitlab https://gitlab.com/users/sign_up (no need to give your actual identity)

Setting up ssh keys#

If you do not have them yet, create a pair of private-public ssh keys. This will encrypt your communications to the remote server using the git protocol

ssh-keygen
# Press Enter three times... (or add a passphrase for security)

Your public key is

cat ~/.ssh/id_rsa.pub

ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQDnnpooSARIJ6HYdy/QWrtv0C1XANNKWUIDei3BxCXy9f62hzAQMtJuVAr/
wu0WfNnygcP1w+D/LOScdrRrzw5hCHainVcVQustw8OtkyW19ITboMD5KC9P2pdSPtsdaUNF8ZK0+fDfYwFpRfeF0+qsebQs
OWaLF03x+o69ZnJf1Gs6PGER2aETBVz9UUniveMf0CqHGmUK5l5Yj9Otzs4uAAYEyvGPt5amtRWMGufQIB5edrOqa/+Mu8gI
xu6uHUtLsEs9AzDslM/McWDVoDAumnBgJsLGJpD3/0DsD4dToH6NtRsNLhy8NmRotsJwL+KSIrT9zpVfk67 coslo@local

Your private key is

cat ~/.ssh/id_rsa

Danger

Never ever share your private key!

In the SSH Keys settings on the web interface (top right corner, then Preferences), add a new key by pasting the content of ~/.ssh/id_rsa.pub

Note

It is also possible to have or grant access to a remote repository with tokens (both for gitlab and github)

Creating a new project#

You can create a new git project directly from the command line (it will be private by default).

The default remote is called origin. Add the gitlab server as the new origin remote, then push the master branch over there

git remote add origin git@your_server:your_username/docs.git
git push -u origin master

Warning

Remember to change the dummy names (“your_server”, “your_username”) above with yours!

If you have them, push all existing branches (and tags)

git push -u origin --all
git push -u origin --tags

Differences between pull, merge and rebase#

First, note that

git pull origin master

is equivalent to

git fetch origin
git merge origin/master

Unless the merges resolves in a fast-forward, git will keep track of the branching path in the commit history. To always flatten commit history, make a rebase instead

git pull --rebase origin master

or equivalently

git fetch origin
git rebase origin/master

Exercise 1: create an account on a git platform#

choose a web platform of your choice
create an account on it
create your ssh keys and add the public one in your account
push your docs repository over there
browse your project online
commit, commit, commit… then push the changes to the server again

To upload existing files from your computer, use the instructions below. Remember to replace dummy paths with relevant ones.

Push an existing Git repository

This is the most common use case.

cd existing_repo
git remote rename origin old-origin
git remote add origin git@your_server:your_username/docs.git
git push -u origin --all  # -u sets origin as upstream server of every branch
git push -u origin --tags  # if you have tags

Push an existing folder

If existing_folder contains a repository but you want to start a brand new one, just delete the .git folder at its root

cd existing_folder
git init --initial-branch=main
git remote add origin git@your_server:your_username/docs.git
git add .
git commit -m "Initial commit"
git push -u origin main

Create a brand new repository

This assumes you create an empty repository on the remote server

git clone git@your_server:your_username/docs.git
cd docs
git switch -c main
touch README.md
git add README.md
git commit -m "add README"
git push -u origin main

Exercise 2: collaborative editing of a document#

who plays Alice? who plays Bob?
clone the template-docs repository from framagit
set the origin of the repository to point to a new project on your remote server
push the repository to your remote server
edit the Authors section in docs/index.rst and commit the change
push the changes to your remote server
make sure your projects are public (or give each other access to them via tokens)
add a new remote pointing to your collaborator’s project on his/her remote server
pull his/her commit into your own master branch

Bonus:

handle conflicts if both of you modify the same parts of docs/index.rst!