[isabelle-dev] Isabelle on Mercurial
makarius at sketis.net
Wed Dec 3 12:02:51 CET 2008
There is a useful convenience for synchronizing a local repository with
changes that have accumulated on the pull/push area: see "hg fetch" in the
Mercurial book http://hgbook.red-bean.com or the wiki.
The relevant section from the book is attached below.
The "fetch" command automatically handles routine merges, and clearly
indicates so in the log entry. A non-trivial situation needs to be
handled separately, with hand-written log entry as appropriate to the
situation. In most cases the message should be just "merged", unless a
real semantic conflict was resolved.
3.3 Simplifying the pull-merge-commit sequence
The process of merging changes as outlined above is straightforward, but
requires running three commands in sequence.
hg commit -m 'Merged remote changes'
In the case of the final commit, you also need to enter a commit message,
which is almost always going to be a piece of uninteresting "boilerplate"
It would be nice to reduce the number of steps needed, if this were
possible. Indeed, Mercurial is distributed with an extension called fetch
that does just this.
Mercurial provides a flexible extension mechanism that lets people extend
its functionality, while keeping the core of Mercurial small and easy to
deal with. Some extensions add new commands that you can use from the
command line, while others work "behind the scenes," for example adding
capabilities to the server.
The fetch extension adds a new command called, not surprisingly, "hg
fetch". This extension acts as a combination of "hg pull", "hg update" and
"hg merge". It begins by pulling changes from another repository into the
current repository. If it finds that the changes added a new head to the
repository, it begins a merge, then commits the result of the merge with
an automatically-generated commit message. If no new heads were added, it
updates the working directory to the new tip changeset.
Enabling the fetch extension is easy. Edit your .hgrc, and either go to
the [extensions] section or create an [extensions] section. Then add a
line that simply reads "fetch ".
(Normally, on the right-hand side of the "=" would appear the location of
the extension, but since the fetch extension is in the standard
distribution, Mercurial knows where to search for it.)
More information about the isabelle-dev