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

[Ben Franksen]

Am 03.07.20 um 05:22 schrieb James Cook:
> On Thu, 2 Jul 2020 at 18:40, Ben Franksen <ben.franksen at online.de>
> wrote:> The final chapter about the effect of extended patches and how
> to
>> resolve the conflicts they represent could use a bit of elaboration. For
>> instance, though you refer to the process, you haven't explained how
>> (extended) patches are merged. I think you will need to introduce
>> inversion for this. This is probably quite simple but maybe still worth
>> writing down explicitly.
> 
> I mention at the start "every merge is a clean merge in the new
> theory". So the procedure for merging A and B is supposed to be that
> you make A;A^;B then commute that to A;B;A^ and drop the A^. You could
> similarly merge three changes A B C by permuting A;A^;B;B^;C;C^ to
> A;B;C;A^;B^;C^.

I assumed as much.

> But yes, I realized after writing it that I never covered inverting
> extended patches.
> 
> Thinking about it more, I think I've found some problems. Let's say s
> is the starting context of A and B, and A ends with a and B ends with
> B. Here are three problems:
> 
> (a) I'm not sure inverses exist in general.

I had thought that was the easy part:

  (a, b, (Qi), (nj), X, Y)^ = (b, a, (Qi)^, (nj)^, Y^, X^)

where inversion for a set of names is the set of inverted names. You do
need names to be invertible.

> (b) Even when A^ and B^ do exist (e.g. if they're primitive patches),
> merging A and B in a different order results in different ending
> contexts. If you write A;A^;B then commute to A;B', you end up with
> the context (a, b, A^;B, {B}, {A^}). If you switch the roles of A and
> B, you end up with (b, a, B^;A, {A}, {B^}). It would be better if
> those two contexts were the same.

This reminds me (again) of the troubles with darcs-1 Merger patches.
Here we run into the problem that the representation is not canonical.
In other words, there are completely different "extended patches"
(mergers) that we have to regard as equal/equivalent in order for
permutivity to be preserved. This is best illustrated with a cube
consisting of three mutually conflicting patches starting from the same
context. Permutivity requires that the "second wave" of mergers is
consistent, so that e.g.

  Merger(Merger(a,b),Merger(a,c)) = Merger(Merger(b,a),Merger(b,c))

In darcs-1 calculating this equivalence is exponential because it uses a
nested representation. You may have more luck with your approach.

> (c) I think Proposition 5 might introduce duplicate primitive patches.
> Also, the patch sequence it generates is longer than it needs to be.

Ah, this may be true. If you add inverses you can run in circles, which
means encountering the same patch more than once in a sequence can no
longer be excluded. I guess you need to add rules that allow to
eliminate inverse pairs from a sequence...

> I've got an idea for solving all three of those. It involves a
> substantial change. I need to think more about it.
> 
> I've written about the starting point for that idea in the next two
> paragraphs, but you may wish to skip it until I've thought it through
> more carefully...
> 
> Everywhere one of those sequences (Qi) appears in an address, add a
> requirement that (Qi) is a cycle: it starts and ends at the same
> context, and for every patch P that appears in (Qi), P^ also appears
> in (Qi). I'm pretty sure that if you don't care about addresses being
> minimal, you can always extend ("unsimplify"?) an address to satisfy
> this property. I would need to adapt the definition of "minimal" to
> accommodate the cycle requirement. Also, the definition of
> "equivalent" would need to be extended substantially, so that for
> example the cycles A^;B;B^;A and B^;A;A^;B would be considered
> equivalent.

Indeed, for a cycle you have no starting and ending context, so any
cyclic (sic!) permutation is equivalent.

> My intuition is that (a) will somehow be solved by the sequence (Qi)
> always having inverses; (b) will be solved because we've expanded the
> notion of "equivalent"; and the solution to (c) will have something to
> do with rotating the cycle to start and end at the associated
> primitive context c.
> 
> But I haven't thought it through fully, so what I wrote might turn out
> to be nonsense.

It sound like something worth pursuing to me.

>> I find the last chapter hard to follow because I don't quite understand
>> the motivation. It sounds as if what you are saying here is that we
>> cannot merge patches from another repo as long as our repo is
>> conflicted. But that cannot be true if all patches can be commuted. Or
>> is this about /recording/ new patches in a conflicted repo? Some
>> clarification would be helpful.
> 
> The issue is recording new patches. I tried to explain that in the
> remark: "In other words, the problem here is that after applying a
> conflicted patch, e.g. after a conflicted merge, the user would like
> to be able to get back to work applying ordinary patches."

Ah, okay.

> Maybe I
> should change the last three words to "recording new primitive
> patches"?

Yes. Applying suggests you already have a patch.

> Here's my attempt to work through an example of the problem:
> 
> * Suppose primitive patches A^ and B don't commute and we try to merge
> A and B. So, we permute AA^B to AB'A^' and then drop A^' from the end.
> Let c' be the starting context of A and B (because I called it c' in
> Chapter 7).

(I would rather use the primed notation "c'" for the extended context
throughout.)

> * The final context of the repo, after AB', is a context outside the
> primitive patch theory. This is called c in Chapter 7. If we don't
> mark the conflict in some way, then to the user, c looks just like its
> associated primitive context, which is c' (i.e. the context before
> applying either A or B).
> 
> * Now the user wants to continue working, so they create a primitive
> patch C which has starting context c'. Assume C doesn't commute with
> A^ or B^.
>
> * We need C to have starting context c in order to apply it to the
> repo. Naïvely, we might try to commute C to an extended patch C' with
> the same name but starting context c.
> 
> * However, that new patch C' will not have the expected effect.
> Applying C from context c' will just turn our two-way conflict into a
> three-way conflict. We end up with the patch sequence AB'C', the
> ending context of which is another extended context which is
> associated with the original primitive context c'.
> 
> * In summary, applying C (as its commuted form C') ended up having no
> effect on the repo.

Okay, I see the problem now. Thanks for explaining.

In Darcs we don't have this problem because we do not distinguish
between primitive and extended contexts. You can just revert the
conflict markup and record anything you like. If this happens to overlap
(i.e. depend on) the changes reverted by the conflict, then it is
regarded as a conflict resolution. It is clear that this cannot work in
your theory, so you need something else to mark a conflict as resolved.
Sounds like an interesting problem indeed.

As I remarked a while ago in a different discussion, adding a proper
force-commute operation to darcs is unsound for the simple reason that
we could no longer unambiguously define what it means for a repo to have
(unresolved) conflicts: (force-)commuting any two patches makes the repo
conflicted. Your approach solves that problem nicely, but now you have
to find a way to get away from a conflicted repo state.

Regarding your proposed solution, I think Proposition 5 cannot be true
unless you add inverses. Here is a counter example: we have prims
A;(B\/C), where neither A;B nor A;C commute as prims. The extended
universe of patches adds the force-commuted sequences B';A' and C';A'',
together with their mid-contexts. But that's it: you get two sides of
the cube, with a common edge (A). Without inversion there is no way from
the mid-context of B';A' to that of C';A''.

If, however, you add inverses, then Proposition 5 is trivial.

Cheers
Ben