Migrating the coq repository from svn to git

Author: Pierre Letouzey, with many other contributors (Enrico, Arnaud, Matthieu, Hugo...).

Note : this page is a wiki, please edit it to integrate your suggestions, remarks, criticism. Just ensure that your notes are visible, for instance by putting them into colored blocks like this one. In complement, you can also drop a message to coqdev.

Previous situation

Earlier, the official read-write repository of coq was a svn one on gforge.inria.fr. We already add an existing git clone of the coq svn repository, created and maintained via git-svn up to now :

 git://scm.gforge.inria.fr/coq/coq-svn.git

This clone was mirrored on github :

Many persons had cloned either of these repository and proposed their own extensions / experiments / ... on top of them.

Which content for the official git repository ?

We decided to reuse the content of these existing git clones.

Pros:

Cons:

The new repository

We decided to continue using gforge.inria.fr for the hosting of the official coq repository. In particular, all gforge accounts with commit rights on the earlier svn archive are still able to push commits on the git archive.

The url of the new repository is :

 git://scm.gforge.inria.fr/coq/coq.git

This url is for the anonymous access, for pushing commits you'll need to rather use:

 git+ssh://yourname@scm.gforge.inria.fr/gitroot/coq/coq.git

Of course, the github mirror is still maintained. There is also an anonymous access via an https url if necessary :

 https://gforge.inria.fr/git/coq/coq.git

But note that using this https protocol might not work out-of-the-box due to issues with the ssl certificate of gforge.inria.fr, more details in the gforge FAQ. A workaround is to set the environment variable "GIT_SSL_NO_VERIFY=true" in your shell, at least during the git operations.

The migration itself

The switch has been done on Tuesday, 19 November 2013.

For memory, here are the main steps used during the transition. More information on the process in the documentation and FAQ of gforge.inria.fr.

  1. First, the svn archive has been made read-only that day (via a pre-commit hook rejecting all new commits). Then this archive has been backuped somewhere else just in case.
  2. Then we stopped the cron task that runs git-svn and pushed updates to the existing git clones (on gforge and github).
  3. Then we asked for the svn=>git switch on the gforge interface (tab "source", sub-tab "admin"). This triggers a script that runs up to 6 hours according to the FAQ. This script initializes an empty coq.git repository somewhere on the gforge server, and adapts the "source" pages of the project (with a gitweb viewer, etc).

  4. We pushed to this coq.git repository all the content of coq-svn.git
  5. Some setup: in particular we forbid "non-fastforward push" (e.g. destructive, non strictly increasing change in the archive). See guidelines below.
  6. The mailing list coq-commits announcing each commit has been adapted (cf. FAQ + gforge bug ticket #15388).
  7. Tests : attempt to push a commit to check everything is all right (archive, gitweb, coq-commits)
  8. We removed the old svn repository : this way, nobody will stay by mistake on a not-evolving-anymore repository of Coq.
  9. Update any mention of the svn archive, especially on coq.inria.fr
  10. The mirroring to the github archive has been restored

Git usage and guidelines

Basic use

For the developer, this isn't a complete revolution. svn checkout is now git clone, and the usual cycle:

svn update && emacs && make && svn commit

is just replaced by:

git pull && emacs && make && git commit && git push

For those not familiar with git, note the difference between git commit (recording your modification to a local commit) and git push (transfering this commit to the remote repository).

Git documentation

Some documents about git:

Workflow

We keep for now the same workflow as earlier : one central repository, many commiters having access to this repository.

We also intend to keep the same principle as with svn : once a commit reaches the central repository, it stays there forever. By default, git provides many destructive features (history rewriting, commit reworking, etc). It's perfectly fine to use them on your computer, but not on commits already published, otherwise the other users will encounter issues during their next git pull. To avoid this situation, our gforge repository will be configure to accept only push of "fast-forward" commits (i.e. commits that only adds on top of commits already on the server). Note that this doesn't imply a linear history, since a merge of a branch can be fast-forward.

Advices

Misc

Coqbenchs

The current coqbench will have to be slightly adapted :

User Contribution Archive

This contributions are currently stored in a separate svn repository. We also plan to do something about this repository, but no definite plan nor migration date yet. First, let's do this migration of coq sources. Moreover, for contribs we probably want a notion of sub-repository, one per contrib.

Coqbugs

In coqbugs, we frequently refer to some specific commit (mainly to specify when a bug has been fixed).

External developpers

It will be easier now to propose patch when not being an authorized commiter, either :

And then warn some coq developper or the whole coqdev.

When the owner of the contribution (typically you or your employer) isn't Inria or an Inria partner, you might need to fill first a copyright delegation form. Of course you'll remain credited as the author of the contribution.

Github

Concerning pull requests made via github:

MigrationGit (last edited 22-11-2013 15:43:02 by PierreLetouzey)

Cocorico!WikiLicense