[darcs-users] How to extend a patch theory to fully commute

[Ben Franksen]

Hi James

Am 19.11.20 um 22:44 schrieb James Cook:
>>>> I still wonder if a consistent patch theory *different* from
>>>> camp/darcs-3 could be devised in which conflict resolutions really are
>>>> freely exchangeable with the conflicted patches instead of depending on
>>>> them. In other words, we may *choose* one of the conflicting patches as
>>>> the resolution (creating a new one if none are suitable). I think this
>>>> would require, in the tree view, to add a special flag to mark such
>>>> patches as the chosen resolution. This would make the theory more
>>>> symmetric and would perhaps also make resolving conflicts easier to
>>>> handle; and perhaps simplify commute and merge, too. I haven't thought
>>>> this through, though, and it may turn out that this doesn't work.
> 
> First, a quick recap for some context. I think you framed it best in the
> quotation at the top of this email. I would like a patch theory where
> conflict resolutions are just new patches that replace the conflicting
> ones, and don't depend on the patches they're resolving.

Yes.

> We had talked about doing this by representing a repository as a tree of
> patches rooted at the start context, and one path from the root is
> flagged as the "chosen resolution" (or, everything outside that path is
> marked as deleted).
> 
> My example will show that if we do things that way, we must allow
> patches to appear in more than one place in the tree (in other words,
> multiple patches with the same name).

Interesting. I haven't thought about it like that before. Indeed this is
what happens in Darcs (V3), too: different conflictors may contain named
prims with the same name in their representation. Indeed it seems that
it is quite necessary to allow that, as shown by your proof below.

> Fortunately, these duplicate
> patches don't appear along the "chosen resolution". So, if we're
> careful, they might not cause any real trouble, but it's still a bit
> disappointing to me, since it would have been neat and tidy to have
> every patch just appear once.

Yes. I would have found it disturbing if the same patch could appear
twice along the chosen route, that is, I would take it as an indication
that there is something wrong with the theory. It should be possible to
prove that this cannot happen, once we have a precise spec of the merge
algorithm for "tree-like" repos. For Darcs this is clear, since the
effect of a conflictor consists of inverses of previous patches, and we
do have an invariant that every patch is reverted in this way at most
once (namely by the first conflictor that conflicts with it).

> I'm going to start thinking about what we can do if we simply accept
> that our repository might have multiple patches with the same name
> (but not along the chosen resolution).

Yup.

> ********
> 
> The example: suppose we want to merge these two repositories.
> 
>     b   a   d
>   *-->*-->*-->*
>       |
>       |f
>       v
>       *
> 
>     c   a'  e
>   *-->*-->*-->*
> 
> a and a' have the same names. For this example, I'm not concerned
> with the chosen resolutions, but you could imagine for example
> they're b,a,d and c,a',e.
> 
> Suppose:
> * b and c conflict.
> * a conflicts with f;
> * b and f don't commute;
> * d doesn't commute with b or a;
> * e doesn't commute with c or a.
> 
> Just to show that could really happen, here are some patches that behave
> like that:
> * a and a' create a file called "a".
> * b and c create a file called "b".
> * d and e both delete both files "a" and "b".
> * f creates "a" and deletes "b".
> 
> I claim the merged repository must have two patches with the same name.
> 
> Proof:
> 
> The merged repo has to be a tree with all the patches a, b, c, d, e, f.
> (This is an assumption --- when we merge repos we keep all the patches,
> and repos are always trees.)
> 
> Since d depends on both a and b, our tree must have a node where both a and b
> are applied, i.e. a path from the root with the names a and b.
> Similarly, because e depends on a and c, there must be a path from the
> root with the names a and c.
> 
> Suppose the merged tree has only one patch named a. (Otherwise we're
> done.) Then the a,b and a,c paths both have to share that same patch.
> Since b and c conflict, a has to come before both b and c. The situation
> looks something like this:
> 
>     a   b  d
>   *-->*-->*-->
>       |
>       |c
>       v
>       *-->*
>         e
> 
> Now, f has to appear somewhere in the merged tree. f depends on b but
> conflicts with a. So somewhere in the tree there needs to be a patch
> named b that doesn't have a before it. So we need another patch named b.
> 
> QED.

I can see no mistake in your reasoning.

> In other words, the merged repo either has two patches named a, like
> this:
> 
>     b   a   d
>   *-->*-->*-->*
>   |   |
>   |c  |f
>   v   v
>   *   *
>   |
>   |a'
>   v
>   *-->*
>     e
> 
> or has two patches named b, like this:
> 
>     a   b  d
>   *-->*-->*-->
>   |   |
>   |b' |c
>   v   v
>   *   *-->*
>   |     e
>   |f
>   v
>   *
> 
> We could simplify the example by removing f and asserting a doesn't
> commute with b or c. But I think that situation could not arise in
> practice: if we see a in the context b and also in the context c, that
> implies it commutes with both, otherwise how could it have ended up in
> both places?

Exactly. For the example to be possible a needs to commute with b and c,
otherwise we cannot have the nominally same patches a and a' after
conflicting b and c.

Thanks for sharing this. I found it interesting and instructive. And I
believe you are on a good road!

Cheers
Ben