On Thu, 28 Apr 2011, David Aspinall wrote:

I am keen to use a more modern distributed system but it probably means choosing an external provider rather than trying to get the University to provide yet another semi-supported tool that works at the beginning and then rusts. Sourceforge is the most likely candidate.


I would not expect a paragraph that starts with "modern" end with "Sourceforge". They added some half-harted support for Mercurial, Bazaar, Git some years ago, and people rightly complained that it was "too late and too little".

There are many alternatives, and it depends a little on the cultural background of the VCS and the hosting platform you feel most comfortable.

For example, Google Code can give you SVN or Mercurial support which look very similar on the server side, but Mercurial users are free to work in their own way locally.

People with strong Linux (esp. Debian) background often prefer the central virtues of Github, which is more like a social network. (Git is a bit less comfortable on the client side than Mercurial, bt Github seems to be quite sophisticated.)

More exotic possibilites are Baazar and Darcs (for Haskell enthusiasts), but personally I think that these days the decision is only between Mercurial or Git. The reasons why we've chosen Mercurial for Isabelle:

  * The basic model is strictly monotonic, with immutable base operations;
    mutability is reserved to "maintenance tools".  This fits nicely into
    the functional / concurrent way of thinking of Isabelle/ML.  In
    contrast Git is more like C, i.e. you can poke around in the history.

  * Mercurial is a clean Python library, add-on tools can be written as
    Python programs.  Weakly typed Python is not the best programming
    language, but approximates the idea of "lambda calculus for system
    programmers" better than bash/perl that is used for Git around its C
    executables.

The motivation in the background is to connect the prover to the versioning system eventually, using the Pyhton library instead of script plmubing. Some beginnings of that can be seen here (by Alex Krauss and Florian Haftmann): http://isabelle.in.tum.de/reports/Isabelle/


Proof General source management is a bit less ambitious, of course.

I recommend that you look at Mercurial and Git and develop a taste for either of these two. It is a bit like Gnome vs. KDE, or Rosencrantz vs. Guildenstern, i.e. sometimes it is hard to tell the difference.

Maybe this one also helps: http://hginit.com/ (by Joe Spolsky), especially chapter 0 for people who think they have used version control already:

  It turns out that if you’ve been using Subversion, your brain is a
  little bit, um, how can I say this politely? You’re brain damaged. No,
  that’s not polite. You need a little re-education. I walked around brain
  damaged for six months thinking that Mercurial was more complicated than
  Subversion, but that was only because I didn’t understand how it really
  worked, and once I did, it turns out—hey presto!—it’s really kind of
  simple.


        Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to