Monday, 9 May 2011

Github (and git) for HOL4 development?

Listening to:

Mahler, symphony no. 9. Pierre Boulez conducting the Chicago Symphony Orchestra.

Version Control Systems

I’m beginning to think that we should move HOL4 off Subversion and onto git, preferably hosted on Here’s why:

  • Most importantly, git makes dealing with a certain class of contributor easier. Currently, the Subversion at SourceForge setup means that we can only support two sorts of developer: the regular developer that is allowed to make arbitrary commits across the whole source-tree; and the very occasional developer who mails a regular developer a patch. The regular developer makes the commit themselves, perhaps adding that the bug-fix, additional theory or whatever came from the very occasional developer.

    With git, we can have an intermediate class of developer, the occasional developer. These people can establish their own forks of the source-code, do their own stuff with it, and then make pull requests. If their commits do get incorporated into the “official” repository, their names will still be attached to the commit objects.

  • An advantage of moving to github specifically is that it allows us (through “beta” software admittedly) to view a git repository as a Subversion one, meaning that existing HOL4 developers who don’t want to have to learn git can continue to make commits using the svn command-line tool, in a way that will remain familiar.

    This facility at github is described (in rather sketchy fashion) here.

  • The last advantage is that git is just much cooler than Subversion in many ways. In particular, it gives developers good support for branching and merging, with complete local copies of repositories.

Possible disadvantages:

  • The support for Subversion as a git client at github may not be robust.

  • Our big existing Subversion branch (HOLω; see here) may prove difficult to graft onto the git repository in a nice way.

    My guess at the moment is that we could checkout master, dump the HOLω branch on top of that and do a fresh commit. In that way, we would encapsulate all of the existing history in one huge commit. The subsequent development of HOLω on that branch could use git’s good support for cherry-picking and merging in general to pull across new stuff from master.