[darcs-users] How conflictors work
David Roundy
droundy at darcs.net
Tue May 20 14:32:19 UTC 2008
On Mon, May 19, 2008 at 08:11:41PM +0100, Ian Lynagh wrote:
> On Mon, May 19, 2008 at 11:48:16AM -0400, David Roundy wrote:
> > On Sat, May 17, 2008 at 9:45 AM, Ian Lynagh <igloo at earth.li> wrote:
> > > On Sat, May 17, 2008 at 04:18:21AM -0700, David Roundy wrote:
> > >>
> > >> In definition 4.7 (merge), I don't see why you restrict yourself to
> > >> the merging of conflicts where Esp and Esq are disjoint. It's trivial
> > >> to construct an example where this isn't the case. e.g. consider the
> > >> merge of three patches A, B and C that each modify the same line.
> > >> First you construct AB' and AC', and then you merge B' and C', both of
> > >> which have the same patch in their effect.
> > >
> > > In that case that patch would be in Es_b (b for "both").
> > >
> > > I should remove that line of English, actually, as it might be confusing
> > > given it's also in the side condition of the equation.
> >
> > Actually, I'd vote for fixing it.
>
> I'm not sure I follow. We're talking about this:
>
> And finally, where Es_p and Es_q are disjoint:
>
> [Es_b Es_p, Zp, Ps : p] + [Es_b Es_q, Zq, Qs : q] = ...
>
> Here Es_p and Es_q must be disjoint; any element they might have in
> common would instead be in Es_b in both conflictors.
Oh, I'm stupid. When I read that bit (and reread it) I didn't see that
you'd pre-separated the common part of the effects.
> > Maybe it would make sense to try to implement your merge algorithm
> > before attempting to prove it correct? I would be highly surprised if
> > you were able to prove it correct, and a quick run through unit should
> > be able to prove it incorrect. Or perhaps the typechecker would
> > succeed at that?
>
> That sounds like a good idea. Is it easy to change the conflictor
> definition in darcs and run the unit tests without also updating the
> rest of darcs to build with the changes?
Yeah, that's how I implemented the conflictors in the first place.
> > > Hmm, OK. I don't think I agree at this stage, but perhaps I will once I
> > > get deeper into it!
> >
> > If you make identical patches conflict and use bags rather than sets,
> > then you have the following sort of interesting problem, where you've
> > got two identical changes A and A that are merged, resulting in
> >
> > A [{:A},invA,:A] (repo 1)
>
> OK, so at the named-patch level this is A1 + A2
>
> > Now someone decides to resolve these changes by adding a new identical
> > patch A (but in the context that containts these two changes. So we
> > have
> >
> > A [{:A},invA,:A] A (repo 2)
>
> Right, A1 A2' A3.
>
> > Now a different person pulls the two original conflicting A's from
> > repo 1 into a repository that already contains A and gets
>
> Which A do they already have? an entirely new A, A4?
If the As are identical, then you can't tell. But I presume an A4.
> > A [{:A},invA,:A] [{:A,:A}, ,:A] (repo 3)
>
> A4 A1' A2''?
>
> And we can commute this to A1 A2' A4', and the result had better look
> the same as this is just A+A+A either way:
>
> A [{:A},invA,:A] [{:A,:A}, ,:A]
>
> > Now we merge repo 2 with repo 3,
>
> So this is
>
> A1 A2' (A3 + A4'):
>
> A [{:A},invA,:A] (A + [{:A,:A}, ,:A])
>
> If contexts are sequences of patches then we have
>
> A + [{:A,:A}, ,:A] = A [{:A,:A,:A}, invA,:A]
> = [{:A,:A}, ,:A] [{:A}, , :A]
>
> so the answers are
>
> A [{:A},invA,:A] A [{:A,:A,:A}, invA,:A]
> A [{:A},invA,:A] [{:A,:A}, ,:A] [{:A}, , :A]
>
> These are different to your answers, as you have sequences of catches,
> and I don't have transitive conflicts.
>
> > and we get (depending which way we pull) either
> >
> > A [{A},invA,:A] A [{:A,:A,A[{:A},invA,:A]:A},invA,:A]
> >
> > or
> >
> > A [{A},invA,:A] [{:A,:A}, ,:A] [{:A,:A}, , A[{:A},invA,:A]:A]
> >
> > but this all assumes that we have some way of knowing which of these
> > As were the same A as the other ones, otherwise we'd be up a creek
> > without a paddle. Which means that we need to store an ID with each
> > patch, which means that the patches A, A and A are not actually
> > identical.
> >
> > Note that this example also demonstrates why you need catches to
> > define the context of contexted patches.
>
> I don't see what went wrong doing it my way.
That's all right.
David
More information about the darcs-users
mailing list