[isabelle-dev] Relations vs. Predicates

[Makarius]

On Fri, 13 Apr 2012, Lukas Bulwahn wrote:

>> 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.

Which means I've read the history correctly.  It was OK in that situation, 
especially since "griff" is still warming up.


> 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).

Basically we already have the principle that contributions form a single 
chain of changes wrt. a recent tip of the repository, without any merge 
attempts yet.  Such a branch should normally graft easily on the latest 
local tip (without rebasing), if it is not too old yet.

Since external contributions happen so rarely, the process is hardly 
routine.  So it needs some more practice to make it work smoothly both for 
contributors and maintainers pushing.

I think that recent Mercurial now has a stable "rebase" command, so one 
should probably look there as well.  Personally, I do not like heavy 
rewriting of history, as is done routinely on many git projects -- it can 
introduce mistakes that are not recorded anywhere, while a messy merge at 
least contains the information in principle.  A little bit of rebasing of 
1 or 2 weeks time gap might work out smoothly, nonetheless.


BTW, since a year or so I try to make small contributions to jEdit, but I 
am still not there yet.  They have a rather awkward process that I do not 
quite understand, so whatever I do for jEdit is syntactically incorrect 
and ill-typed.

At least I've managed to excite some jEdit experts for the \<A> Unicode 
problem.  Another one even started looking into proper right-to-left 
type-setting, say for Arabic, but it is not going to happen soon.


 	Makarius