[isabelle-dev] Sane Mercurial history
makarius at sketis.net
Wed Mar 3 17:54:25 CET 2010
Dear Isabelle contributors,
this is a reminder of some basic principles that ensure that our history
It is important to keep in mind that this is a continous communication
with everybody else working on the sources. There are hardly any isolated
parts that could be considered "private", because global system cleanup
can always affect everything. (The authentic syntax effort is a good
example for this.)
Although Mercurial allows to stay separate for a long time and merge back
later, one always needs to keep the semantical complexity in mind. The
basic assumption is that distributed changes are mostly orthogonal,
resulting in trivial merges. Unclear situations, with duplication or lost
update are a counterexample for this -- it usually takes several hours to
disentangle such knots.
>From the experience of the last year or so, the following mode of working
is able to keep the workload for everybody involved at a minimum:
* Before editing, always pull/fetch from public. Do not continue from
your last change, but the most recent one from out there.
* Do not forget about small commits in your local history. Push quickly
(after full isabelle makeall all, of course).
* For longer "projects" the timespan of staying in splendid isolation
is limited to 1-3 days (3 is already quite long, and personally I
usually try to stay within the 0.5-1.5 days interval).
The local history produced in that timespan should be as clear (and
linear) as possible. In particular, intermediate merges with the
public should be avoided. Merge if and only if preparing for a push.
Of course, the merge nodes produced for preparing a push also need to
be fully tested (isabelle makeall all).
More information about the isabelle-dev