[isabelle-dev] Isabelle on Mercurial

Makarius makarius at sketis.net
Tue Dec 2 23:51:00 CET 2008

On Tue, 2 Dec 2008, Tjark Weber wrote:

> On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote:
> > With Mercurial you have the whole history always around, and there is no 
> > need to encode (tiny) parts of it in the file.
> Certainly $Id$ keys are rather useless as long as the file is part of a
> managed repository.  However, files escape into the wild.

In that case you would also have to add a checksum to make sure that the 
identification is actually correct, and require tools to check that fact.
Mercurial does exactly that for you, and more.

Note that Isabelle development snapshots also carry a Mercurial id 
already, and official releases can be mapped to an id via the release tag. 
Trouble starts when people tear distributions apart, but you cannot 
protect against everything.

For now it is most important to get people acquainted with the new 
environment, and refrain from any complications that are not really 

I recommend to use the system mainly for everyday things now, i.e. the 
same kind of things that would have been done last week with CVS, and not 
try out all the potentially cool things right now (at least not on the 
Isabelle repository).


More information about the isabelle-dev mailing list