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
