[isabelle-dev] Relations vs. Predicates

[Makarius]

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