[isabelle-dev] Relations vs. Predicates

[Lukas Bulwahn]

Hi Makarius, Hi Chris,

On 04/12/2012 08:12 PM, Makarius wrote:
> 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 was expecting that someone else who also feels responsible for names 
of the base theories would comment on the changes, but nobody did. So, I 
did not have the patience to wait any longer and pushed the changes.
If anyone present, for any reason knows why these two changesets should 
not be merged, let him speak now or forever hold his peace.

> 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.
>
I tried to do the rebase, but as the merge was non-trivial, the rebasing 
would have taken again quite some time, so I risked having a long edge 
in the repository graph instead.

I guess for the future, especially external contributions should provide 
patches without merges, but instead make sure that the patches can be 
applied to "the current tip" (even though this requires some maintenance 
from the contributor while internals are reviewing the changeset).

> 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.
>
In the commits, I only checked the "very minimal" requirements, although 
as you mention, there are many many aspects for future changesets that 
can be improved.

I still awaiting a good NEWS entry from Chris.


Lukas