[isabelle-dev] Sane Mercurial history

[Makarius]

Dear Isabelle contributors,

this is a reminder of some basic principles that ensure that our history
remains manageable.

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).


 	Makarius