On Wed, 11 Apr 2012, Christian Sternagel wrote:
On 04/05/2012 12:30 PM, Christian Sternagel wrote:
Hi Lukas,
thanks for testing! (Sorry for the late reply, currently my
internet-connectivity is rather sporadic ;)). Please find attached a hg
bundle that does the name change 'rel_comp -> relcomp' for the AFP.
It seems that Lukas has now pushed that, see Isabelle/d8fad618a67a
I now also know who this mysterious "griff" from AFP is :-) Seriously,
you have the free choice to specify your user name for Isabelle hg
contributions, but you need to stick to it in the long run. In the
initial warmup-phase you have one chance to rethink the initial choice,
but do not have to do so.
Is something wrong with my changesets? ;)
You are an experienced Mercurial user already, so there are few technical
things to say here. Semantically, the principles in the (slightly long)
file README_REPOSITORY of the Isabelle repository apply, even when things
are pushed by an intermediary person with administrative push access (the
latter is also resposible to inspect incoming things in this respect).
In the explanations there is a section about merges with a few important
hints:
* Accumulate private commits for a maximum of 1-3 days.
...
* Test the merged result as usual and push back in real time.
Piling private changes and public merges longer than 0.5-2 hours is
apt to produce some mess when pushing eventually!
Since your changes 07f4bf913230 and b75ce48a93ee were a bit too long stuck
in the pipeline, you then had a non-trivial merge in e1b761c216ac. It
seems that Lukus did not want to redo that via a variant of "rebasing"
(e.g. plain "hg import" of individual changesets on tip), so he re-merged
the whole thing with his current tip in d8fad618a67a and then pushed it.
Isn't it nice what the history of Mercurial tells? When producing the
history one also needs to keep readability and clarity in mind -- it needs
to be studied routinely when sorting out problems. Moreover, incoming
changesets needs to be easy to inspect in a few seconds or minutes. (This
is why I always ask to write each log item on a separate line, but still
with a delimiter such as ";").
Nothing bad happened despite all these static type errors in the above
changes, nonetheless one needs to maintain a routine of "correctness by
construction" of Isabelle history. Over the years, I had occasionally
spent several hours or days (or rather nights) trying to disentangle
unclear situations for particularly odd changesets.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
