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

2020-11-20 Thread 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...

-- 
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users


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

2020-11-20 Thread James Cook
On Sat, Nov 21, 2020 at 12:55:04AM +, James Cook wrote:
> On Fri, Nov 20, 2020 at 06:45:49PM +0100, Ben Franksen wrote:
> > Am 20.11.20 um 13:24 schrieb Ben Franksen:
> > >> 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.
> > 
> > What follows started out as describing a potential problem with this
> > idea, but in the end I found that is is easily solvable. The result may
> > even be an improvement over what we have today.
> > 
> > Remember that the actual named patches that the user interacts with
> > consist of multiple primitive patches (a "changeset"). Suppose for named
> > patches A=(a1;a2) and B=(b1;b2) we have a conflict, but only between a1
> > and b1 (this is a pretty typical scenario).
> 
> That's a good point. I wonder if it could happen with prim patches alone,
> though. Maybe some combination of hunks and substitutions, for example.

Oops, I didn't read your example carefully enough, and responded instead
to what I imagined you were talking about. Hopefully the rest of my email
still makes sense :-)

(I imagined you were suggesting that my example is avoided if you
somehow shift the focus to prim patches instead of patches. The
example I put together required each patch to be made of multiple
prims.)

-- 
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users


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

2020-11-20 Thread James Cook
On Fri, Nov 20, 2020 at 06:45:49PM +0100, Ben Franksen wrote:
> Am 20.11.20 um 13:24 schrieb Ben Franksen:
> >> 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.
> 
> What follows started out as describing a potential problem with this
> idea, but in the end I found that is is easily solvable. The result may
> even be an improvement over what we have today.
> 
> Remember that the actual named patches that the user interacts with
> consist of multiple primitive patches (a "changeset"). Suppose for named
> patches A=(a1;a2) and B=(b1;b2) we have a conflict, but only between a1
> and b1 (this is a pretty typical scenario).

That's a good point. I wonder if it could happen with prim patches alone,
though. Maybe some combination of hunks and substitutions, for example.

> 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.

> This suggests that we should present the "inactive" portions of a named
> patch in a special way e.g. "shaded"or with a bit of extra markup. In
> fact this may be superior to how Darcs operates today, where hitting 'v'
> on a conflictor shows you its internal representation, which isn't too
> helpful.

By hitting v do you mean passing -v to darcs changes? Or am I missing
some cool Darcs UI?

> Cheers
> Ben

-- 
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users


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

2020-11-20 Thread Ben Franksen
Am 20.11.20 um 13:24 schrieb Ben Franksen:
>> 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.

What follows started out as describing a potential problem with this
idea, but in the end I found that is is easily solvable. The result may
even be an improvement over what we have today.

Remember that the actual named patches that the user interacts with
consist of multiple primitive patches (a "changeset"). Suppose for named
patches A=(a1;a2) and B=(b1;b2) we have a conflict, but only between a1
and b1 (this is a pretty typical scenario).

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)!

This suggests that we should present the "inactive" portions of a named
patch in a special way e.g. "shaded"or with a bit of extra markup. In
fact this may be superior to how Darcs operates today, where hitting 'v'
on a conflictor shows you its internal representation, which isn't too
helpful.

Cheers
Ben

___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users


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

2020-11-20 Thread 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'