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

[Ben Franksen]

Am 21.11.20 um 03:13 schrieb James Cook:
>>> How do we present this at the user level?
>>>
>>> The unresolved conflict is probably presented quite similar to how we do
>>> it in Darcs now: we tell them that there is a conflict between A and B
>>> and present the alternatives a1 and b1 as the "content" of the conflict,
>>> e.g. using conflict markup.
>>>
>>> So far so good. But what about conflict resolution? Suppose the user
>>> decides that a1 is what they want after all. How do we represent the
>>> chosen sequence, consisting of
>>>
>>>   A=(a1;a2);B=(b2)
>>>
>>> with a "crippled" B in a sensible way?
>>>
>>> This is just a UI question, but it may be important. For instance, if a
>>> different user later pushes B to another repo, they may be surprised to
>>> see that what they push contains more prims than they could see i.e. it
>>> will be the original B=(b1;b2)!
>>
>> Although I haven't fully worked it out, the answer I'm leaning toward
>> is that the deactivation of b1 behaves like a patch (b1 inverse, if you
>> want to think of it that way). So if your repo has B=(b2), that really
>> means it has b1,b2,b1^; b1^ probably appears as part of the conflict
>> resolution patch. When you push your changes, b1^ gets pushed too. There
>> is no way for b1 to ever become active again, except obliteration of b1^.
>>
>> I like this point of view because it gives a simple monotone rule about
>> what happens to each prim when you push: each prim can be in state 0
>> (not present), 1 (present) or 2 (was present but now deleted), and
>> merging puts each prim in the max of the two original states (plus
>> conflict resolution, which is also monotone). This is what I was
>> thinking in an earlier email when I said I want "inverses on all the
>> not-chosen branches instead of a flag on the chosen branch" of the
>> tree.
> 
> Oops, this doesn't really answer the question you raised. The user would
> still push both b1 and b2 if they decide to push just B. I need to slow
> down a bit...

Whether it answers the question I raised or not, I am not sure I like
the plan you laid out above. (Before you reply, please read until the end.)

I dislike inversion of named patches (regardless of whether they are
"compound" patches i.e. changesets, or just named prims). One problem is
that a named patch and its inverse don't cancel. We have discussed this
at great lengths. It means that algebraically they aren't inverses in
the usual sense, but only in the much weaker sense of inverse monoids
(or inverse categories). Dealing with these weaker concepts of inversion
is considerably more difficult. A second and related problem is that the
presence of inverses leads to ambiguities wrt the semantics of
"contexts": on the one hand we want P;P^ to have identical starting and
ending context. But then we no longer have a tree of patches, but a
graph, and that graph is not even acyclic. And since we cannot cancel
inverses, a path through that graph is not allowed to make "shortcuts".
This makes the whole idea of patches leading from one context to another
quite unintuitive IMO.

Here is what I imagined things to work (but note the caveat below):

We mark the "chosen" patches as "active" (or, equivalently, mark the
"unchosen" patches as "inactive") and remove the ability to invert named
patches from the theory. I am convinced that for the merge algorithm
(the "flattened" version w/o considering changesets i.e. only for named
prims) we won't be missing inversion at all. The idea is that inactive
patches are still 100% first class members of our repo: their inactive
status can change to active at any time. This is necessary, since e.g.
obliterating all conflicting patches must turn it into an active one.
Similarly, choosing a different resolution to the conflict will move the
active flag from one patch to another. Of course there need to be
restrictions in place that guarantee that this doesn't violate
invariants. The most important such invariant in this regard is that the
active patches form a path in the tree that starts at the root (empty
context). Thus, if an active patch B depends on another (necessarily
also active) patch A, then then A cannot change its status to inactive
without B also becoming inactive.

However, after writing the above I realised that this idea has a serious
flaw: a repo is no longer defined by the set of patches that it
contains! If A and B conflict, then one repo may have {A,(B)}, while
another repo has {(A),B} (where the notation (X) means that X is inactive).

If instead of marking patches as active/inactive we add inverses for
inactive patches, as you proposed above, we can avoid that problem. So a
conflict resolution always has to be a new patch that (at least) inverts
all but one of the conflicting alternatives. Such a theory will be even
closer to that of Darcs with (V3) conflictors.

I fear that dealing with nested conflicts in such a theory will be
similary unwieldy as in Darcs. What I mean is the scenarion where one
repo has A;B;C;... which depend on one another, and another has X which
conflicts with A. We pull A on top of X and resolve the conflict. Then
we pull B and have to resolve the same conflict again because B will
conflict with our resolution. And so on with C etc. But I may be wrong
about that.

It is also unclear to me how to handle a repo with unresolved conflicts:
on the one hand the inversion is part of the resolution instead of being
part of the (conflicted) patch, but on the other hand we cannot have
both conflicting patches applied! So your VCS will have to add some sort
of "automatic resolution patch". Unfortunately, such a patch cannot be a
first class citizen; for instance, we cannot obliterate it.

Cheers
Ben