[isabelle-dev] Sane Mercurial history

[Brian Huffman]

On Wed, Mar 3, 2010 at 8:54 AM, Makarius <makarius at sketis.net> wrote:
>  * 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).
...
>    Of course, the merge nodes produced for preparing a push also need to
>    be fully tested (isabelle makeall all).

Note that these requirements are somewhat in conflict with each other.

Running all the tests with "isabelle makeall all" already takes me
nearly 0.5 days, during which time it is very likely that the
repository will have changed again. If I required myself to run
"isabelle makeall all" after merging and immediately before each push,
I might be able to push my changes once or twice a week, during
periods of low activity on the repository.

The alternative is to take shortcuts on testing. Here's what I usually do now:
1. pull and merge
2. make edits and local commits
3. compile and test everything on a separate machine
... hours pass ...
4. pull and merge again if necessary
5. check that there were no non-trivial file merges
6. push

I think this is a reasonable compromise between thoroughness of
testing vs. timeliness of pushing.

- Brian