[isabelle-dev] Relations vs. Predicates
c-sterna at jaist.ac.jp
Fri Apr 13 04:51:00 CEST 2012
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
> 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.
More information about the isabelle-dev