Git for mathematicians

Contents

Si vous avez déjà lu une partie de cette page et cherchez simplement un rappel, vous pouvez consulter l'aide-mémoire.

Pourquoi git ?

Git est un logiciel de gestion de versions, il sert à enregistrer de façon structurée l'évolution d'un ensemble de fichiers et à synchroniser le travail entre plusieurs machines, éventuellement appartenant à des utilisateurs différents. À la différence de Dropbox, ou de son équivalent Seafile proposé par Mathrice, ou de services du type « Time machine », git n'enregistre ni ne synchronise pas de façon automatique l'évolution des fichiers. En effet le but est d'avoir un historique comportant une suite de modifications cohérentes et commentées par leur auteur.

Les bases

Installation et configuration initiale

Cette section décrit les opérations à réaliser une seule fois par ordinateur utilisant git. On peut les oublier ensuite.

Sous Linux, git est empaqueté par toute les distributions. Par exemple sur Debian et ses dérivées (comme Ubuntu), on tapera « sudo apt-get install git ».

Sous Windows ou Mac, on se rapportera à la page téléchargements

Avant la première utilisation on dit à git de quelle façon nous identifier dans l'historique du dépôt :

git config --global user.name "John Doe"
git config --global user.email "johndoe@example.com"

puis on lui dit quel éditeur utiliser pour les messages décrivant chaque modification (on peut remplacer vim par emacs, nano, etc.):

git config --global core.editor vim

Les utilisateurs de MacOS qui n'utilisent pas d'éditeur puissant peuvent demander textedit en tapant plutôt:

git config --global core.editor "open -W -n"

Sous MacOS, il faut bien prendre garde à vraiment quitter l'éditeur après avoir écrit et enregistré le message décrivant la modification, et ne pas se contenter de cacher l'éditeur sans rendre la main à git.

Enfin il est commode de taper la commande suivante, sans chercher à la comprendre pour l'instant.

git config --global push.default current

Utilisation sur une seule machine

On peut utiliser git seul, sur une seule machine, sans connexion internet. Pour transformer un répertoire en dépôt git, il suffit de taper la commande git init. Par exemple :

cd /tmp
mkdir monProjet
cd monProjet
git init

