[isabelle-dev] Relations vs. Predicates
makarius at sketis.net
Fri Apr 13 11:33:28 CEST 2012
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
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.
More information about the isabelle-dev