[isabelle-dev] Sane Mercurial history

[Makarius]

On Wed, 3 Mar 2010, Brian Huffman wrote:

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

I would call this a non-problem.  Even on low-end hardware from 2 years 
ago the makeall all can be done in 1-2 hours -- although I am still hoping 
for someone to work out a way to use one of these distributed make tools.

You do have an official account at TUM, so it should be possible to work 
out a scheme how you can make use of some suitable machines (e.g. 
macbroy20..29).


 	Makarius