créé un répertoire monProjet et y initialise un dépôt git (vide pour l'instant). Il ne faut pas hésiter à vraiment taper ces commandes pour pouvoir essayer toutes les autres commandes décrites ci-dessous.

Les trois zones

Git divise l'univers en trois parties : la copie de travail, la zone d'index et le dépôt.

La copie de travail est l'ensemble des fichiers présents dans répertoire contenant le dépôt et ses sous-répertoires. Ces répertoires peuvent mélanger des fichiers suivis par git et des fichiers ignorés par git. Par exemple il n'est pas souhaitable que les fichiers .aux, .log et .pdf crées par LaTeX soient suivis par git.

Le dépôt est la base de données contenant toutes les versions successives des fichiers suivis et les métadonnées accompagnant chaque modification (date, auteur, commentaires...).

La zone d'index est une zone intermédiaire entre les deux précédentes, elle peut être essentiellement ignorée dans le cadre d'une utilisation basique, sauf lorsqu'on veut demander à git de suivre un nouveau fichier. La commande git add nomFichier demande à git de placer le fichier nomFichier dans la zone d'index. La commande git commit envoie tous les fichiers présents en zone d'index vers la base de données. Dans l'exemple ci-dessus, on peut créer un fichier exos.tex dans le répertoire monProjet puis taper

git add exos.tex
git commit

La commande git commit commence par ouvrir un éditeur invitant à taper une description des modifications. Cette description peut être très brève ou au contraire contenir des explications sur les motivations de l'auteur.

On peut voir le résultat de ces commandes en tapant git log qui affiche l'histoire du dépôt.

Après modification du fichier exos.tex on peut soit retaper les deux commandes add et commit ci-dessus soit utiliser le raccourci git commit -a qui envoie en tous les fichiers suivis dans la zone d'index puis immédiatement dans la base de données.

Utilisation d'un dépôt Mathrice

Afin d'avoir une sauvegarde en lieu sûr, pour collaborer ou tout simplement pour travailler depuis plusieurs ordinateurs, il est utile d'avoir une copie du dépôt sur un serveur. Le portail des maths de l'INSMI offre ce service via le logiciel web gitlab qui permet aussi de visualiser en ligne les modifications, de discuter des projets, d'avoir un wiki, de compiler du TeX sur le serveur et le mettre à dispositation, et bien d'autres choses.

Configuration initial pour Mathrice

L'utilisation du serveur git de Mathrice requiert quelques formalités à accomplir avant la première utilisation sur chaque ordinateur concerné.

La toute première étape est bien sûr d'avoir un compte Mathrice (appelé aussi compte PLM). Il suffit d'en faire la demande aux informaticiens du laboratoire, la création ne prend qu'une minute et ouvre accès à bien d'autres services.

L'utilisation du serveur git de Mathrice requiert une clef ssh, par exemple RSA. Dans les systèmes Unix (Linux ou MacOSX) les clefs ssh sont typiquement stockées dans un répertoire .ssh à la racine du répertoire utilisateur. Il est fortement recommandé de garder cet emplacement par défaut qui fait fonctionner de façon automatique les étapes suivantes. On peut générer une clef RSA par la commande ssh-keygen tapée dans un terminal. Cette commande crée une paire de fichiers id_rsa et id_rsa.pub, éventuellement protégés par un mot de passe (qui sera à taper une fois pas session). La clef publique id_rsa.pub est à déposer sur le site web plmlab. Il faut copier dans le grand champ de texte le contenu du fichier id_rsa.pub créé par ssh-keygen /Astuce :/ si le fait que le répertoire .ssh est caché pose problème, on peut provisoirement copier ce fichier dans un répertoire plus accessible. Puis il faut donner un nom à la clef (il ne sert qu'à aider l'utilisateur à différencier ses éventuelles multiples clefs) et cliquer sur « Add key ». L'expérience montre que, après dépôt de la clef, le serveur a parfois besoin de quelques minutes pour la prendre en compte, c'est le moment d'aller prendre un café.

Après ces formalités, on peut se rendre sur la page Projets pour voir la liste des projets accessibles ou pour en créer un nouveau. Vous pouvez aussi taper dans un terminal la commande git clone git@plmlab.math.cnrs.fr:dupont/nom_du_depot.git si le collègue Dupont a invité à utiliser son dépôt nom_du_depot. Par défaut cette commande créé un répertoire nom_du_depot dans le répertoire courant. Si ce nom ne convient pas, on peut taper plutôt git clone git@plmlab.math.cnrs.fr:dupont/nom_du_depot.git mon_meilleur_nom, le collègue Dupont n'en saura jamais rien.

Synchronisation avec le serveur

L'utilisation d'un dépôt git cloné depuis un serveur externe est identique à l'utilisation sur un seul ordinateur, avec ses commandes git add, git commit, etc. Le dépôt cloné contient toute l'histoire du dépôt et peut fonctionner de façon autonome, y compris en l'absence de connexion internet (TGV, eduroam capricieux...). La synchronisation avec le serveur se fait par les deux commandes git pull qui tire les commits du serveur vers le dépôt local et git push qui les pousse du dépôt local vers le serveur.

Utilisation plus avancée

Les conflits

Mise en place de dépôts de test

Les conflits se produisent lorsque deux utilisateurs travaillent en même temps sur le même dépôt ou, plus souvent, lorsqu'un utilisateur oublie de tirer par git pull avant de modifier des fichiers surveillés. Pour expérimenter cela, il est bon de créer un dépôt central et deux clones (sur un seul ordinateur) :

cd /tmp
git init --bare central
git clone central clone1
git clone central clone2

Les commandes ci-dessus crée un dépôt central qui ne contient par de copie de travail, il n'est destiné qu'à servir d'intermédiaire entre ses deux clones clone1 et clone2 (créés par les deux dernières commandes). C'est ce type de dépôt qu'héberge le serveur de Mathrice. Les dépôts clone1 et clone2 sont des dépôts ordinaires. Afin de simuler l'interaction de deux utilisateurs différent, on se rend dans le répertoire clone1 pour y taper git config user.name "Mon clone 1" puis dans clone2 pour y taper git config user.name "Mon clone 2". Ce changement d'identité (optionnel) n'aura d'effet que dans ces deux dépôts, il permet de distinguer deux auteurs fictifs lorsqu'on examine l'historique par git log.

Un conflit simple

On crée maintenant dans clone1 un fichier exos.tex contenant

exo1 : Montrer que $a + b = x$.

exo2 : Montrer que $a^2 + b^2 = c^2$.

puis on tape comme d'habitude

git add exos.tex
git commit
git push

On se rend alors dans le répertoire clone2 pour y taper git pull et constater l'apparition du fichier exos.tex attendu. On va maintenant se placer dans une situation de conflit simple en transformant le exos.tex se trouvant dans clone1 en :

exo1 : Montrer que $a + b = x$.

exo2 : Montrer que $a^2 - b^2 = c^2$.

et en validant par git commit -a et git push. Puis, on se rend dans le répertoire clone2 où l'on oublie de taper git pull avant de transformer notre fichier en :

exo1 : Montrer que $a + b = y$.

exo2 : Montrer que $a^2 + b^2 = c^2$.

Puis on tape git commit -a qui ne pose aucun problème, cette commande étant purement locale. Par contre git push déclenche un message d'erreur. Comme le suggère ce message, on tape alors git pull pour tirer les modification manquantes. Git se rend alors compte que les modifications manquantes en provenance de clone1 sont compatibles avec celles de clone2. Il propose alors la fusion des modifications, avec un message explicatif par défaut qu'on peut éditer ou non. Après validation de ce message, la situation redevient normale. En particulier le dépôt clone1 peut tirer ces modifications avant de continuer à travailler.

Un conflit complexe

Dans le conflit précédant, git a su réconcilier les deux versions automatiquement. Cela n'est évidemment pas possible si la même ligne est éditée des deux côtés ou bien si une des séries de modifications a tellement changé le fichier qu'il est impossible d'y incorporer de façon fiable les modifications de l'autre côté.

Modifions par exemple du côté clone1 en

exo1 : Montrer que $a + b = y$.

exo2 : Montrer que $0 = 1$.

validé par git commit -a et git push

et du côté clone2 en

exo1 : Montrer que $a + b = y$.

exo2 : Montrer que $1 = 1$.

validé par git commit -a. Là encore git push déclenche un message d'erreur. Mais git pull ne suffit pas à résoudre le conflit : il faut clairement une intervention humaine. Toujours du côté clone2, on édite le fichier exos.tex pour y trouver :

exo1 : Montrer que $a + b = x$.

<<<<<<< HEAD
exo2 : $1 = 1$.
=======
exo2 : Montrer que $0 = 1$.
>>>>>>> 0da67485ae2e473a07f1c0d7ed74601294c4cd0a

Les zones de conflits sont marquées par <<<<<<<, =======, >>>>>>> (les autres informations présentes sur ces lignes peuvent être ignorées ici). Malgré son aspect un peu effrayant ce fichier reste parfaitement normal, on peut l'éditer en effaçant une des versions et les marqueurs de conflits ou bien remplaçant le tout par une troisième version. On valide ensuite ce changement par git commit -a qui propose un message de commit signalant la fusion comme dans le conflit simple. Ici il est presque sûrement utile de signaler qu'il y a eu conflit et de motiver la façon dont il a été résolu. Après cela, le git push se passe normalement. L'historique montrera les deux séries de modifications et la fusion.

Les fichiers ignorés

La commande git status montre, entre autre, la liste des fichiers qui ne sont pas suivis par git. Certains de ces fichiers sont volontairement laissés de côté, en particulier tous les fichiers créés par TeX lors de la compilation, les répertoires .DS_Store de MacOS etc. On peut signaler cette situation à git en créant, à la racine du dépôt, un fichier nommé .gitignore et contenant par exemple les lignes suivantes :

*.pdf
*.aux
*.log
*.out
*.idx
*.synctex.gz
*.nav
*.snm
.DS_Store

Ainsi la commande git status ne parlera plus jamais de ces types de fichiers. De même la commande git add ignorera ces fichiers, sauf si on insiste en utilisant plutôt git add -f (f comme force), par exemple parce qu'un fichier pdf est destiné à être inclus directement par LaTeX.

Les alias git

Lorsqu'on utilise git de façon régulière, il est fastidieux de passer son temps à taper in extenso git commit -a etc. On peut définir des alias, par exemple en tapant :

git config --global alias.ca 'commit -a'

qui permet de taper ensuite git ca à la place de git commit -a.

Examiner l'historique

Comme expliqué ci-dessus, la commande git log montre l'historique des modifications. On peut limiter la liste aux modifications impactant les fichiers du répertoire courant et de ses sous-répertoires en tapant git log . (noter l'apparition d'un point à la fin de la ligne). On peut même limiter à un fichier spécifique avec git log nom_fichier.

Chaque commit porte un petit nom du genre « 6169c85e668180b5ba6e72865e35a2ed11f74223 ». Pour chaque utilisation de ce nom, on peut utiliser seulement les premiers caractères (au moins quatre) comme abbréviation, sous réserve qu'il y ait assez de caractères pour le distinguer de tous les autres commits du dépôt.

Par exemple pour montrer les différences entre l'état du dépôt après le commit 6169c85 et le commit 6e72865 on tape git diff 6169c85 6e72865.

La sortie cette commande n'est pas toujours très lisible, on peut essayer la variante git diff --word-diff 6169c85 6e72865. On peut aussi installer un logiciel d'édition de diff graphique comme meld et dire à git de l'utiliser en tapant git config --global diff.tool meld et en remplaçant git diff par git difftool dans la commande ci-dessus.

Revenir en arrière

La gestion de version permet bien sûr d'annuler l'effet d'une modification. En temps normal rien ne doit disparaître l'historique, surtout lorsqu'un dépôt est cloné à différents endroits par différents utilisateurs. L'annulation consiste donc à créer un nouveau commit, pas à réécrire l'histoire.

Supposons que git surveille un fichier exo.tex contenant :

exo1 : Montrer que $a + b = y$.

exo2 : Montrer que $1 = 1$.

On le modifie en

exo1 : Montrer que $a + b = y$.

exo2 : Montrer que $1 = 0$.

puis git commit -a et nouvelle modification en

exo1 : Montrer que $a + b = x$.

exo2 : Montrer que $1 = 0$.

et nouveau git commit -a. La commande git log montre quelque chose comme :

commit 0da67485ae2e473a07f1c0d7ed74601294c4cd0a
Author: Patrick Massot <patrick.massot@polytechnique.edu>
Date:   Mon Aug 22 17:57:35 2016 +0200

    Modif exo 1

commit f320af95cbe7fb2ae6269fb8ca7b2e6fdd0cabe9
Author: Patrick Massot <patrick.massot@polytechnique.edu>
Date:   Mon Aug 22 17:46:12 2016 +0200

    Modif exo 2

commit b60c4f65b4bf94b14f82c7e8b4b848ecf62c76a1
Author: Patrick Massot <patrick.massot@polytechnique.edu>
Date:   Mon Aug 22 17:42:41 2016 +0200

    Nouveau fichier exos.

Puis on réalise que la première modification, celle du commit f320af95 n'est pas si brillante. On veut l'annuler mais sans perdre la modification correcte de l'exo 1 par le commit 0da67485. Il suffit de taper git revert f320af95. Cette commande ouvre l'éditeur de message de commit avec un message par défaut qu'il est probablement utile de compléter par une explication motivant l'annulation. C'est tout, l'historique montre maintenant un nouveau commit qui annule f320af95. Bien sûr ce tour de magie n'est possible que parce que le commit conservé n'a pas modifié la même ligne que le commit annulé.

Mode panique

Il arrive parfois qu'un utilisateur de git, surtout débutant, fasse une fausse manœuvre et ne comprenne plus où en est git, même après avoir examiné ce que dit git status. En dernière extrémité, on peut utiliser la commande git reset --hard pour vider la zone d'index et ramener la copie de travail à l'état dans lequel elle était après le dernier commit enregistré dans le dépôt. Cette commande est dangereuse car elle efface toutes les modifications locales qui n'ont pas été envoyées dans le dépôt par un git commit. Par contre elle ne touche pas aux fichiers présents dans le répertoire mais non suivis par git.

Dans le cas d'un dépôt partagé, par exemple via le serveur de Mathrice, une méthode encore plus radicale consiste à effacer tout le répertoire et à retourner à la commande git clone de la section Mathrice. C'est encore plus dangereux car les fichiers non suivis sont bien sûrs effacés aussi, mais surtout parce que les modifications validées localement par git commit mais pas poussées par git push sont aussi perdues.

Aide-mémoire

Procédure à suivre pour éditer un fichier et partager la nouvelle version (toutes les commandes sont bien sûr à taper depuis le répertoire contenant le dépôt) :

  • git pull (télécharge la dernière version du serveur)
  • effectuer ses modifications
  • git commit -a et taper un message explicatif (enregistre la modification localement)
  • git push (envoie la modification au serveur)

Pour ajouter un nouveau fichier au dépôt

  • éditer le fichier normalement
  • git add nomDuFichier
  • git commit

Procédure en cas de conflit :

  • git push proteste et conseille de lancer git pull
  • si git pull ouvre l'éditeur de message de commit, valider le message et lancer git push
  • si git pull signale que le conflit perdure, éditer les fichiers en conflit, remplacer tout le contenu entre marqueurs de conflit <<<<<<<, et >>>>>>> par la version voulue, lancer git commit -a et git push.
updated on October 08 2019.