[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

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.