Hi Makarius,
On 04/13/2012 03:12 AM, Makarius wrote:
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.
Maybe "christ" would be better ;). But seriously, this is just my
default user name (and I didn't setup an hg specific one on my local
machine). Is my warmup-phase already over? Otherwise I would change the
name to "sternagel" (or something similar). (I guess the old changesets
will stick with the awkward name?)
And thanks for the detailed comments.
Piling private changes and public merges longer than 0.5-2 hours is
apt to produce some mess when pushing eventually!
I don't see how this can be avoided when pushing as an "external" from a
different time zone.
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.
I didn't use "hg import" yet. Maybe it would be a good idea (for
externals and developers) to have some "recipe" (e.g., at the community
wiki) that describes how to merge/import third-party changesets most
smoothly into the existing history.
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 ";").
Indeed. I hope my commit messages have at least been "correct" in this
respect?
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.
Unfortunately there are not so many people who know all this, and
Makarius' wisdom only comes by hindsight with fire and brimstone. ;)
(Just kidding! I'm glad about any comments that increase my understanding.)
- chris (a.k.a. griff ... this almost sounds alike ... if you lisp)
PS: sorry for being partly off topic.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
