Re: [darcs-users] How to extend a patch theory to fully commute
On Sun, Nov 22, 2020 at 07:58:18AM +0100, Ben Franksen wrote:
> Am 21.11.20 um 22:25 schrieb James Cook:
> > I was, however, thinking that deactivation would be "permanent" or
> > "sticky", in the sense that once a prim patch has been deactivated, it
> > cannot be re-activated except by obliterating the thing that
> > deactivated it.
>
> What is that "thing that deactivated" a patch, say P?
>
> If it is any other patch Q (present in our repo) that conflicts with P,
> which is how I understand the idea, then your patch theory is equivalent
> to that of Darcs! Because this is exactly what a conflictor is/does: it
> "deactivates" any previous conflicting patches (unless they have already
> been deactivated). It also deactivates itself, of course.
>
> But we wanted to design a different patch theory. One where I can pick
> and choose among conflicting (sequences of) named prims. And where any
> conflict resolution I am doing manually is just another conflicting
> variant I add into the mix. Or at least that is how I understood the idea.
>
> Let's make this all a bit more concrete:
>
> Show me a scenario in which your system behaves differently from Darcs
> in a user-visible way. A simple example to demonstrate what you want to
> achieve.
I put some examples in the write-up I just linked
(https://www.falsifian.org/a/xxOw/misc.pdf). Section 4.1.1 shows that
it allows a few different ways to resolve conflicts, including
Darcs-style replacement of the original patches, or keeping one of the
two patches and "rebasing" the other one on top of it (by recording a
new prim patch with a new name, but which is intended to have the
effect of the other conflicting patch). I think it could also be used
to allow non-destructive manipulation of repository history; I wrote
about that in 4.1.5 but didn't go into much detail.
> >> 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.
> >
> > This is essentially my motivation for making deactivation "permanent".
> > It makes merging of repos easier to reason about.
>
> You need to be clearer about what you mean when you say "permanent". In
> a distributed VCS you cannot influence what happens in other
> repositories. So a (named prim) patch may be active in one and inactive
> in another repo. When these repos exchange patches, will they have to
> exchange information about active/inactive state of their patches? In
> that case you violate the principle of "a repo is a set of patches". If
> not, then how can the overall behavior be any different from that of Darcs?
In the end, I was able to allow patches to be re-activated. (It might
have been simpler not to, but I think it's worth the complexity.)
My section on "destructive" and "non-destructive" operations (4.2.4)
suggests a possible definition for "permanent". A state of affairs is
"permanent" if it persists through any non-destructive operation.
For the most part, my write-up actually does violate the principle that
"a repo is a set of patches", but this is mitigated by two things:
* A partial ordering on repositories, that shows we can still make
sense of what should happen when pushing/pulling and recording new
changes.
* In Section 4.2.11 I attempt to show how to keep some aspects of "a
repository is a set of patches". Specifically, a "tree patch
repository" (Definition 21) is in some sense identified by the set of
"tree patches" in it.
> >> 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.
> >
> > Hopefully we won't need the "automatic resolution patch". Instead, we
> > could do this. First, create pending changes that deactivate both
> > conflicting patches, but don't record them yet. Then modify the working
> > directory by adding conflict resolution markers. The user should then
> > resolve the conflict by editing the files. When they record, the two
> > pending deactivations will be included as part of the "conflict
> > resolution" patch they make.
>
> What if I revert all pending changes? This will remove
Re: [darcs-users] How to extend a patch theory to fully commute
Am 21.11.20 um 22:25 schrieb James Cook:
> I was, however, thinking that deactivation would be "permanent" or
> "sticky", in the sense that once a prim patch has been deactivated, it
> cannot be re-activated except by obliterating the thing that
> deactivated it.
What is that "thing that deactivated" a patch, say P?
If it is any other patch Q (present in our repo) that conflicts with P,
which is how I understand the idea, then your patch theory is equivalent
to that of Darcs! Because this is exactly what a conflictor is/does: it
"deactivates" any previous conflicting patches (unless they have already
been deactivated). It also deactivates itself, of course.
But we wanted to design a different patch theory. One where I can pick
and choose among conflicting (sequences of) named prims. And where any
conflict resolution I am doing manually is just another conflicting
variant I add into the mix. Or at least that is how I understood the idea.
Let's make this all a bit more concrete:
Show me a scenario in which your system behaves differently from Darcs
in a user-visible way. A simple example to demonstrate what you want to
achieve.
>> 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.
>
> This is essentially my motivation for making deactivation "permanent".
> It makes merging of repos easier to reason about.
You need to be clearer about what you mean when you say "permanent". In
a distributed VCS you cannot influence what happens in other
repositories. So a (named prim) patch may be active in one and inactive
in another repo. When these repos exchange patches, will they have to
exchange information about active/inactive state of their patches? In
that case you violate the principle of "a repo is a set of patches". If
not, then how can the overall behavior be any different from that of Darcs?
>> 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.
>
> Hopefully we won't need the "automatic resolution patch". Instead, we
> could do this. First, create pending changes that deactivate both
> conflicting patches, but don't record them yet. Then modify the working
> directory by adding conflict resolution markers. The user should then
> resolve the conflict by editing the files. When they record, the two
> pending deactivations will be included as part of the "conflict
> resolution" patch they make.
What if I revert all pending changes? This will remove the markup as
well as the pending changes that remove the conflicting patches.
Furthermore, pending changes are (at least in Darcs) unnamed prims. That
makes sense because when the user edits a file or says something like
'darcs add filename', we don't yet have a patch name for that prim.
The only viable solution to this problem would be to store the "open
conflict" patches separately from regular pending patches and also make
them "unrevertable". But again, that seems to be equivalent to what you
have in Darcs with conflictors.
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
On Sat, Nov 21, 2020 at 07:55:28PM +0100, Ben Franksen wrote: > 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 hope my below responses address some of your concerns. Hopefully I will also have a write-up soon so it'll be more clear what I'm talking about. > 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. I agree that patch inverses can cause confusion when we allow them to appear in patch sequences. The lines I've been thinking along lately don't really have any place for "inverse patches" (except maybe as temporary objects that exist when computing a merge). I was, however, thinking that deactivation would be "permanent" or "sticky", in the sense that once a prim patch has been deactivated, it cannot be re-activated except by obliterating the thing that deactivated it. The only reason for this requirement is that it makes it easier to reason about how everything will work. An implementation of this might end up accumulating "deactivation markers" to help keep track of which patches have been deactivated. This is what I meant by "inverses on all the not-chosen branches". Maybe I should not have called them "inverses", because they would not behave like inverse patches (they're nothing more than a name; they cannot appear in a patch sequence). Does that resolve your concern about the bad behaviour of inverse patches? Below, you have a good argument that the "permanent" aspect of deactivation could cause problems, which I've responded to. > 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. I
Re: [darcs-users] How to extend a patch theory to fully commute
On Sat, Nov 21, 2020 at 06:02:49PM +0100, Ben Franksen wrote: > >> 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? > > Indeed! Try 'darcs log -i' (for interactive). For each patch you are > presentetd with a menu of keys to get more detailed information about > the patch. This is the same when you pull or push or whatever. Hitting > '?' will display help about the available keys. > > Example: > > >darcs log -i > patch a4b12fc212dadeacd92c47b262ff999db6451a69 > Author: Ben Franksen > Date: Tue Nov 3 00:39:30 CET 2020 > * resolve issue2632: remove context from patch bundles > > The function makeBundle has one less parameter now and is pure. > Shall I view this patch? (1/?) [yN...], or ? for more options: ? > How to use view changes: > y: view this patch and go to the next > n: skip to the next patch > > v: view this patch in full > p: view this patch in full with pager > r: view this patch > x: view a summary of this patch > > q: quit view changes > k: back up to previous patch > j: skip to next patch > g: start over from the first patch > c: count total patch number > > ?: show this help > > : accept the current default (which is capitalized) > > Cheers > Ben Thanks, that will be useful! -- 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
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
Re: [darcs-users] How to extend a patch theory to fully commute
>> 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? Indeed! Try 'darcs log -i' (for interactive). For each patch you are presentetd with a menu of keys to get more detailed information about the patch. This is the same when you pull or push or whatever. Hitting '?' will display help about the available keys. Example: >darcs log -i patch a4b12fc212dadeacd92c47b262ff999db6451a69 Author: Ben Franksen Date: Tue Nov 3 00:39:30 CET 2020 * resolve issue2632: remove context from patch bundles The function makeBundle has one less parameter now and is pure. Shall I view this patch? (1/?) [yN...], or ? for more options: ? How to use view changes: y: view this patch and go to the next n: skip to the next patch v: view this patch in full p: view this patch in full with pager r: view this patch x: view a summary of this patch q: quit view changes k: back up to previous patch j: skip to next patch g: start over from the first patch c: count total patch number ?: show this help : accept the current default (which is capitalized) 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
> > 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
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
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
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
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'
Re: [darcs-users] How to extend a patch theory to fully commute
> >> 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. > >> > >> Cheers > >> Ben > > > > I think the goal I described in my other email just now would end up > > looking something like this, but with inverses on all the not-chosen > > branches instead of a flag on the chosen branch. > > Let me know if you have something concrete that looks promising. > > Cheers > Ben Hi Ben, I just picked this up again. I do not have a solution right now, but I did find an example showing a limitation of the "tree view" which I wanted to share. Feel free to ignore this and just wait to see if I have positive news to share later. This is mostly an exercise for me to write up what I found for future reference. 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. 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). 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. 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). 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. 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? -- 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
Am 01.10.20 um 01:10 schrieb James Cook: > Thanks. I have not read through the details in the camp paper or the > Darcs V3 source code yet, but I think your explanation of conflictors > above, and the connection to the tree point of view, gives me some good > intuition to start with. > > I wonder if some of this could go on the wiki? Feel free to copy anything I write here to the wiki or add new pages. I am personally not too fond of wiki editing since (a) the formatting is too tedious and (b) the information usually gets out of date pretty soon (and nobody ever fixes it or removes obsolete information). >> 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. >> >> Cheers >> Ben > > I think the goal I described in my other email just now would end up > looking something like this, but with inverses on all the not-chosen > branches instead of a flag on the chosen branch. Let me know if you have something concrete that looks promising. 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
> In camp/darcs-3 (see src/Darcs/Patch/V3) a conflictor consists of three > parts (all prim patches are of course named): > > * The effect (a sequence of prim patches that negate all patches that we > conflict with, unless already negated by a previous conflictor), > > * a set of "contexted" (prim) patches (those we conflict with) > > * the (prim) patch itself (its "identity"), also as a contexted prim patch. > > Contexted patches should be visualized as forking off to the side, the > only part that is actually applied is the effect. The "contexted" here > means that the actual prim patch is prefixed by a sequence of prim > patches that re-context the original patch such that it applies at the > end of the conflictor. The camp paper visualizes this as (arrows point > rightward): > > / > (context+)conflicts > / > *--effect--*--(next patch)-- > \ > (context+)identity > \ > > In principle it would be possible to replace the contexted patches in > the set of conflicts with patch names, since it is guaranteed (by a > global invariant) that they must occur in the context (preceding > patches). The above representation makes conflictors self-contained with > respect to commute and merge i.e. we don't have to consult (or know) the > context. Also note that the "context" in a contexted patch usually > consists of negated patches (we have to walk backwards along the history > to reach the patch we reference). BTW, to keep them minimal we do use > cancellation of inverses in these "contexts" and also commute any patch > past (and then drop it) if possible. > > The only difficult thing here is to determine the proper side-conditions > when commuting and merging conflictors, so that the patch laws (mainly > permutivity) are satisfied. The source code in Darcs has a number of > comments to explain what is going on but may still be hard to follow for > someone unfamiliar with the code base. The last chapter of teh camp > paper explains each case in detail and motivates the various side > conditions with examples. > > The tree view can only be equivalent to this if we somehow store > additional information about which patches are in (direct) conflict with > each other. This is because given only the tree view we cannot > distinguish between a conflict (between say patches d and e) and its > (manual) resolution c (recorded after the conflict), since all three > patches start from the same "context" (node in the tree). In Darcs the > conflict resolution patch *depends* on the conflicted patches, but it > does not conflict with them. Also, whenever we have multiple conflicts > at the same point (say, a conflicts with b, which conflicts with c, but > a doesn't conflict directly with c), then we have to either store or > re-calculate that information because camp conflictors only store direct > conflicts and thus only considers these in the merge and commute rules. > > If we have this extra information (as, say, a finite map from patch > names to sets of patch names), and a way to look up the (unique, per > repo) patch representation plus its context (preceding patches) by name, > then we can reconstruct the conflictor representation from that. > Conversely, given a sequence of (possibly conflicted) patches, we can > reconstruct the tree by traversing "contexted" patches in a conflictor > backwards until we reach the patch they reference, then create a branch > of the tree at that point. (This is just a rough sketch but I hope you > get the idea). Thanks. I have not read through the details in the camp paper or the Darcs V3 source code yet, but I think your explanation of conflictors above, and the connection to the tree point of view, gives me some good intuition to start with. I wonder if some of this could go on the wiki? (Incidentally, I just discovered http://darcs.net/Ideas/Graphictors which seems related to this tree point of view.) > 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. > > Cheers > Ben I think the goal I described in my other email just now would end up looking something like this, but with inverses on all the not-chosen branches instead of a flag on the chosen branch. -- James ___ darcs-users mailing list
Re: [darcs-users] How to extend a patch theory to fully commute
(new email address) I'm hoping to do a little write-up of my idea for avoiding conflictors, after working out some details. (Maybe I'll discover it doesn't work out.) For now though I have waited long enough to answer your email so here goes... > I am going to discuss only d here, we need to do the same for e of > course. So we have a commuting square with d hanging off the bottom: > > Y >/ \ > c' b' > / \ > L R > \ / > b c >\ / > X--d--* > > Note that all arrows point rightward here (which is why we have to > (temporarily) invert c to c^ to make it point leftward). We can attach d > to either L, Y, or R, which gives us three possibilities to re-attach d > to the upper part of this diagram: > > * commute b';c^ past d to get Y--d'--* > * commute only c^ past d to get R--d'--* > * commute b past d to get L--d'--* > > Whatever we choose, we have to make sure these commutatations succeed. Thanks for the explanation. I think I had something different in mind for my version (a) of representing a tree with a sequence, but there are still problems. Representation (a) from my last email inserts the sequence d e'' between b and c: so the tree is represented as a b d e'' c, where (using your correction) merge(d\/e) = (e''/d'). This means that the context X in your diagram doesn't exist: the ending context of b and the starting context of c are different. We have: O--a--L--b--X1--d--Z--e''--X2--c--R I think with this representation there's no need for c^, but commuting b and c clearly does require some interaction with d and e''. Also, it's not clear to me how freely the branches of the tree could be re-ordered with this representation. Anyway, I am more interested in my version (b), which doesn't involve conflictors. > > I can see two ways to represent that tree with linear sequence of patches: > > > > (a) Create a conflictor e' by commuting (d^, e) <-> (e'', d'^), and > > represent the above tree as a b d e'' c. I guess this is the Darcs > > way. > > In principle yes, except that the conflictor cannot be defined in terms > of commutation alone, you need a primitive merge operation here i.e. > merge(d\/e)=(e'/\d') that satisfies the merge-commute law. This law > states that d;e' then commutes to e;d', which is required because we > want the result of merges to be independent of the order in which we > merge. (Remember that we regard sequences that differ only with respect > to re-ordering via commutation as equivalent.) That sounds right; thanks. > I agree that it is very tempting to linearize the tree representation > with a depth first traversal involving inverses, as you suggested: > > a;b;d;d^;e;e^;c. > > In fact, *if* the conflictor for e could be expressed as e'=(d^;e;e^), > then the above sequence would be identical to > > a;b;d;e';c > > Unfortunately this conflictor representation is too simple. It cannot > handle three-way conflicts correctly. The corresponding diagram involves > a commuting *cube* which is difficult to paint using ASCII graphics, but > easy with pencip and paper. The equations that must hold according to > the law of permutivity can then be directly read off the diagram. Doing > this is a very instructive exercise. Version (b) (linearizing with DFS) isn't supposed to involve conflictors at all. I think it would be better if I wait until I have a more careful write-up of how I imagine this working. > I'll respond to your further remarks in a separate message. > > We have veered off your initial idea quite a bit! I think it may still > be worth resurrecting your extended contexts and patches to see where > this gets us if we try to complete all proofs and flesh out the > requirements properly. Yes, I should probably return to that at some point. -- 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
On 2020-09-17 16:38, Ben Franksen wrote:
> Also note that the "context" in a contexted patch usually
> consists of negated patches (we have to walk backwards along the history
> to reach the patch we reference).
Sorry, this is wrong. In fact, all contexted patches contain only
positive prims. We even test this as a property (an invariant that holds
for all contexted patches contained in a V3 Conflictor, see
prop_ctxPositive in src/Darcs/Patch/V3/Contexted.hs and
harness/Darcs/Test/Patch/Properties/RepoPatchV3.hs).
I must admit that I was surprised by this. Apparently the only reason we
need Contexted patches at all is to cancel the negating effects of this
or previous conflictors involved in the same conflict. Indeed, all
occurrences of ctxAdd* in src/Darcs/Patch/V3/Core.hs take patches from
the effect of either the LHS ('r') or the RHS Conflictor ('s') as
argument, or some commuted variant of either. Inspection of the code
further reveals that indeed everywhere we add patches from the effect
without (re-)inverting them, we actually remove patches from the context
that we previously added during merge or commute.
On a more fundamental level, I think the set of contexted patches that a
conflictor (knows that it) conflicts with really corresponds to a set of
paths branching off the side in the tree view, which makes it pretty
obvious that they must all be positive.
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
>> Conflictors in Darcs can be seen as "internalizing" the relevant parts >> of the above tree structure /into/ the (conflicted) patch >> representation. This is the source of their complexity. What we gain >> form that is the possibility arrange all patches in a repo in a linear >> sequence where commutation is the only allowed (and required) form of >> sequence re-arrangement. > > Maybe it would be helpful to formalize this connection. If nothing > else, it might be an alternative way of explaining the Camp theory. > Actually, for all I know this is exactly how I'm supposed to think of > conflictors in Camp. I never fully understood that write-up; maybe I > should take another look. In camp/darcs-3 (see src/Darcs/Patch/V3) a conflictor consists of three parts (all prim patches are of course named): * The effect (a sequence of prim patches that negate all patches that we conflict with, unless already negated by a previous conflictor), * a set of "contexted" (prim) patches (those we conflict with) * the (prim) patch itself (its "identity"), also as a contexted prim patch. Contexted patches should be visualized as forking off to the side, the only part that is actually applied is the effect. The "contexted" here means that the actual prim patch is prefixed by a sequence of prim patches that re-context the original patch such that it applies at the end of the conflictor. The camp paper visualizes this as (arrows point rightward): / (context+)conflicts / *--effect--*--(next patch)-- \ (context+)identity \ In principle it would be possible to replace the contexted patches in the set of conflicts with patch names, since it is guaranteed (by a global invariant) that they must occur in the context (preceding patches). The above representation makes conflictors self-contained with respect to commute and merge i.e. we don't have to consult (or know) the context. Also note that the "context" in a contexted patch usually consists of negated patches (we have to walk backwards along the history to reach the patch we reference). BTW, to keep them minimal we do use cancellation of inverses in these "contexts" and also commute any patch past (and then drop it) if possible. The only difficult thing here is to determine the proper side-conditions when commuting and merging conflictors, so that the patch laws (mainly permutivity) are satisfied. The source code in Darcs has a number of comments to explain what is going on but may still be hard to follow for someone unfamiliar with the code base. The last chapter of teh camp paper explains each case in detail and motivates the various side conditions with examples. The tree view can only be equivalent to this if we somehow store additional information about which patches are in (direct) conflict with each other. This is because given only the tree view we cannot distinguish between a conflict (between say patches d and e) and its (manual) resolution c (recorded after the conflict), since all three patches start from the same "context" (node in the tree). In Darcs the conflict resolution patch *depends* on the conflicted patches, but it does not conflict with them. Also, whenever we have multiple conflicts at the same point (say, a conflicts with b, which conflicts with c, but a doesn't conflict directly with c), then we have to either store or re-calculate that information because camp conflictors only store direct conflicts and thus only considers these in the merge and commute rules. If we have this extra information (as, say, a finite map from patch names to sets of patch names), and a way to look up the (unique, per repo) patch representation plus its context (preceding patches) by name, then we can reconstruct the conflictor representation from that. Conversely, given a sequence of (possibly conflicted) patches, we can reconstruct the tree by traversing "contexted" patches in a conflictor backwards until we reach the patch they reference, then create a branch of the tree at that point. (This is just a rough sketch but I hope you get the idea). 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. 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
Am 17.09.20 um 01:51 schrieb James Cook:
>> So this can succeed only if c does not conflict with either of its
>> sibling cancelled branches, that is, if c^ commutes with all sequences
>> ("paths") in the cancelled branches, that is, all elements of {d, e;f,
>> e;g, e;h;i}. We then get
>>
>> a--b'-c'
>> |\
>>d' e'-f'
>> |\
>> g' h'-i'
>>
>> where we dropped the result of commuting c^ past.
>
> I think I'm missing a piece (or maybe you made a mistake).
>> Where does
> c^ come into the picture? Also, shouldn't b be unmodified?
I don't think so, see below.
> Let me go through this in a bit more detail, to explain what I mean
> and help myself make sure I understand.
>
> I'll simplify your example a bit to this:
>
> a--b--c
>|\
>d e
>
> Actually, I'd rather put the patches on the edges.
Yes, this notation is a lot clearer and less error prone. I should have
stuck to it.
> I guess the above tree becomes:
>
> a b c
> *--*--*--*
> |\
> d| \e
> * *
Yes. And the question I raised is: suppose b;c (taken in isolation)
commute to c';b', what are the side-conditions that allow us to make
them commute in the full picture?
Let me give a name to some of contexts involved:
a b c
*---L---X---R
|\
d| \e
| \
* *
Now, if we commute
b c
L---X---R
to
c' b'
L---Y---R
then this creates a new context Y that wasn't there before, whereas the
old context X has vanished. So *the least* we have to ensure is that we
can somehow transform d and e so that they can be attached somewhere to
the trunk a;c';b'.
I am going to discuss only d here, we need to do the same for e of
course. So we have a commuting square with d hanging off the bottom:
Y
/ \
c' b'
/ \
L R
\ /
b c
\ /
X--d--*
Note that all arrows point rightward here (which is why we have to
(temporarily) invert c to c^ to make it point leftward). We can attach d
to either L, Y, or R, which gives us three possibilities to re-attach d
to the upper part of this diagram:
* commute b';c^ past d to get Y--d'--*
* commute only c^ past d to get R--d'--*
* commute b past d to get L--d'--*
Whatever we choose, we have to make sure these commutatations succeed.
> I can see two ways to represent that tree with linear sequence of patches:
>
> (a) Create a conflictor e' by commuting (d^, e) <-> (e'', d'^), and
> represent the above tree as a b d e'' c. I guess this is the Darcs
> way.
In principle yes, except that the conflictor cannot be defined in terms
of commutation alone, you need a primitive merge operation here i.e.
merge(d\/e)=(e'/\d') that satisfies the merge-commute law. This law
states that d;e' then commutes to e;d', which is required because we
want the result of merges to be independent of the order in which we
merge. (Remember that we regard sequences that differ only with respect
to re-ordering via commutation as equivalent.)
> (b) a b d d^ e e^ c. This follows my idea of handling conflicts by
> cancelling out everything involved in the conflict.
>
> Now, we want to rearrange it to:
>
> a b c'
> *--*--*--*
> |\
>d'| \e'
> * *
>
> In version (a), that just means re-ordering d e'' c to c' d' e'. In
> version (b), it means reordering d d^ e e^ c to c' d' d'^ e' e'^. Does
> that all sound correct?
I think you misunderstood the point I was trying to make. I hope my
above explanations made that clearer.
I agree that it is very tempting to linearize the tree representation
with a depth first traversal involving inverses, as you suggested:
a;b;d;d^;e;e^;c.
In fact, *if* the conflictor for e could be expressed as e'=(d^;e;e^),
then the above sequence would be identical to
a;b;d;e';c
Unfortunately this conflictor representation is too simple. It cannot
handle three-way conflicts correctly. The corresponding diagram involves
a commuting *cube* which is difficult to paint using ASCII graphics, but
easy with pencip and paper. The equations that must hold according to
the law of permutivity can then be directly read off the diagram. Doing
this is a very instructive exercise.
I'll respond to your further remarks in a separate message.
We have veered off your initial idea quite a bit! I think it may still
be worth resurrecting your extended contexts and patches to see where
this gets us if we try to complete all proofs and flesh out the
requirements properly.
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
> So this can succeed only if c does not conflict with either of its
> sibling cancelled branches, that is, if c^ commutes with all sequences
> ("paths") in the cancelled branches, that is, all elements of {d, e;f,
> e;g, e;h;i}. We then get
>
> a--b'-c'
> |\
>d' e'-f'
> |\
> g' h'-i'
>
> where we dropped the result of commuting c^ past.
I think I'm missing a piece (or maybe you made a mistake). Where does
c^ come into the picture? Also, shouldn't b be unmodified?
Let me go through this in a bit more detail, to explain what I mean
and help myself make sure I understand.
I'll simplify your example a bit to this:
a--b--c
|\
d e
Actually, I'd rather put the patches on the edges. I guess the above
tree becomes:
a b c
*--*--*--*
|\
d| \e
* *
I can see two ways to represent that tree with linear sequence of patches:
(a) Create a conflictor e' by commuting (d^, e) <-> (e'', d'^), and
represent the above tree as a b d e'' c. I guess this is the Darcs
way.
(b) a b d d^ e e^ c. This follows my idea of handling conflicts by
cancelling out everything involved in the conflict.
Now, we want to rearrange it to:
a b c'
*--*--*--*
|\
d'| \e'
* *
In version (a), that just means re-ordering d e'' c to c' d' e'. In
version (b), it means reordering d d^ e e^ c to c' d' d'^ e' e'^. Does
that all sound correct?
> Note that we did employ inversion of the patch c here, but it is now
> apparent that it is only needed temporarily to move the conflicted
> branches to a new context.
>
> I think this theory is completely equivalent to that of Darcs in the
> sense that all operations have the same semantics. However, we can no
> longer represent the set of patches in a linear sequence, so this would
> have to have quite a different UI.
I wouldn't be surprised, except note that I found two interpretations
(a) and (b) above. (I didn't realize that until I began writing this
email.)
I wonder if the (b) interpretation allows some other applications of
inverses, other than conflict resolution. For example, you can go
through the same motions if there's only one branch in the "conflict"
(e.g. take my simplified example above but without the "e" branch).
This is nonsensical for actual conflict resolution (with just one
patch, there can't be a conflict), but maybe appending the sequence
d^c could mean c is an "amendment" to patch d.
> Whether that helps in your quest for a theory with unrestricted
> commutation is hard to say. The side conditions we have to impose on
> whether we are allowed to commute b;c to b';c' do have a certain
> similarity to how your "re-arrangement" of sequences depends on the context.
>
> Conflictors in Darcs can be seen as "internalizing" the relevant parts
> of the above tree structure /into/ the (conflicted) patch
> representation. This is the source of their complexity. What we gain
> form that is the possibility arrange all patches in a repo in a linear
> sequence where commutation is the only allowed (and required) form of
> sequence re-arrangement.
Maybe it would be helpful to formalize this connection. If nothing
else, it might be an alternative way of explaining the Camp theory.
Actually, for all I know this is exactly how I'm supposed to think of
conflictors in Camp. I never fully understood that write-up; maybe I
should take another look.
> It *may* be that the tree representation is more efficient, however, so
> I think it might be worth exploring this region of the design space.
Thanks, this email was helpful. Besides efficiency, I wonder if the
tree point of view is easier to understand when the conflict is
complex. Or, without touching any implementation or UI, I wonder if it
could just be useful as an alternative way of explaining how
conflictors work.
> 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
Hi James
I think I mentioned that inverses in patch theory always confuse me. So
I may be talking nonsense here.
My current thinking is this:
When we add names to primitive patches, we implicitly make the theory
asymmetric in the sense that /new/ patches can enter the scene only as
positive patches: any patch you record starts out as a positive one. The
only way to get a negative patch is to have the VCS implicitly negate a
positive patch to cancel it, which is done (only) when it detects that
the patch conflicts with another (positive) one.
Can we get by without the notion of inversion for named patches?
Perhaps. A conflicted repo could look like a tree, with conflicted
branches hanging off the side:
a--b--c
|\
d e--f
|\
g h--i
Here, only the top sequence a;b;c is actually applied. All other patches
are implicitly "negated" or "cancelled" because they conflict. Any patch
can occur at most once in the tree.
Since c is in the trunk i.e. applied, it must be the case that it either
does not conflict with any of the cancelled branches, or it has been
recorded after the conflict (i.e. as a manual resolution).
We now have to answer the question: how does the picture look if we
commute b;c to c';b' (assuming b;c does indeed commute)? This can only
succeed if we find a way to move the cancelled branches to a new
context, since the context "between b and c" no longer exists in the trunk.
So this can succeed only if c does not conflict with either of its
sibling cancelled branches, that is, if c^ commutes with all sequences
("paths") in the cancelled branches, that is, all elements of {d, e;f,
e;g, e;h;i}. We then get
a--b'-c'
|\
d' e'-f'
|\
g' h'-i'
where we dropped the result of commuting c^ past.
Note that we did employ inversion of the patch c here, but it is now
apparent that it is only needed temporarily to move the conflicted
branches to a new context.
I think this theory is completely equivalent to that of Darcs in the
sense that all operations have the same semantics. However, we can no
longer represent the set of patches in a linear sequence, so this would
have to have quite a different UI.
Whether that helps in your quest for a theory with unrestricted
commutation is hard to say. The side conditions we have to impose on
whether we are allowed to commute b;c to b';c' do have a certain
similarity to how your "re-arrangement" of sequences depends on the context.
Conflictors in Darcs can be seen as "internalizing" the relevant parts
of the above tree structure /into/ the (conflicted) patch
representation. This is the source of their complexity. What we gain
form that is the possibility arrange all patches in a repo in a linear
sequence where commutation is the only allowed (and required) form of
sequence re-arrangement.
It *may* be that the tree representation is more efficient, however, so
I think it might be worth exploring this region of the design space.
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
> > Oops, I didn't pay enough attention to your concrete example. > > > > Did you mean b = hunk f 1 [1a,2,3] [1b,2b,3b]? (I'm guessing hunk f n > > [u,v,w] [x,y,z] means lines n..n+2 of file f start out as [u,v,w] and > > end up as [x,y,z]; is that right?) > > Yes to both, sorry I messed up the example. For reference, here is the > fixed example in full: > > a=hunk f 1 [1] [1a] > b=hunk f 1 [1a,2,3] [1b,2b,3b] > c=hunk f 3 [3] [3c] > > > Then yes, I guess the order b;b^;c;a is not possible. > > > > I really want this to work, though, > > May I ask why? I mean, really, this is what commutation of patches is > all about: to determine if we /can/ re-arrange the internals of patches > in such a way that they make sense in a different context and in such a > way that the patch laws hold. My dream is to be able to do away with conflictor patches, or any kind of "extended patches", and instead just use a primitive patch theory + inverses to back out of conflicts. Conflictors, or my own "extended patches", seem complicated and it would be interesting if we can just completely get rid of them. I suspect this can be done with a bit more flexibility in how patch sequences are rearranged. As a concrete example, let's use your patches a, b, c above. (I'm sticking with patch names for this example, so e.g. I won't change a to a' if the patch gets rewritten.) Consider: 1. Alice's and Bob's repositories both start out with just patch a. 2. Alice, in her repository, creates patch b. Alice now has a;b. 3. Meanwhile, Bob, in his repository, creates patch c. Bob now has a;c. 4. Now Alice pulls from Bob, and there is a conflict. I propose to handle the conflict by setting Alice's repository to a;b;b^;c;c^, and put uncommitted conflict markers in the working directory. The conflict could just as well be represented as a;c;c^;b;b^, but a;b;b^;c;c^ can't be commuted to a;c;c^;b;b^ because, e.g., c^;b don't commute. Now that I've written this out, I'm not sure it's actually necessary to be able to go between a;b;b^;c;c^ and a;c;c^;b;b^. It seems strange to not allow it though. Another thought: I'm not sure why I ended up talking about inserting/removing b;b^ as being a legal rearrangement. Maybe what I really need is a "cycle swap" operation that lets me change b;b^;c;c^ to c;c^;b;b^, or in general C;D to D;C for any cycles C and D. > > so now I wonder what happens if we > > just accept the situation: even though c can be rearranged to b;b^;c, > > The point is that you can /not/ do that. Yes, the /effect/ of b;b^;c is > the same as that of c, that is, you can apply both to the same tree and > get the same result. But with respect to commutation they are not > equivalent. > > > and a;c can be rearranged to c;a > > Remember that in the general commutation may result in a different pair > c';a'. (In my example above a=a' and c=c', but this is a special case.) > > > it turns out we can't combine the > > two to rearrange a;c to b;b^;c;a. > > This means "rearrangement" is not permutative. Permutivity is essential > for proving that merging is order-independent. This is *the* key feature > that distinguishes Darcs from e.g. git. How are you defining permutivity? My understanding is based on Jacobson's inverse semigroups paper. I think permutivity means that if there are two different sequences of commute operations that result in the same overall permutation of patches, then it doesn't matter which sequence of operations you apply: you'll end up with the same new patch sequence either way. I guess you have a stronger definition in mind, where the available operations don't change depending on context. Despite your example, I think two things could be guaranteed: * The available /commute/ operations don't depend on the context. I.e. if a;b can be commuted to some b';a', then any other a'';b'' with the same names can still be commuted to some b''';a'''. (Since I'm not changing the commute relation (I'm using "rearrange" for my new relation) there's simply no reason this would be violated.) * I think my weaker understanding of permutivity can be fully satisfied. In fact, I think there is no conflict between my notion of "rearrangement" and the definition of "patch universe" from my latex writeup*, so any property that follows from that definition could still be satisfied, including, for example, that any two patches with the same starting context and the same name are equal. *https://www.falsifian.org/a/xxOw/misc.pdf / https://hub.darcs.net/falsifian/misc-pub/browse/patch_theory/misc.tex > > I guess it's kind of ugly that changing the context can change what > > rearrangements are possible: > > So far, patch theory has been designed precisely to avoid that, which is > why in Darcs we allow re-arrangement of a sequence only via commutation. > > > in this case, the rearrangement c -> > > b;b^;c may be possible or not depending on whether a patch named "a" > > has been applied. This is cause to be suspicious, but is
Re: [darcs-users] How to extend a patch theory to fully commute
Am 08.09.20 um 21:47 schrieb James Cook: In your case, for two adjacent /sequences/ A;B, and equivalences A~A', B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose you have patches a;b;b^;c, where none of the adjacent pairs commute. You'd have to show that this implies that a;c commutes neither (taking e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A counter example consists of 3 hunks a, b, c, where a and b overlap, b and c overlap, but a and c do not overlap. More concretely, take the initial state as file f=[1,2,3] and a=hunk f 1 [1] [1a] b=hunk f 1 [1,2,3] [1b,2b,3b] c=hunk f 3 [3] [3c] >>> >>> I'm still not sure I understand the problem. I agree that in your >>> example, it's possible to commute [a] with [c] but not [a] with >>> [b;b^;c]. But it is possible to "rearrange" a;b;b^;c into b;b^;c;a if >>> "rearrange" is defined broadly enough to allow the following three >>> steps: a;b;b^;c -> a;c -> c;a -> b;b^;c;a. >> >> Commutation means that we may have to re-arrange the /content/ of the >> patches we commute, such that they make sense in their new context. You >> abstracted that part away here. If we re-add it, the sequence becomes: >> >> a;b;b^;c -> a;c -> c';a' -> b';b'^;c';a' >> >> But what is the new b'? It should be clear that, in general, it cannot >> be the same as b: if b depends on a (which is what we assumed), then >> that means that b makes no sense without having a before it. >> >> Take the above three hunk patches and tell me how b' should be defined >> such that the resulting sequence b';b'^;c';a' makes sense. > > Oops, I didn't pay enough attention to your concrete example. > > Did you mean b = hunk f 1 [1a,2,3] [1b,2b,3b]? (I'm guessing hunk f n > [u,v,w] [x,y,z] means lines n..n+2 of file f start out as [u,v,w] and > end up as [x,y,z]; is that right?) Yes to both, sorry I messed up the example. For reference, here is the fixed example in full: a=hunk f 1 [1] [1a] b=hunk f 1 [1a,2,3] [1b,2b,3b] c=hunk f 3 [3] [3c] > Then yes, I guess the order b;b^;c;a is not possible. > > I really want this to work, though, May I ask why? I mean, really, this is what commutation of patches is all about: to determine if we /can/ re-arrange the internals of patches in such a way that they make sense in a different context and in such a way that the patch laws hold. > so now I wonder what happens if we > just accept the situation: even though c can be rearranged to b;b^;c, The point is that you can /not/ do that. Yes, the /effect/ of b;b^;c is the same as that of c, that is, you can apply both to the same tree and get the same result. But with respect to commutation they are not equivalent. > and a;c can be rearranged to c;a Remember that in the general commutation may result in a different pair c';a'. (In my example above a=a' and c=c', but this is a special case.) > it turns out we can't combine the > two to rearrange a;c to b;b^;c;a. This means "rearrangement" is not permutative. Permutivity is essential for proving that merging is order-independent. This is *the* key feature that distinguishes Darcs from e.g. git. > I guess it's kind of ugly that changing the context can change what > rearrangements are possible: So far, patch theory has been designed precisely to avoid that, which is why in Darcs we allow re-arrangement of a sequence only via commutation. > in this case, the rearrangement c -> > b;b^;c may be possible or not depending on whether a patch named "a" > has been applied. This is cause to be suspicious, but is there an > obvious reason it's unworkable? I can't answer this question in any exact or precise way. My gut feeling is that it's going to be an ugly mess, but I haven't tried it so I may be wrong. I should perhaps also point out that there are some operations in Darcs for which the context is important; for instance, conflict markup in general requires access to the complete context. 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
> >> In your case, for two adjacent /sequences/ A;B, and equivalences A~A', > >> B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose > >> you have patches a;b;b^;c, where none of the adjacent pairs commute. > >> You'd have to show that this implies that a;c commutes neither (taking > >> e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A > >> counter example consists of 3 hunks a, b, c, where a and b overlap, b > >> and c overlap, but a and c do not overlap. More concretely, take the > >> initial state as file f=[1,2,3] and > >> > >> a=hunk f 1 [1] [1a] > >> b=hunk f 1 [1,2,3] [1b,2b,3b] > >> c=hunk f 3 [3] [3c] > > > > I'm still not sure I understand the problem. I agree that in your > > example, it's possible to commute [a] with [c] but not [a] with > > [b;b^;c]. But it is possible to "rearrange" a;b;b^;c into b;b^;c;a if > > "rearrange" is defined broadly enough to allow the following three > > steps: a;b;b^;c -> a;c -> c;a -> b;b^;c;a. > > Commutation means that we may have to re-arrange the /content/ of the > patches we commute, such that they make sense in their new context. You > abstracted that part away here. If we re-add it, the sequence becomes: > > a;b;b^;c -> a;c -> c';a' -> b';b'^;c';a' > > But what is the new b'? It should be clear that, in general, it cannot > be the same as b: if b depends on a (which is what we assumed), then > that means that b makes no sense without having a before it. > > Take the above three hunk patches and tell me how b' should be defined > such that the resulting sequence b';b'^;c';a' makes sense. Oops, I didn't pay enough attention to your concrete example. Did you mean b = hunk f 1 [1a,2,3] [1b,2b,3b]? (I'm guessing hunk f n [u,v,w] [x,y,z] means lines n..n+2 of file f start out as [u,v,w] and end up as [x,y,z]; is that right?) Then yes, I guess the order b;b^;c;a is not possible. I really want this to work, though, so now I wonder what happens if we just accept the situation: even though c can be rearranged to b;b^;c, and a;c can be rearranged to c;a, it turns out we can't combine the two to rearrange a;c to b;b^;c;a. I guess it's kind of ugly that changing the context can change what rearrangements are possible: in this case, the rearrangement c -> b;b^;c may be possible or not depending on whether a patch named "a" has been applied. This is cause to be suspicious, but is there an obvious reason it's unworkable? 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
Am 08.09.20 um 17:29 schrieb James Cook:
> On Thu, 3 Sep 2020 at 14:24, Ben Franksen wrote:
>>
> If I wanted to implement it, I think it would just become this:
>
> * A repository consists of two things:
> * A sequence S of primitive patches with distinct names, starting at
> O, with no inverses (i.e. only positive names).
> * A set of names, called "tombstones", representing "deleted"
> patches. These names don't appear in S.
The problem I see here is that this looses the start (or ending) state
of the "deleted" patches. And you don't even remember their content,
just their name. But even supposing you remember a start state and the
patch representation of every deleted patch, this will still mess up
your commutation. Because deleting inverse pairs AA^ from the main
sequence basically means the same as stating that such a pair commutes
with any other patch, which is clearly wrong
>>>
>>> Yes, I forgot that the repo needs to remember the content of those
>>> "deleted" patches. E.g. someone might later obliterate A^, or someone
>>> might want to pull A and not A^ to another repo; or someone might
>>> simply want to see the content of A and A^ in the output of "darcs
>>> changes -v". So, tombstones as names only clearly isn't enough.
>>>
>>> I'm a bit fuzzy about the problem with commutation that you raise.
>>> Yes, one way to delete AA^ would be to commute them all the way to the
>>> end of the sequence and then drop them. But what would go wrong if we
>>> simply declare that whenever you have a sequence B;A;A^;C you're free
>>> to simply replace it with B;C (and vice versa) as an operation
>>> distinct from commuting?
>>
>> Well, if you allow to replace parts of a sequence, then this means that
>> for the purpose of your theory you regard the two versions of the
>> sequence as equivalent. But this works out only if you can prove that
>> the equivalence is structure preserving.
>>
>> Take the integers Z as an example, and for some fixed positive integer
>> p, define n ~ m iff n%p = m%p ('%' means modulo; so this tells us that
>> we can "drop" multiples of p from any number). This equivalence
>> preserves the arithmetic structure, which is why we can regard Z_p as a
>> Ring by doing the arithmetic on an arbitrary representative of the
>> equivalence class. But it does not preserve the order structure of the
>> integers.
>>
>> In your case, for two adjacent /sequences/ A;B, and equivalences A~A',
>> B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose
>> you have patches a;b;b^;c, where none of the adjacent pairs commute.
>> You'd have to show that this implies that a;c commutes neither (taking
>> e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A
>> counter example consists of 3 hunks a, b, c, where a and b overlap, b
>> and c overlap, but a and c do not overlap. More concretely, take the
>> initial state as file f=[1,2,3] and
>>
>> a=hunk f 1 [1] [1a]
>> b=hunk f 1 [1,2,3] [1b,2b,3b]
>> c=hunk f 3 [3] [3c]
>
> I'm still not sure I understand the problem. I agree that in your
> example, it's possible to commute [a] with [c] but not [a] with
> [b;b^;c]. But it is possible to "rearrange" a;b;b^;c into b;b^;c;a if
> "rearrange" is defined broadly enough to allow the following three
> steps: a;b;b^;c -> a;c -> c;a -> b;b^;c;a.
Commutation means that we may have to re-arrange the /content/ of the
patches we commute, such that they make sense in their new context. You
abstracted that part away here. If we re-add it, the sequence becomes:
a;b;b^;c -> a;c -> c';a' -> b';b'^;c';a'
But what is the new b'? It should be clear that, in general, it cannot
be the same as b: if b depends on a (which is what we assumed), then
that means that b makes no sense without having a before it.
Take the above three hunk patches and tell me how b' should be defined
such that the resulting sequence b';b'^;c';a' makes sense.
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
On Thu, 3 Sep 2020 at 14:24, Ben Franksen wrote:
>
> >>> If I wanted to implement it, I think it would just become this:
> >>>
> >>> * A repository consists of two things:
> >>> * A sequence S of primitive patches with distinct names, starting at
> >>> O, with no inverses (i.e. only positive names).
> >>> * A set of names, called "tombstones", representing "deleted"
> >>> patches. These names don't appear in S.
> >>
> >> The problem I see here is that this looses the start (or ending) state
> >> of the "deleted" patches. And you don't even remember their content,
> >> just their name. But even supposing you remember a start state and the
> >> patch representation of every deleted patch, this will still mess up
> >> your commutation. Because deleting inverse pairs AA^ from the main
> >> sequence basically means the same as stating that such a pair commutes
> >> with any other patch, which is clearly wrong
> >
> > Yes, I forgot that the repo needs to remember the content of those
> > "deleted" patches. E.g. someone might later obliterate A^, or someone
> > might want to pull A and not A^ to another repo; or someone might
> > simply want to see the content of A and A^ in the output of "darcs
> > changes -v". So, tombstones as names only clearly isn't enough.
> >
> > I'm a bit fuzzy about the problem with commutation that you raise.
> > Yes, one way to delete AA^ would be to commute them all the way to the
> > end of the sequence and then drop them. But what would go wrong if we
> > simply declare that whenever you have a sequence B;A;A^;C you're free
> > to simply replace it with B;C (and vice versa) as an operation
> > distinct from commuting?
>
> Well, if you allow to replace parts of a sequence, then this means that
> for the purpose of your theory you regard the two versions of the
> sequence as equivalent. But this works out only if you can prove that
> the equivalence is structure preserving.
>
> Take the integers Z as an example, and for some fixed positive integer
> p, define n ~ m iff n%p = m%p ('%' means modulo; so this tells us that
> we can "drop" multiples of p from any number). This equivalence
> preserves the arithmetic structure, which is why we can regard Z_p as a
> Ring by doing the arithmetic on an arbitrary representative of the
> equivalence class. But it does not preserve the order structure of the
> integers.
>
> In your case, for two adjacent /sequences/ A;B, and equivalences A~A',
> B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose
> you have patches a;b;b^;c, where none of the adjacent pairs commute.
> You'd have to show that this implies that a;c commutes neither (taking
> e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A
> counter example consists of 3 hunks a, b, c, where a and b overlap, b
> and c overlap, but a and c do not overlap. More concretely, take the
> initial state as file f=[1,2,3] and
>
> a=hunk f 1 [1] [1a]
> b=hunk f 1 [1,2,3] [1b,2b,3b]
> c=hunk f 3 [3] [3c]
>
> Cheers
> Ben
Sorry again for the slow reply.
I'm still not sure I understand the problem. I agree that in your
example, it's possible to commute [a] with [c] but not [a] with
[b;b^;c]. But it is possible to "rearrange" a;b;b^;c into b;b^;c;a if
"rearrange" is defined broadly enough to allow the following three
steps: a;b;b^;c -> a;c -> c;a -> b;b^;c;a.
So, I guess I am proposing to think in terms of "rearranging", not
"commuting", where "rearranging" means a sequence of the following
three kinds of operation: (a) commute; (b) introduce a patch and its
inverse together anywhere in the squence (c;a -> b;b^;c;a); and
eliminating an inverse pair (a;b;b^;c -> a;c). Or, maybe it would need
some other definition. It might simply mean finding *any* other path
with the same start and end contexts; I'm not sure.
I guess I should back this up by showing this notion of
"rearrangement" satisfies some properties? E.g. given a patch sequence
p1;p2;...;pn and a subset of those patches that someone wants to
obliterate, darcs currently has an algorithm to move that subset to
the end iff it's possible. I guess I should show that there's an
efficient algorithm to either "rearrange" the sequence so that the
subset to be obliterated is at the end, or determine that no such
rearrangement is possible.
I still haven't done the homework I assigned myself (the three "next
steps" from my Sept 1 email).
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
>>> If I wanted to implement it, I think it would just become this:
>>>
>>> * A repository consists of two things:
>>> * A sequence S of primitive patches with distinct names, starting at
>>> O, with no inverses (i.e. only positive names).
>>> * A set of names, called "tombstones", representing "deleted"
>>> patches. These names don't appear in S.
>>
>> The problem I see here is that this looses the start (or ending) state
>> of the "deleted" patches. And you don't even remember their content,
>> just their name. But even supposing you remember a start state and the
>> patch representation of every deleted patch, this will still mess up
>> your commutation. Because deleting inverse pairs AA^ from the main
>> sequence basically means the same as stating that such a pair commutes
>> with any other patch, which is clearly wrong
>
> Yes, I forgot that the repo needs to remember the content of those
> "deleted" patches. E.g. someone might later obliterate A^, or someone
> might want to pull A and not A^ to another repo; or someone might
> simply want to see the content of A and A^ in the output of "darcs
> changes -v". So, tombstones as names only clearly isn't enough.
>
> I'm a bit fuzzy about the problem with commutation that you raise.
> Yes, one way to delete AA^ would be to commute them all the way to the
> end of the sequence and then drop them. But what would go wrong if we
> simply declare that whenever you have a sequence B;A;A^;C you're free
> to simply replace it with B;C (and vice versa) as an operation
> distinct from commuting?
Well, if you allow to replace parts of a sequence, then this means that
for the purpose of your theory you regard the two versions of the
sequence as equivalent. But this works out only if you can prove that
the equivalence is structure preserving.
Take the integers Z as an example, and for some fixed positive integer
p, define n ~ m iff n%p = m%p ('%' means modulo; so this tells us that
we can "drop" multiples of p from any number). This equivalence
preserves the arithmetic structure, which is why we can regard Z_p as a
Ring by doing the arithmetic on an arbitrary representative of the
equivalence class. But it does not preserve the order structure of the
integers.
In your case, for two adjacent /sequences/ A;B, and equivalences A~A',
B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose
you have patches a;b;b^;c, where none of the adjacent pairs commute.
You'd have to show that this implies that a;c commutes neither (taking
e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A
counter example consists of 3 hunks a, b, c, where a and b overlap, b
and c overlap, but a and c do not overlap. More concretely, take the
initial state as file f=[1,2,3] and
a=hunk f 1 [1] [1a]
b=hunk f 1 [1,2,3] [1b,2b,3b]
c=hunk f 3 [3] [3c]
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
> One a minor note, your patch universe definition is not suitable for > extended patches as defined in Darcs: For these, the square commute law > (which you call rotation, perhaps a better name) does not hold. Though > to be fair, a while ago we have stopped treating them as invertible in > the first place, so nowadays we couldn't even /state/ that property for > them. (This remark is largely irrelevant for your theory.) If you don't have inverses, you could replace the balance-respecting law with: If two patch sequences have the same name signature, then [the two sequences have the same starting context] iff [the two sequences have the same ending context]. I think some desirable properties will still hold, but I haven't thought it through carefully. (Here, names don't have signs so a "name signature" is just a multiset of names without signs.) When I wrote the Latex write-up, I first tried to start with this definition, and make addinv be an operation on patch universes: so, you can start with a fully-functional patch universe without inverses, then add inverses on top of it. Then I tried to prove the balance-respecting property as a consequence, but realized it doesn't follow. So I abandoned that approach. (I don't remember offhand why I thought the balance-respecting property is important.) 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
On Wed, 19 Aug 2020 at 11:52, Ben Franksen wrote: > Am 19.08.20 um 11:44 schrieb Ben Franksen: > > The fact that your patches have no "content" is of of course a result of > > starting out with "enriched" contexts. As you note in 2.2 > > Interpretation, your contexts can *not* in general be understood simply > > as "working tree states": the mapping from contexts to states is not > > injective. It is not yet clear to me if that will have consequences when > > it comes to implementing your theory. > > Let me elaborate this point a bit. > > Your theory assume the existence of contexts as a "set". That doesn't > give us any hint as to how these contexts should be represented in a > concrete implementation. If we start out with some notion of prim patch > (such as the one in Darcs), then these exist as concrete representations > of state changes as data. But we know that states do not correspond 1:1 > to contexts. The simplest example involves duplicate prim patches p, q, > such that name(p)/=name(q), but repr(p)==repr(q). Assuming a starting > context X for both p and q, the ending context is different, even though > the end state is the same. More interesting examples involve things like > (remove f; add g) versus (move f g). > > The question now is: how can we arrive at a suitable definition (i.e. > representation) of context, given such a concrete definition of prim > patches and states? > > The answer, in Darcs at least, is to not define contexts. Contexts > aren't represented at runtime at all. Instead, in our code contexts > exist only formally at the type level. > > Your definition of context address may require that we have a way to > reify contexts as data. A natural way of arriving at a suitable > definition is to go backwards from patches: identify a context with the > set of all patch sequences that start at the empty state and that differ > only by commutation. At this point I am always tempted to say "and > elimination of inverses"; indeed your definition of a patch universe > implies that a sequence [a;b;b^] really has the same start and end > context as the plain [a]. But with respect to commutation this doesn't > seem right: [a;c] may commute to some [c';a'], but [a;b;b^;c] may not, > because e.g. [a;b] may not commute. Every time I think about this I am > getting head-aches. I cannot reconcile these two points of view. > > Anyway, assuming we have sorted this out somehow, I am still having > doubts about reifying contexts, because the definition as an equivalence > class of sequences does not easily map to an efficient representation. > > Cheers > Ben Sorry again for the long pause. It's not clear to me right now exactly what properties a representation of contexts would need to have. Your example about [a b b^; c] not commuting is troubling but I need to think about where exactly that would cause a problem, if anywhere. I find my definition of context address as signed name multiset kind of tantalizing. (The one that's currently in the pdf as Definition 10, but that I promptly disavowed in a follow-up email after sending the link. Fix the starting context to be the empty state; then a context is just represented by the names of patches you follow to get there.) The lack of an actual sequence probably causes problems but I don't yet know what those problems are. On the other hand it's an easy data structure to work with. I have three next steps in mind right now (hopefully I'll find the time): 1. Move things from my original hms_patchfinder writeup to the new Latex document, and rework the proofs to use the new definition of patch universe. The goal is to increase confidence that in theory, at least, patch universes can be extended to fully commute in the way I originally described. 2. Look for ways to simplify; e.g. can an extended context address just be a signed name multiset? (I'm always tempted to skip to this step, but I think I should make myself start with step 1.) 3. Think more about my implementation idea from a previous email, wherein a repository is just a primitive patch sequence plus tombstones. I think I never answered your response, so here's an answer: > > If I wanted to implement it, I think it would just become this: > > > > * A repository consists of two things: > > * A sequence S of primitive patches with distinct names, starting at > > O, with no inverses (i.e. only positive names). > > * A set of names, called "tombstones", representing "deleted" > > patches. These names don't appear in S. > > The problem I see here is that this looses the start (or ending) state > of the "deleted" patches. And you don't even remember their content, > just their name. But even supposing you remember a start state and the > patch representation of every deleted patch, this will still mess up > your commutation. Because deleting inverse pairs AA^ from the main > sequence basically means the same as stating that such a pair commutes > with any other patch, which is clearly
Re: [darcs-users] How to extend a patch theory to fully commute
Am 19.08.20 um 11:44 schrieb Ben Franksen: > The fact that your patches have no "content" is of of course a result of > starting out with "enriched" contexts. As you note in 2.2 > Interpretation, your contexts can *not* in general be understood simply > as "working tree states": the mapping from contexts to states is not > injective. It is not yet clear to me if that will have consequences when > it comes to implementing your theory. Let me elaborate this point a bit. Your theory assume the existence of contexts as a "set". That doesn't give us any hint as to how these contexts should be represented in a concrete implementation. If we start out with some notion of prim patch (such as the one in Darcs), then these exist as concrete representations of state changes as data. But we know that states do not correspond 1:1 to contexts. The simplest example involves duplicate prim patches p, q, such that name(p)/=name(q), but repr(p)==repr(q). Assuming a starting context X for both p and q, the ending context is different, even though the end state is the same. More interesting examples involve things like (remove f; add g) versus (move f g). The question now is: how can we arrive at a suitable definition (i.e. representation) of context, given such a concrete definition of prim patches and states? The answer, in Darcs at least, is to not define contexts. Contexts aren't represented at runtime at all. Instead, in our code contexts exist only formally at the type level. Your definition of context address may require that we have a way to reify contexts as data. A natural way of arriving at a suitable definition is to go backwards from patches: identify a context with the set of all patch sequences that start at the empty state and that differ only by commutation. At this point I am always tempted to say "and elimination of inverses"; indeed your definition of a patch universe implies that a sequence [a;b;b^] really has the same start and end context as the plain [a]. But with respect to commutation this doesn't seem right: [a;c] may commute to some [c';a'], but [a;b;b^;c] may not, because e.g. [a;b] may not commute. Every time I think about this I am getting head-aches. I cannot reconcile these two points of view. Anyway, assuming we have sorted this out somehow, I am still having doubts about reifying contexts, because the definition as an equivalence class of sequences does not easily map to an efficient representation. 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
Am 19.08.20 um 03:26 schrieb James Cook: >> I changed the definition of Context >> Address to work better with my new "patch universe" definition, but I >> think it amounts to the same thing. > > Thinking about it more, I'm not sure my new definition of Context > Address is a good one, since I've been finding it hard to associate a > primitive context with every minimal context address in the same way I > did in the hms_patchfinder writeup. > > It might be better to stick closer to my original definition of > context address. The proof should still be about as easy as the one in > the linked pdf: if a context address points to two different contexts, > you can conclude the contexts are equal because a name-balanced path > connects. them. I agree; your new definition is too general: you allow arbitrary signed name multisets; whereas your original definition started out with a valid sequence. 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
Am 18.08.20 um 22:42 schrieb James Cook: > Okay, I wrote something up: https://www.falsifian.org/a/xxOw/misc.pdf I like it. Especially the part where you define commutation in terms of the balance-respecting property. This is very elegant. It confirms what I have long since suspected, namely that the whole theory becomes simpler and more regular if we concentrate on patch /sequences/ instead of individual patches. The fact that your patches have no "content" is of of course a result of starting out with "enriched" contexts. As you note in 2.2 Interpretation, your contexts can *not* in general be understood simply as "working tree states": the mapping from contexts to states is not injective. It is not yet clear to me if that will have consequences when it comes to implementing your theory. One a minor note, your patch universe definition is not suitable for extended patches as defined in Darcs: For these, the square commute law (which you call rotation, perhaps a better name) does not hold. Though to be fair, a while ago we have stopped treating them as invertible in the first place, so nowadays we couldn't even /state/ that property for them. (This remark is largely irrelevant for your theory.) I'll comment on the new context address definition in another message. 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
> I changed the definition of Context > Address to work better with my new "patch universe" definition, but I > think it amounts to the same thing. Thinking about it more, I'm not sure my new definition of Context Address is a good one, since I've been finding it hard to associate a primitive context with every minimal context address in the same way I did in the hms_patchfinder writeup. It might be better to stick closer to my original definition of context address. The proof should still be about as easy as the one in the linked pdf: if a context address points to two different contexts, you can conclude the contexts are equal because a name-balanced path connects. them. 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
> >> A good way to see if your definition holds up is to see whether you can > >> prove your > >> > >> Conjecture 1: Every context address points to at most one context. > > > > Sure, that's a nice goal. > > > > I think I will start a latex file, try to define what a patch theory > > is and what context address is for a given patch theory, then try to > > prove Conjecture 1. > > > > I know of two places with formal definitions of "patch theory": J. > > Jacobson's Inverse Semigroups paper and the Camp theory document. I'll > > probably start a new definition with just the properties I find I > > need. (A patch theory is a (possibly infinite) directed graph, with a > > "commute" relation and a "name" function, satisfying the following > > axioms: ...) > > I think the approach you took so far is better: find out bit by bit what > you need, instead of trying to come up with a full formal definition up > front. Okay, I wrote something up: https://www.falsifian.org/a/xxOw/misc.pdf ; Latex source at https://hub.darcs.net/falsifian/misc-pub/browse/patch_theory/misc.tex This covers just the definition of "patch universe" and Conjecture 1 (every context address points to at most one context). I ended up going in an unconventional direction: patch commuting is not fundamental to my definition of a "patch universe" but instead can be derived from it (proofs in Sec 2.3). There are two reasons I went this way: (a) it's simple: a patch universe is a just graph with names on the edges, and the rule that if you follow a sequence of edges where the names "balance out", you end up back where you started. (b) It makes my Conjecture 1 easy to prove. (In other words: I cheated. Hopefully I haven't optimised for this use case too narrowly...) See Section 3. I changed the definition of Context Address to work better with my new "patch universe" definition, but I think it amounts to the same thing. The terminology is kind of dense right now and the write-up could benefit from examples. If you prefer, you could wait until I've done some more work on it. (I might discover bugs in the meantime too.) 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
Am 13.08.20 um 19:54 schrieb James Cook:
> Question: is there a good place to read about how "darcs pull" works?
I am not aware of anything that you could read. What happens is
basically this:
We read the _darcs/hashed_inventory of both the local and remote repo.
These give us the latest know clean tag and the patches after that and
possibly (the hash of) a parent inventory, for both repos. The patch
list contains the name and hash of a patch; I use "name" here as a
short-hand for the full PatchInfo, including the hidden random number
that serves to make names unique; the hash here refers to the
representation of the patch i.e. the patch itself can be accessed as
_darcs/patches/ or _darcs/inventories/ for inventories. As I
explained in an earlier message, we now try to find the latest common
tag (by name, in the above sense). When we found that we have a point
from which two sequences of patches fork off. We are now commuting every
patch common to both sequences to before the forking point, ending up
with two sequences starting at the same state with no patch in common.
These two steps are done by taggedIntersection and findCommonAndUncommon
in src/Darcs/Patch/Depends.
These are then merged as described in the camp paper, I think in chapter
8; or you could read the code of merge2FL in src/Darcs/Patch/Ident.hs
and the instance Merge (FL p) in src/Darcs/Patch/Merge.hs. Once we
calculated the merge, we can concatenate one half of it with our repo
and all that remains to do is applying the new patches to our pristine
state (and marking conflicts in the working tree). A detailed
description of the algorithm and most of the details I glossed over here
can be found in src/Darcs/Repository/Merge.hs.
>>> I was concerned that adding just that one new kind of equivalence
>>> might not be enough.
>>
>> I think you first need a more precise definition of what inversion means
>> for primitive patches. For instance, if inverse patches come into play,
>> your definition of context addresses runs into problems because now the
>> same patch can occur multiple times in a sequence, so you can no longer
>> uniquely refer to the patches in a sequence by their names. For
>> instance, if you split A;A^;A;B after the A^, your patch name sets will
>> be X={A,A^} and Y={A,B}, where A now occurs in both X and Y.
>
> I wonder whether I could forbid a context address from containing more
> than one patch with the same name. I will think about whether that
> would cause problems with the rest of the theory.
This might be possible.
>> A good way to see if your definition holds up is to see whether you can
>> prove your
>>
>> Conjecture 1: Every context address points to at most one context.
>
> Sure, that's a nice goal.
>
> I think I will start a latex file, try to define what a patch theory
> is and what context address is for a given patch theory, then try to
> prove Conjecture 1.
>
> I know of two places with formal definitions of "patch theory": J.
> Jacobson's Inverse Semigroups paper and the Camp theory document. I'll
> probably start a new definition with just the properties I find I
> need. (A patch theory is a (possibly infinite) directed graph, with a
> "commute" relation and a "name" function, satisfying the following
> axioms: ...)
I think the approach you took so far is better: find out bit by bit what
you need, instead of trying to come up with a full formal definition up
front.
> Also, to make sure I don't lose track: last month you described a way
> to model patch sequences with inverse categories:
> https://lists.osuosl.org/pipermail/darcs-users/2020-July/027451.html .
> If I understood that right, that doesn't include a definition of what
> a patch theory is
I think there is not one patch theory but many. The theory for primitive
patches is certainly different from that for "extended" patches as you
call them. For instance, in Darcs extended patches are not invertible,
while prim patches certainly are. OTOH extended patches have a total
merge operation which prim patches don't have, in general.
I think the most important law that should be valid for all patch
theories is permutivity. Given inverses, commute and (partial i.e.
clean) merge for prim patches can be defined in terms of each other. My
point of view is that patches /represent/ partial 1:1 functions on the
set of possible states (source trees). Equivalent patch sequences (i.e.
sequences that differ only in the order of patches) must represent the
same function on states.
Patch names complicate that picture a bit: they add structure that is
independent of the original "meaning" of a patch as a partial 1:1 function.
> Here's another direction I want to think about: I suspect that when it
> comes time to implement this, all you really need are two things:
> primitive patches, and "tombstones" representing patches that have
> been deleted (if you like, representing pairs AA^ that have cancelled
> each other out). In particular, you don't need any
Re: [darcs-users] How to extend a patch theory to fully commute
Question: is there a good place to read about how "darcs pull" works?
You mentioned hashed inventories in an earlier email; I guess I could
look at the darcs source keeping that in mind. (I've been thinking
about reading some of the source code anyway).
It's relevant to the last part of this email.
> > I was concerned that adding just that one new kind of equivalence
> > might not be enough.
>
> I think you first need a more precise definition of what inversion means
> for primitive patches. For instance, if inverse patches come into play,
> your definition of context addresses runs into problems because now the
> same patch can occur multiple times in a sequence, so you can no longer
> uniquely refer to the patches in a sequence by their names. For
> instance, if you split A;A^;A;B after the A^, your patch name sets will
> be X={A,A^} and Y={A,B}, where A now occurs in both X and Y.
I wonder whether I could forbid a context address from containing more
than one patch with the same name. I will think about whether that
would cause problems with the rest of the theory.
> A good way to see if your definition holds up is to see whether you can
> prove your
>
> Conjecture 1: Every context address points to at most one context.
Sure, that's a nice goal.
I think I will start a latex file, try to define what a patch theory
is and what context address is for a given patch theory, then try to
prove Conjecture 1.
I know of two places with formal definitions of "patch theory": J.
Jacobson's Inverse Semigroups paper and the Camp theory document. I'll
probably start a new definition with just the properties I find I
need. (A patch theory is a (possibly infinite) directed graph, with a
"commute" relation and a "name" function, satisfying the following
axioms: ...)
Also, to make sure I don't lose track: last month you described a way
to model patch sequences with inverse categories:
https://lists.osuosl.org/pipermail/darcs-users/2020-July/027451.html .
If I understood that right, that doesn't include a definition of what
a patch theory is, and is designed for reasoning about extending patch
theories. I don't know whether or not the point of view is useful for
Conjecture 1; I guess it comes into play more when extending the patch
theory.
--
--
Here's another direction I want to think about: I suspect that when it
comes time to implement this, all you really need are two things:
primitive patches, and "tombstones" representing patches that have
been deleted (if you like, representing pairs AA^ that have cancelled
each other out). In particular, you don't need any kind of
"conflictor" or "extended patch" or anything like that.
To be a bit more precise: suppose we define a "repository" to be an
extended patch sequence as defined in my HMS Patchfinder theory,
starting at the primitive context O. Resolving conflicts means
adjusting the repository so that the ending context is also primitive.
I conjecture that an extended patch sequence that starts and ends at
primitive contexts is just a sequence of primitive patches with some
extra loops (involving patches that cancel each other out).
If I wanted to implement it, I think it would just become this:
* A repository consists of two things:
* A sequence S of primitive patches with distinct names, starting at
O, with no inverses (i.e. only positive names).
* A set of names, called "tombstones", representing "deleted"
patches. These names don't appear in S.
* Pulling from another repository works as follows:
a) First, add the tombstones from the other repo to this repo's set
of tombstones. If any of the patches in this repo's S now have
tombstones, delete them from S. If any patches in S depended on those,
delete them as well, and add them to the set of tombstones, and add
conflict markers into the working directory.
b) Next, pull in the primitive patches from the other repo. This
works just like it does in darcs (1 2 or 3; as far as I know it
doesn't matter) except for two differences. First, any time darcs
would have introduced a conflictor patch, we instead delete all
patches involved in the conflict, add tombstones for the conflicting
patches, and add conflict markers in the working directory as usual.
Second, we have to deal with patches in the remote repo that depend on
patches deleted in this repo; this should work something like step a).
Of course, a lot of detail would need to be worked out. I don't have a
complete understanding of how "darcs pull" works but hope that this
could be implemented in a similar way.
The point is that maybe the whole theory isn't really needed, and I
could instead just focus on the parts needed to get the above working.
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
Am 08.08.20 um 22:51 schrieb James Cook:
>> Why are you so hung up on this tree / cycle thing? What is wrong about
>> your original context addresses and patch (sequence) adresses? If
>> efficiency is the concern, we are talking about a factor of two here.
>> This is irrelevant. For the theory you need to get the asymptotics
>> right, the rest are implementation details.
>
> Sorry for the long silence; I was distracted by other things. I'm
> hoping to take some time soon to review the thread and respond to
> parts of it.
Hi James,
it's goo to hear from you again. I was pretty busy myself, so nothing lost.
> To respond to your quoted question above: I was concerned my
> "canonical context address" representation of patches might not make
> enough things equivalent, i.e. distinguish things that shouldn't be
> distinguished.
>
> This came up when we talked about inverses: we need to add some rule
> in order to guarantee that the starting context of A^ equals the
> ending context of A.
>
> When I raised the concern, you suggested* "with inversion added, every
> context address has two minimal forms: forward and backward, and these
> denote the same extended context."
I did.
> I was concerned that adding just that one new kind of equivalence
> might not be enough.
I think you first need a more precise definition of what inversion means
for primitive patches. For instance, if inverse patches come into play,
your definition of context addresses runs into problems because now the
same patch can occur multiple times in a sequence, so you can no longer
uniquely refer to the patches in a sequence by their names. For
instance, if you split A;A^;A;B after the A^, your patch name sets will
be X={A,A^} and Y={A,B}, where A now occurs in both X and Y.
A good way to see if your definition holds up is to see whether you can
prove your
Conjecture 1: Every context address points to at most one context.
> But I didn't think it through carefully. Honestly
> I thought the cycle representation seemed kind of neat, but I guess I
> don't really have a justification for it right now.
I agree that it'd be nice to have a canonical representation, but I
think it is too early to search for it. You first need a firm
understanding of how context addresses behave in the presence of inverse
patches.
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
> > and whether it's okay to restrict S to be tree-like during the > > intermediate steps. It is probably simpler to just drop the cycle > > version and think only of trees, but I want to make sure I understand > > how the primitive patch theory's commuting rules turn into tree > > transformations. > > Why are you so hung up on this tree / cycle thing? What is wrong about > your original context addresses and patch (sequence) adresses? If > efficiency is the concern, we are talking about a factor of two here. > This is irrelevant. For the theory you need to get the asymptotics > right, the rest are implementation details. > > Cheers > Ben Sorry for the long silence; I was distracted by other things. I'm hoping to take some time soon to review the thread and respond to parts of it. To respond to your quoted question above: I was concerned my "canonical context address" representation of patches might not make enough things equivalent, i.e. distinguish things that shouldn't be distinguished. This came up when we talked about inverses: we need to add some rule in order to guarantee that the starting context of A^ equals the ending context of A. When I raised the concern, you suggested* "with inversion added, every context address has two minimal forms: forward and backward, and these denote the same extended context." I was concerned that adding just that one new kind of equivalence might not be enough. But I didn't think it through carefully. Honestly I thought the cycle representation seemed kind of neat, but I guess I don't really have a justification for it right now. *https://lists.osuosl.org/pipermail/darcs-users/2020-July/027434.html 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
Definition: A category X is said to be an inverse category whenever, for each arrow f : A -> B in X, there exists a unique f^ : B -> A in X such that ff^f = f and f^ff^ = f^. (I write composition as juxtaposition without an operator.) Given a universe of extended invertible patches, define a category as follows: * Objects are the extended contexts. * Arrows are (finite) sequences of extended patches, with the identifications pp^p = p and p^pp^ = p^ and pq=q'p' whenever commute(pq)=q'p' (which I also write as pq<->q'p') * Composition is concatenation. * Identities are empty sequences (denoted id_X : X -> X). In other words, we start with the free inverse category on the graph of extended patches and factor that by the equivalence relation that identifies sequences that differ only up to commutation. This is also an inverse category because commutation respects inversion i.e. pq<->q'p' <=> q^p^<->q'^p'^, which is a consequence of the square-commute law. Some remarks: * I think in your theory you need to show that the squere-commute law holds for extended patches (assuming it does for primitive patches). * This construction works only if extended patches do have inverses i.e. not for Darcs. In Darcs we give up invertibility when we extend primitive patches, and instead define merging as a new "primitive" (sorry for overloading the term) operation. In your definition of extended patches invertibility falls out quite naturally, and indeed is required because you define merging in terms of inversion as in the primitive theory. So our arrows are equivalence classes of extended patch sequences. The construction is such that given a sequence P=...pp^p... we can reduce that to an equivalent smaller P'=...p... and I think it should be possible to show that all members of a class that are minimal (with respect to the length of the sequence) have the property that any patch they contain occurs at most once. (Formally: if names(P) is the set of names of patches occurring in P, then |names(P)|=length(P).) It is assumed that the primitive patch graph has a distinguished node (context) O that denotes an empty state with no files or directories. Since primitive contexts are embedded in extended contexts, we could then define a repository as an arrow in the inverse category of extended patch sequences that starts at O. 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
Am 06.07.20 um 19:37 schrieb James Cook: > On Mon, 6 Jul 2020 at 10:29, Ben Franksen wrote: >> Am 05.07.20 um 20:36 schrieb Ben Franksen: >>> Am 04.07.20 um 23:59 schrieb James Cook: > I think that whenever a sequence of patches starts and ends at a > primitive context (e.g. this is true of an unconflicted repository) > you can re-order the patches so that they are all primitive. I should add: this probably requires allowing new permutations that weren't in the primitive theory. E.g. you can commute anything past A;A^, even if you couldn't in the primitive theory. This might mean some algorithms need to be changed; hopefully these changes will not make them less efficient. >>> >>> You need to be very careful here. A commutes past B;B^ only if A at >>> least commutes with B. Otherwise you move B to an invalid context in >>> which it can no longer be applied. >> >> To put this point in a wider perspective: >> >> From the viewpoint of inverse semigroup theory, inverse pairs are >> idempotent elements. While idempotents always commute with each other >> (i.e. XX^YY^=YY^XX^ for all X,Y), it is not in general true that XX^Y=YXX^. >> >> From the corresponding viewpoint of groupoid theory (which I prefer >> because it is, more or less, a "statically typed" version of inverse >> semigroups), for any X:x->x', XX^=id_x is the identity /at state x/. If >> y is a different state and Y:x->y, then Y=XX^Y:x->y is well-typed, and >> it is true that XX^YY^=YY^XX^:x->x. But the composition YXX^ is not >> well-typed and thus undefined! > > Yes, I should have been more careful about what can commute past what. > The email I sent just now suggests you can commute any two cycles; > maybe that's enough. > > Also, thanks for the reference to groupoids. I have been wondering how > to think about a primitive patch theory and just had a vague sense > it's sort of like a category. For a category you need composition and identities. Patches themselves have neither so they do not form a category. But patch /sequences/ do. (This is well-known construction: the category of all paths in a directed graph, there's a name for that but I forgot it.) If you add inverses and allow them to cancel in a sequence, then this becomes a groupoid. But remember that we must not allow cancellation of inverses for repositories, or in general for sequences involving conflicted merges. So unfortunately groupoids can serve as a framework only for primitive patches. For extended patches we need something weaker; I am currently exploring if perhaps inverse categories fit the bill. (I haven't found much literature on inverse categories, though.) 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
Am 06.07.20 um 19:33 schrieb James Cook:
>> I guess you want to avoid proper cycles, i.e. cycles other than those of
>> the form patches;patches^, but that's just an intuition.
>
> A;A^;B;B^;C;C^ isn't a proper cycle in that sense but may be useful to
> be able to have if you're merging or have merged non-commuting patches
> A, B, C.
>
> It may be good to avoid non-tree-like cycles like B';A';B^;A^.
That's what I meant to say.
> Maybe it's possible to avoid creating them in the first place.
Yes, I think your constructions so far do that.
> As a motivating example, suppose A;B;C don't commute at all, and we
> have the context address (A;B;C, {B}, {A, C}). (I'm leaving out the
> first two parts of the tuple, since as you point out they are
> implied.)
(Unless the sequence is empty)
> From the old point of view, we can delete C because it's in Y and
> already at the end of the sequence, producing the minimal context
> address (A;B, {B}, {A}).
>
> But another way to do it is this: first extend the sequence to the
> cycle A;B;C;C^;B^;A^. The address becomes (A;B;C;C^;B^;A^, {A^, B,
> C^}, {A, B^, C}).
Ah, yes. I forgot your idea to turn all context addresses into cycles.
But then you also have to redefine the two sets X and Y. Because in a
cycle there is no "before" or "after. (Edit: after reading to the end I
get the idea, but I don't find it very elegant.)
> (See below for some intuition about why I extended
> the sets X and Y in that way.) Then, we eliminate C;C^ as a
> consecutive pair. However, we have to be careful: if we just always
> eliminated consecutive primitive patches we'd end up with an empty
> sequence.
>
> Viewed as a tree, this is going to look like the following: there is a
> line A;B;C with three edges, and each edge has an orientation. The "A"
> edge points left (away from B and C), the "B" edge points right, and
> the "C" edge points left. We delete the C edge following a general
> rule that leaves can be deleted when they are connected by edges that
> point to the rest of the tree.
>
> o--<--o-->--o--<--o
> A B C
>
> o--<--o-->--o
> A B
>
> If all of a tree's edges point inward toward one "root" node, then all
> the edges can be deleted and the tree just represents the primitive
> context at its root.
I am confused about this redefinition of the orientation of arrows. In
my book, a patch already has an orientation. In your example this would be
o-->--o-->--o-->--o
A B C
You explain this direction thing below but I don't like the overloading
of the direction concept here.
> Here's how it could work in general.
>
> * A context address is a tuple (S, X, Y), where S is a "tree-like"
> cycle. (I used to use the notation (Qi) but that's getting annoying.)
Yup. The traditional math notation for sequences sucks badly. I like to
keep use of indices to the barest minimum possible (sometimes you need
them but most times you don't).
> (Tree-like means following the cycle is the same as doing depth-first
> search on some tree, or in other words, for every patch P with
> start/end contexts a and b in S, the patch P^ appears with start/end
> contexts b and a.)
I really like the notation established in category theory where, in
analogy to the tradition notation for functions, you just say
P : a -> b and P^ : b -> a
It is patently clear from this notation that P^ cannot have any other
type. So your explanation of "tree-like" appears vacuous to me.
> * (S, X, Y) can be thought of as a rooted tree with an orientation on
> each edge, with the following transformation.
>
> Put the root at the start/end context of the cycle S.
A cycle has no start/end context. Okay, in your notation it has one,
because you start out with a sequence of prim patches. I'll try to
accept that and go on.
> Draw a tree by
> following all the patches in S. Each edge of the tree consists of a
> pair P and P^. Orient the edge as pointing away from the root if P is
> in X and P^ is in Y, and toward the root if P is in Y and P^ is in X.
Okay, here comes the new arrow orientation. I still don';t think this is
a good idea. Can't you avoid this?
> * We can rotate S to produce an equivalent address. When we rotate,
> patches move between X and Y. Specifically, if patch P is moved from
> the start to end of S or vice versa, P and P^ switch places. In other
> words, (P;S', {P} U X', {P^} U Y') becomes (P;S', {P^} U X', {P} U
> Y').
>
> From the tree point of view, this preserves the orientation of all the
> edges. All that happens is the root moves.
>
> So, we can forget where the root was and just think of it as an unrooted tree.
>
> * If P;P^ appear consecutively in S, and P is in Y and P^ is in X,
> then they can be eliminated. Similarly if P^;P appears, P^ is in Y and
> P is in X.
>
> In other words, we can delete a leaf from a tree so long as its edge
> points away from the leaf.
Very well. What I don't get yet is what you gain from all that.
> * More
Re: [darcs-users] How to extend a patch theory to fully commute
On Mon, 6 Jul 2020 at 10:29, Ben Franksen wrote: > Am 05.07.20 um 20:36 schrieb Ben Franksen: > > Am 04.07.20 um 23:59 schrieb James Cook: > >>> I think that whenever a sequence of patches starts and ends at a > >>> primitive context (e.g. this is true of an unconflicted repository) > >>> you can re-order the patches so that they are all primitive. > >> > >> I should add: this probably requires allowing new permutations that > >> weren't in the primitive theory. E.g. you can commute anything past > >> A;A^, even if you couldn't in the primitive theory. This might mean > >> some algorithms need to be changed; hopefully these changes will not > >> make them less efficient. > > > > You need to be very careful here. A commutes past B;B^ only if A at > > least commutes with B. Otherwise you move B to an invalid context in > > which it can no longer be applied. > > To put this point in a wider perspective: > > From the viewpoint of inverse semigroup theory, inverse pairs are > idempotent elements. While idempotents always commute with each other > (i.e. XX^YY^=YY^XX^ for all X,Y), it is not in general true that XX^Y=YXX^. > > From the corresponding viewpoint of groupoid theory (which I prefer > because it is, more or less, a "statically typed" version of inverse > semigroups), for any X:x->x', XX^=id_x is the identity /at state x/. If > y is a different state and Y:x->y, then Y=XX^Y:x->y is well-typed, and > it is true that XX^YY^=YY^XX^:x->x. But the composition YXX^ is not > well-typed and thus undefined! Yes, I should have been more careful about what can commute past what. The email I sent just now suggests you can commute any two cycles; maybe that's enough. Also, thanks for the reference to groupoids. I have been wondering how to think about a primitive patch theory and just had a vague sense it's sort of like a category. 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
> > I don't know how darcs figures out what patches need to be pulled,
> > especially if R1 is lazy.
>
> Don't let yourself be confused by lazy repos.
>
> Conceptually, darcs reads the complete remote repo, figures out the
> common patches, commutes all uncommon patches in both repos to the end,
> and then runs the actual merge algorithm only on the remaining
> (uncommon) sequences. The camp paper has a chapter with many nice
> pictures where this is explained in detail.
>
> In reality we almost never need to read the full remote repo. This is
> because the order of patches in a repositories is stored in so called
> inventories. An inventory is a file that lists patch names along with
> the content hash of each patch. Inventories can be nested and are stored
> hashed, too (i.e. the file name is equal to the content hash). This
> makes it easy to compare two repos efficiently to find the latest point
> at which they diverge. We only need to download remote inventories until
> we find an identical one in our local repo. Since cloning preserves
> inventories and operations deep inside a repo are uncommon (and also
> pretty expensive), this search usually terminates quickly.
>
> Lazy repos are missing only patches listed in closed inventories, which
> means that pulling from a lazy repo normally works fine. However, it
> /can/ fail if we actually need access to such a patch (e.g. in order to
> commute it) and we cannot download it from any source repository listed
> in the local repo (which includes the per-user cache).
Thanks, that was informative. Maybe it could be put on the wiki
somewhere? (I tried to check if something like that already is, but
darcs.net seems to be down.)
> > given a tree, you can turn it into a patch
> > sequence address by doing a depth first search (record positive
> > patches as you go deeper into the tree, and negative patches when you
> > return back upward). I suspect the other direction can be done too,
> > after you extend (Qi) in a patch sequence address to be a cycle and
> > then do some commuting, but I'm not sure.
>
> I guess you want to avoid proper cycles, i.e. cycles other than those of
> the form patches;patches^, but that's just an intuition.
A;A^;B;B^;C;C^ isn't a proper cycle in that sense but may be useful to
be able to have if you're merging or have merged non-commuting patches
A, B, C.
It may be good to avoid non-tree-like cycles like B';A';B^;A^. Maybe
it's possible to avoid creating them in the first place.
> > An advantage of the patch sequence address representation over the
> > tree representation is that I find it easier to think about how
> > commuting can modify a cycle. With the tree representation you'd want
> > to push conflicts as far down the tree as possible. This should be
> > related to the minimality condition for patch sequence addresses, but
> > I haven't wrapped my head around it.
>
> Well, suppose you have primitive A;(B\/C) where neither A;B nor A;C
> commute. If we start with the sequence A;B;B^;C and want to minimize
> that to A;C, we have no other choice but to cancel inverses. Otherwise
> you'd have the situation that A;B;B^;C and A;C are not equivalent as
> context addresses. (I am not using the full notation here because
> primitive contexts are implicit in primitive patches, assuming all
> patches are well-typed, and the sets X and Y are irrelevant here.)
That's an interesting point. Thinking about it more, I think it
completely replaces the existing minimality rule if we switch to a
tree or cycle representation. (You need to be a little careful about
what exactly you can eliminate once everything is a cycle.)
Here are my thoughts so far...
As a motivating example, suppose A;B;C don't commute at all, and we
have the context address (A;B;C, {B}, {A, C}). (I'm leaving out the
first two parts of the tuple, since as you point out they are
implied.)
>From the old point of view, we can delete C because it's in Y and
already at the end of the sequence, producing the minimal context
address (A;B, {B}, {A}).
But another way to do it is this: first extend the sequence to the
cycle A;B;C;C^;B^;A^. The address becomes (A;B;C;C^;B^;A^, {A^, B,
C^}, {A, B^, C}). (See below for some intuition about why I extended
the sets X and Y in that way.) Then, we eliminate C;C^ as a
consecutive pair. However, we have to be careful: if we just always
eliminated consecutive primitive patches we'd end up with an empty
sequence.
Viewed as a tree, this is going to look like the following: there is a
line A;B;C with three edges, and each edge has an orientation. The "A"
edge points left (away from B and C), the "B" edge points right, and
the "C" edge points left. We delete the C edge following a general
rule that leaves can be deleted when they are connected by edges that
point to the rest of the tree.
o--<--o-->--o--<--o
A B C
o--<--o-->--o
A B
If all of a tree's edges point inward toward one "root" node, then all
the edges
Re: [darcs-users] How to extend a patch theory to fully commute
Am 05.07.20 um 20:36 schrieb Ben Franksen: > Am 04.07.20 um 23:59 schrieb James Cook: >>> I think that whenever a sequence of patches starts and ends at a >>> primitive context (e.g. this is true of an unconflicted repository) >>> you can re-order the patches so that they are all primitive. >> >> I should add: this probably requires allowing new permutations that >> weren't in the primitive theory. E.g. you can commute anything past >> A;A^, even if you couldn't in the primitive theory. This might mean >> some algorithms need to be changed; hopefully these changes will not >> make them less efficient. > > You need to be very careful here. A commutes past B;B^ only if A at > least commutes with B. Otherwise you move B to an invalid context in > which it can no longer be applied. To put this point in a wider perspective: >From the viewpoint of inverse semigroup theory, inverse pairs are idempotent elements. While idempotents always commute with each other (i.e. XX^YY^=YY^XX^ for all X,Y), it is not in general true that XX^Y=YXX^. >From the corresponding viewpoint of groupoid theory (which I prefer because it is, more or less, a "statically typed" version of inverse semigroups), for any X:x->x', XX^=id_x is the identity /at state x/. If y is a different state and Y:x->y, then Y=XX^Y:x->y is well-typed, and it is true that XX^YY^=YY^XX^:x->x. But the composition YXX^ is not well-typed and thus undefined! 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
Am 04.07.20 um 23:59 schrieb James Cook: >> I think that whenever a sequence of patches starts and ends at a >> primitive context (e.g. this is true of an unconflicted repository) >> you can re-order the patches so that they are all primitive. > > I should add: this probably requires allowing new permutations that > weren't in the primitive theory. E.g. you can commute anything past > A;A^, even if you couldn't in the primitive theory. This might mean > some algorithms need to be changed; hopefully these changes will not > make them less efficient. You need to be very careful here. A commutes past B;B^ only if A at least commutes with B. Otherwise you move B to an invalid context in which it can no longer be applied. 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
Am 04.07.20 um 23:43 schrieb James Cook: > On Sat, 4 Jul 2020 at 09:59, Ben Franksen wrote: >> Am 04.07.20 um 00:10 schrieb James Cook: > I'd say this is a feature, not a bug. If you mark the conflict between A > and B as resolved, *without* recording a new patch, then this means you > are satisfied with the resolution that reverts both changes. There is no > reason why pulling C should conflict now. If, on the other hand, you are > not satisfied with this resolution, you may want record a "proper" > resolution, usually a mixture of A and B. This will then typically > conflict with C. >>> >>> That's a great point. I'm much less worried now. >> >> You should be, though. I think what I wrote above is nonsense. >> >> [...] > > I'm not sure I understand your concern right. Ah, forget it. My concern was about cancelling inverses. I am biased by my own theorizing about patches. I once thought that patch sequences should form a groupoid, which requires that we must always cancel inverses. This is apparently not what you are aiming at. However, I do think you need to cancel inverse in /addresses/ as part of the minimization process. > Let me try to step > through what I'd like to happen. > > Suppose the starting context is s and patches A and B conflict and > have ending contexts a and b. > > In repository R1, the user tries to merge A and B, sees conflict > markers, and records a conflict resolution. The conflict resolution > consists of A^, B^, and a new patch C which replaces A and B. The > repository now looks like this (after re-ordering a bit): > > s A a A^ s B b B^ s C c There is nothing wrong with that as long as you always keep all patches in the sequence and never annihilate inverses. > Now, suppose the user tries to pull from another repository R2 that > has just patch A. Here, it is very important that R1 "remember" that > the A\/B conflict was already resolved. Otherwise, it may treat C \/ A > as a new conflict. > > But can't we just observe that the name "A" is already present in R1, > and therefore there's no need to pull in A? Wouldn't that ensure that > we never again try to resolve a conflict involving A? Of course. If you keep "inverses" in the repo (i.e. don't cancel them), then you are now in a situation where you want to merge (A;A^;B;B^;C)\/(A). The common subsequence is (A) and the uncommon parts are (A^;B;B^;C)\/() and their merge is trivially ()/\(A^;B;B^;C). So the result is A;A^;B;B^;C i.e. equal to R1. > I don't know how darcs figures out what patches need to be pulled, > especially if R1 is lazy. Don't let yourself be confused by lazy repos. Conceptually, darcs reads the complete remote repo, figures out the common patches, commutes all uncommon patches in both repos to the end, and then runs the actual merge algorithm only on the remaining (uncommon) sequences. The camp paper has a chapter with many nice pictures where this is explained in detail. In reality we almost never need to read the full remote repo. This is because the order of patches in a repositories is stored in so called inventories. An inventory is a file that lists patch names along with the content hash of each patch. Inventories can be nested and are stored hashed, too (i.e. the file name is equal to the content hash). This makes it easy to compare two repos efficiently to find the latest point at which they diverge. We only need to download remote inventories until we find an identical one in our local repo. Since cloning preserves inventories and operations deep inside a repo are uncommon (and also pretty expensive), this search usually terminates quickly. Lazy repos are missing only patches listed in closed inventories, which means that pulling from a lazy repo normally works fine. However, it /can/ fail if we actually need access to such a patch (e.g. in order to commute it) and we cannot download it from any source repository listed in the local repo (which includes the per-user cache). > I suspect the current implementation might > need to be extended so that a repository stores a set of all names of > patches that have been cancelled out, i.e. the names of all patches A > such that both A and A^ are present. But this is speculative because I > don't know how that algorithm works. See above. You can add such a set as an optimization but the algorithm doesn't need it *if* you keep all patches in the sequence that represents the state of your repo. >> If you want to have proper inverses (for conflict resolution) and still >> remember all of the history, you must abandon the idea that a repo is a >> sequence of patches (or rather: an equivalence class of such sequences, >> module permutations). So your idea of phantom patches (a patch together >> with its tombstone) amounts to saying that a repo is not a sequence of >> patches, but a tree (with multiple dead branches), and to merge a patch >> means to merge it with all branches of the tree (you'll have to work out
Re: [darcs-users] How to extend a patch theory to fully commute
> I think that whenever a sequence of patches starts and ends at a > primitive context (e.g. this is true of an unconflicted repository) > you can re-order the patches so that they are all primitive. I should add: this probably requires allowing new permutations that weren't in the primitive theory. E.g. you can commute anything past A;A^, even if you couldn't in the primitive theory. This might mean some algorithms need to be changed; hopefully these changes will not make them less efficient. Maybe I should learn about the algorithms darcs currently uses to re-order patches as needed for operations like pull and obliterate. 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
On Sat, 4 Jul 2020 at 16:05, Ben Franksen wrote:
> Hi James
>
> It was an interesting journey through the sea of patches!
>
> I think your construction is sound. I have somewhat skimmed over the
> more complicated proofs, but I trust they contain no grave mistakes,
> given that your exposition is otherwise very careful and precise.
>
> > 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. The
> > starting context of a primitive patch is always a primitive context,
> > so it will be impossible to apply any primitive patches after a
> > conflict.
>
> I think the last sentence here shows a clear advantage of this kind of
> patch theory over that of darcs. In your theory it becomes patently
> clear when a repository is conflicted. In darcs this is more
> complicated: we regard a conflict as resolved if it cannot be commuted
> to the end, that is if another patch depends on the conflicted one.
>
> Another nice aspect of your theory is that extended (i.e. conflicted)
> commutation is defined symmetrically. That was of course the whole
> purpose, so I'd say you have achieved your goal.
>
> There remain lingering doubts about the efficiency of (some of) the
> operations. Perhaps these are unfounded.
>
> Cheers
> Ben
Thanks for taking the time to read it, and for all your comments,
corrections, and advice.
I do think efficiency is a concern. I think storing patches
individually using the "canonical patch address" representation should
be avoided whenever possible.
I may take a stab at a new write-up that incorporates the ideas we've discussed.
I am currently thinking along these lines:
I think that whenever a sequence of patches starts and ends at a
primitive context (e.g. this is true of an unconflicted repository)
you can re-order the patches so that they are all primitive. E.g. once
you've merged incompatible patches A\/B and added C to replace them,
the repository is simply A;A^;B;B^;C (like in my last email). Or a
better representation might just be the single patch C, together with
the set of tombstones {A, B}.
So, in some sense, this all might boil down to two things:
(a) An unconflicted repo is nothing more than a sequence of primitive
patches, possibly plus a set of tombstones. In other words, when there
are no conflicts, you don't need to store any patches outside the
primitive theory.
(b) Temporarily, while a conflict is unresolved, this theory provides
a way to represent the conflicted state using extended patches.
This doesn't mean efficiency won't be a concern, but it does make me optimistic.
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
On Sat, 4 Jul 2020 at 09:59, Ben Franksen wrote: > Am 04.07.20 um 00:10 schrieb James Cook: > >>> I'd say this is a feature, not a bug. If you mark the conflict between A > >>> and B as resolved, *without* recording a new patch, then this means you > >>> are satisfied with the resolution that reverts both changes. There is no > >>> reason why pulling C should conflict now. If, on the other hand, you are > >>> not satisfied with this resolution, you may want record a "proper" > >>> resolution, usually a mixture of A and B. This will then typically > >>> conflict with C. > > > > That's a great point. I'm much less worried now. > > You should be, though. I think what I wrote above is nonsense. > > This works only if inverses really cancel each other which means > applying the inverse is the same as obliterate. That means your repo > will not be able to remember that you once had a conflict between A and > B. I guess this is not what you want. > > But if inverses don't cancel then they aren't proper inverses in the > sense that you arrive at exactly the same context you started with. In > particular, you /cannot/ go back to the point you were before a > conflicted merge. > > Having proper inverses, or more generally a patch graph with cycles, is > more akin to time travel (not as in fantasy stories, but the physical > version i.e. time-like closed paths) than to a conventional journey that > visits the same destination but at a different time. > > In Darcs all patches in a repo have a positive name. You can obliterate > patches and start fresh (i.e. travel back in time) but that is unrelated > to conflicted merge which keeps all of the history. I'm not sure I understand your concern right. Let me try to step through what I'd like to happen. Suppose the starting context is s and patches A and B conflict and have ending contexts a and b. In repository R1, the user tries to merge A and B, sees conflict markers, and records a conflict resolution. The conflict resolution consists of A^, B^, and a new patch C which replaces A and B. The repository now looks like this (after re-ordering a bit): s A a A^ s B b B^ s C c Now, suppose the user tries to pull from another repository R2 that has just patch A. Here, it is very important that R1 "remember" that the A\/B conflict was already resolved. Otherwise, it may treat C \/ A as a new conflict. But can't we just observe that the name "A" is already present in R1, and therefore there's no need to pull in A? Wouldn't that ensure that we never again try to resolve a conflict involving A? I don't know how darcs figures out what patches need to be pulled, especially if R1 is lazy. I suspect the current implementation might need to be extended so that a repository stores a set of all names of patches that have been cancelled out, i.e. the names of all patches A such that both A and A^ are present. But this is speculative because I don't know how that algorithm works. > If you want to have proper inverses (for conflict resolution) and still > remember all of the history, you must abandon the idea that a repo is a > sequence of patches (or rather: an equivalence class of such sequences, > module permutations). So your idea of phantom patches (a patch together > with its tombstone) amounts to saying that a repo is not a sequence of > patches, but a tree (with multiple dead branches), and to merge a patch > means to merge it with all branches of the tree (you'll have to work out > what that means precisely). I had been thinking about representing a repo as a tree. I think there is a certain equivalence between trees and patch sequence addresses: given a tree, you can turn it into a patch sequence address by doing a depth first search (record positive patches as you go deeper into the tree, and negative patches when you return back upward). I suspect the other direction can be done too, after you extend (Qi) in a patch sequence address to be a cycle and then do some commuting, but I'm not sure. An advantage of the patch sequence address representation over the tree representation is that I find it easier to think about how commuting can modify a cycle. With the tree representation you'd want to push conflicts as far down the tree as possible. This should be related to the minimality condition for patch sequence addresses, but I haven't wrapped my head around it. 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
Hi James It was an interesting journey through the sea of patches! I think your construction is sound. I have somewhat skimmed over the more complicated proofs, but I trust they contain no grave mistakes, given that your exposition is otherwise very careful and precise. > 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. The > starting context of a primitive patch is always a primitive context, > so it will be impossible to apply any primitive patches after a > conflict. I think the last sentence here shows a clear advantage of this kind of patch theory over that of darcs. In your theory it becomes patently clear when a repository is conflicted. In darcs this is more complicated: we regard a conflict as resolved if it cannot be commuted to the end, that is if another patch depends on the conflicted one. Another nice aspect of your theory is that extended (i.e. conflicted) commutation is defined symmetrically. That was of course the whole purpose, so I'd say you have achieved your goal. There remain lingering doubts about the efficiency of (some of) the operations. Perhaps these are unfounded. 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
Am 01.07.20 um 18:45 schrieb James Cook: >> Just to check I understood the idea (up to this point): roughly >> speaking, you represent "unrepresentable" states by formally commuting >> patches. >> >> That is, if we regard the primitive states as vertices and primitive >> (named) patches as edges in a graph, then you extend the graph with new >> nodes and edges. > > That's exactly the intuition. > > If you had n patches that all commuted, this graph would be a > hypercube, i.e. the nodes are the 2^n subsets of patches and each edge > adds one patch. > > I think my theory always extends this graph exactly to that hypercube, > filling in exactly those nodes and edges that are missing. I haven't > thought carefully about that point of view so maybe that's not true. > >> The construction works by inductively taking any pair of incommutable >> patches (in sequence, i.e. with a common middle state) and then >> "formally" commuting it. The new node is represented as that pair of >> patches. Is that, essentially, the idea? > > Yes, that's exactly what happens when there are only two patches > involved and they don't commute. > >> It reminds me of the darcs-1 patch format, where a "merger" patch is >> defined as the ordered pair consisting of both conflicting patches. > > I think I read about darcs-1 conflictors a long time ago, so that > general idea has been on my mind for a while. Okay, I guess I'll need to read on, then. I wonder how you define commutation for the extended set of patches... 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
Am 04.07.20 um 00:10 schrieb James Cook: >>> I'd say this is a feature, not a bug. If you mark the conflict between A >>> and B as resolved, *without* recording a new patch, then this means you >>> are satisfied with the resolution that reverts both changes. There is no >>> reason why pulling C should conflict now. If, on the other hand, you are >>> not satisfied with this resolution, you may want record a "proper" >>> resolution, usually a mixture of A and B. This will then typically >>> conflict with C. > > That's a great point. I'm much less worried now. You should be, though. I think what I wrote above is nonsense. This works only if inverses really cancel each other which means applying the inverse is the same as obliterate. That means your repo will not be able to remember that you once had a conflict between A and B. I guess this is not what you want. But if inverses don't cancel then they aren't proper inverses in the sense that you arrive at exactly the same context you started with. In particular, you /cannot/ go back to the point you were before a conflicted merge. Having proper inverses, or more generally a patch graph with cycles, is more akin to time travel (not as in fantasy stories, but the physical version i.e. time-like closed paths) than to a conventional journey that visits the same destination but at a different time. In Darcs all patches in a repo have a positive name. You can obliterate patches and start fresh (i.e. travel back in time) but that is unrelated to conflicted merge which keeps all of the history. If you want to have proper inverses (for conflict resolution) and still remember all of the history, you must abandon the idea that a repo is a sequence of patches (or rather: an equivalence class of such sequences, module permutations). So your idea of phantom patches (a patch together with its tombstone) amounts to saying that a repo is not a sequence of patches, but a tree (with multiple dead branches), and to merge a patch means to merge it with all branches of the tree (you'll have to work out what that means precisely). 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
> > I'd say this is a feature, not a bug. If you mark the conflict between A > > and B as resolved, *without* recording a new patch, then this means you > > are satisfied with the resolution that reverts both changes. There is no > > reason why pulling C should conflict now. If, on the other hand, you are > > not satisfied with this resolution, you may want record a "proper" > > resolution, usually a mixture of A and B. This will then typically > > conflict with C. That's a great point. I'm much less worried now. > > That said, there is a problem here. To arrive at the default resolution > > (revert the conflicting prim patches) you add inverse patches to the > > repo. But what does "adding a patch to a repo" mean, precisely, if > > inverses are involved? Is a repo still a sequence of patches? Is A;A^;A > > the same as A? That would be bad because resolving a conflict would then > > be the same as obliterating the conflicting patches. So inverse pairs > > cannot simply be cancelled. > > An afterthought: what if you do not simply add the inverse for the > resolution, but instead record a new patch with the same effect as the > inverse? In other words, you add the inverse, but give it a new > (positive) name, so that it cannot cancel. Just an idea. I'll think about that idea. Here's another approach I'd been thinking about, which I'd held back because I thought the thing we just talked about was a bug that needed fixing : ) (a) When you pull patches from some repo R1 to R2, you never pull patches that are already present in both. (I assume Darcs already ensures this, but I don't know how it does that given that repositories can be lazy.) (b) However, we'll allow a repository to contain both a patch and its inverse. A and A^ are completely independent patches as far as rule (a) is concerned. (c) Another way of looking at rules (a) and (b): a patch A can be added to the repository, and later its "tombstone" A^ can be added which just means A was deleted. Once a tombstone is added to a repository, it is there forever and the original patch A can never be added back. I'm being a bit vague here about how that's actually implemented; I should figure out the details. (d) The "patch" that resolves the A\/B conflict is actually two patches, A^ and B^ (or more if the conflict is more involved). It may be desirable to store some metadata somewhere indicating that A^ and B^ were added together as part of a merge conflict, but as far as the theory is concerned, adding A^ and adding B^ were completely separate events. Given rules (a) and (b), there's no trouble with adding A^ and B^. 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
Am 03.07.20 um 23:44 schrieb Ben Franksen: > Am 03.07.20 um 22:22 schrieb James Cook: >> I think I've found a new problem with Proposition 5, though. >> >> Suppose A, B and C are three mutually conflicting patches with >> starting context s. >> >> Suppose I merge A and B, then I use Proposition 5 to navigate back to >> the starting context s so that I can continue recording new patches. >> >> The problem: now if I pull in C, it looks just like any other new >> patch to be recorded starting at context s. So, by marking the A\/B >> conflict as resolved, I've made my repository unaware that C should be >> considered to be a conflict. > > I'd say this is a feature, not a bug. If you mark the conflict between A > and B as resolved, *without* recording a new patch, then this means you > are satisfied with the resolution that reverts both changes. There is no > reason why pulling C should conflict now. If, on the other hand, you are > not satisfied with this resolution, you may want record a "proper" > resolution, usually a mixture of A and B. This will then typically > conflict with C. > > That said, there is a problem here. To arrive at the default resolution > (revert the conflicting prim patches) you add inverse patches to the > repo. But what does "adding a patch to a repo" mean, precisely, if > inverses are involved? Is a repo still a sequence of patches? Is A;A^;A > the same as A? That would be bad because resolving a conflict would then > be the same as obliterating the conflicting patches. So inverse pairs > cannot simply be cancelled. An afterthought: what if you do not simply add the inverse for the resolution, but instead record a new patch with the same effect as the inverse? In other words, you add the inverse, but give it a new (positive) name, so that it cannot cancel. Just an idea. 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
Am 03.07.20 um 22:22 schrieb James Cook:
>>> 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.
>
> The trouble is that doesn't give compatible starting/ending contexts
> according to the definition of starting/ending context in Chapter 4.
>
> I want the ending context of A to be the starting context of A^ and vice
> versa.
>
> But, for example, let's see what happens when you commute A;B to B';A'
> and try inverting B'. (contexts aAbBc)
>
> B' is (a, c, A;B, [B], {}, {A}). Its ending context is (a, c, A;B, {B}, {A}).
>
> If you take B'^ to be (c, a, B^;A^, [B^], {A^}, {}), then the starting
> context of B'^ is (c, a, B^;A^, {A^}, {B^}).
>
> Probably those two contexts should be considered equivalent, but under
> the current write-up they're not.
I see. Yes, with inversion added, every context address has two minimal
forms: forward and backward, and these denote the same extended context.
>> 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.
>
> I was assuming the primitive patch theory already has inverses. Is
> that not normal?
You are right, I forgot about that. However, your primitive patches are
named. In Darcs you cannot record a "negative" patch. So while prim
inverses can be calculated internally, they can never be stored as
patches in a repo (except as ingredients of a conflictor).
So the question is whether you want to allow inverse prim patches to be
part of the repo or not.
In any case, you already have inversion in the extended theory. You just
have to show that it has the right properties:
If you commute A;B to B';A', then the inverse of B';A' must be equal to
the commutation of B^;A^. For this to work, you *have* to identify the
mid-contexts. These two contexts exactly correspond to the above forward
and backward minimal context addresses.
Proposition 5 is still trivial with inverses: a (non-empty) complete
undirected graph is connected.
> I think I've found a new problem with Proposition 5, though.
>
> Suppose A, B and C are three mutually conflicting patches with
> starting context s.
>
> Suppose I merge A and B, then I use Proposition 5 to navigate back to
> the starting context s so that I can continue recording new patches.
>
> The problem: now if I pull in C, it looks just like any other new
> patch to be recorded starting at context s. So, by marking the A\/B
> conflict as resolved, I've made my repository unaware that C should be
> considered to be a conflict.
I'd say this is a feature, not a bug. If you mark the conflict between A
and B as resolved, *without* recording a new patch, then this means you
are satisfied with the resolution that reverts both changes. There is no
reason why pulling C should conflict now. If, on the other hand, you are
not satisfied with this resolution, you may want record a "proper"
resolution, usually a mixture of A and B. This will then typically
conflict with C.
That said, there is a problem here. To arrive at the default resolution
(revert the conflicting prim patches) you add inverse patches to the
Re: [darcs-users] How to extend a patch theory to fully commute
> > 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.
The trouble is that doesn't give compatible starting/ending contexts
according to the definition of starting/ending context in Chapter 4.
I want the ending context of A to be the starting context of A^ and vice versa.
But, for example, let's see what happens when you commute A;B to B';A'
and try inverting B'. (contexts aAbBc)
B' is (a, c, A;B, [B], {}, {A}). Its ending context is (a, c, A;B, {B}, {A}).
If you take B'^ to be (c, a, B^;A^, [B^], {A^}, {}), then the starting
context of B'^ is (c, a, B^;A^, {A^}, {B^}).
Probably those two contexts should be considered equivalent, but under
the current write-up they're not.
> > Maybe I
> > should change the last three words to "recording new primitive
> > patches"?
>
> Yes. Applying suggests you already have a patch.
Done:
https://hub.darcs.net/falsifian/misc-pub/patch/d6c3c2d848c8512f9d6dc6e4694f982b02742112
> > 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.)
Good idea. Done:
https://hub.darcs.net/falsifian/misc-pub/patch/bab89c7257ee66c8b2936e3dea2109439bc24b38
I noticed while changing it that I had them mixed up in at least one place.
> 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.
I was assuming the primitive patch theory already has inverses. Is
that not normal?
I think I've found a new problem with Proposition 5, though.
Suppose A, B and C are three mutually conflicting patches with
starting context s.
Suppose I merge A and B, then I use Proposition 5 to navigate back to
the starting context s so that I can continue recording new patches.
The problem: now if I pull in C, it looks just like any other new
patch to be recorded starting at context s. So, by marking the A\/B
conflict as resolved, I've made my repository unaware that C should be
considered to be a conflict.
The only way I can think of to solve this involves recursively adding
new contexts and patches to our underlying patch theory to keep track
of what's been resolved. But I fear this may lead to some
exponentially large data structures like in Darcs-1 when the newly
added things themselves conflict.
Here's my unsatisfactory idea in a bit more detail. We add a new
context s{A, B} to the universe which has the same repo state as s,
and intuitively means "s, except we've seen a conflict between A and
B". We make s{A, B} behave like a primitive context, in the sense that
every primitive patch with starting context s can be converted to a
new (differently named) "primitive"-like patch that does the same
thing but starting at s{A, B}. (In practice, the implementation would
probably not need to be aware of whether it's recording a real
primitive patch or a "primitive"-like patch.) We can
Re: [darcs-users] How to extend a patch theory to fully commute
Am 03.07.20 um 05:22 schrieb James Cook:
> On Thu, 2 Jul 2020 at 18:40, Ben Franksen
> 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
Re: [darcs-users] How to extend a patch theory to fully commute
On Thu, 2 Jul 2020 at 18:40, Ben Franksen
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^.
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.
(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.
(c) I think Proposition 5 might introduce duplicate primitive patches.
Also, the patch sequence it generates is longer than it needs to be.
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.
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.
> 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." Maybe I
should change the last three words to "recording new primitive
patches"?
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).
* 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.
> Also, this paragraph is unsatisfying:
>
> > After some quick thinking, Pseudo managed to find a patch P' which was
> > equivalent in effect to P. However,
Re: [darcs-users] How to extend a patch theory to fully commute
On Thu, 2 Jul 2020 at 09:42, Ben Franksen wrote:
> Am 01.07.20 um 05:09 schrieb James Cook:
> > Definition: We associate a primitive context to every context address
> > (and in particular to every extended context) (a, b, (Qi), X, Y) using
> > the following recursive algorithm.
> >
> > * If X=Y={}, then the context is a (=b). This is an embedded primitive
> > context.
> >
> > * If the sequence (Qi) can be permuted so that it starts with a patch P
> > in X, then we recurse on (a', b, (Q'i), X \ {P}, Y), where a' is ending
> > context of P and Q'i is the rest of the sequence.
> >
> > * Similarly, if (Qi) can be permuted so that it ends with a patch P in
> > Y, then we recurse on (a, b', (Q'i), X, Y \ {P}), where b' is the
> > starting context of P and (Q'i) is the rest of the sequence.
> >
> > * Otherwise, we have a minimal context address. Swap X and Y and recurse
> > on the result (a, b, (Qi), Y, X).
>
> As a possible simplification, wouldn't it be enough to define the
> associated primitive context for minimal context addresses? This would
> eliminate the second and third case. The fourth case would be
> re-formulated as
>
> * Otherwise swap X and Y, minimize, and recurse on the result.
>
> It is clear that a minimal context address is no longer minimal if we
> swap X and Y. Thus, the minimization actually makes it "smaller" ( i.e.
> (Qi) becomes shorter), proving termination.
Good idea.
https://hub.darcs.net/falsifian/misc-pub/patch/8b55486b825568be209028b994383274a85ec1f3#misc/hms_patchfinder
> In general, I think it would be good to dwell a bit on this minimization
> process early on. That is, given some arbitrary context address, how
> exactly do we calculate a minimal version? I suspect this will be (at
> least) quadratic in the length of the context address (see my earlier
> remarks about calculating minimal contexts).
I agree with your suspicion. I have at least the start of an idea for
implementing this reasonably efficiently, but I need to think more
about it.
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
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 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. Also, this paragraph is unsatisfying: > After some quick thinking, Pseudo managed to find a patch P' which was > equivalent in effect to P. However, this turned out not to be a great > solution, since although P' had the same effect as P, it had the name of > a completely different patch, which was confusing. Moreover, the space > required to store P', and computing power needed to commute it, was more > than one should rightfully expect from a simple primitive patch. I think this should either be extended to explain how P' was constructed, or it should be left out. 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
On Thu, 2 Jul 2020 at 09:12, Ben Franksen wrote: > Am 01.07.20 um 05:09 schrieb James Cook: > > The overall procedure is this: > > > > 1. Merge the individual patches to be permuted into a patch sequence > > address (a, b, (Qi), (nj), X, Y). (You could merge a pair of adjacent > > patches, the whole sequence of patches in the repo, or anything in > > between.) > > I think it would be good if you pointed out that what you call "merging" > here is unrelated to what is usually understood as merging patches or > patch sequences. Even better would be to avoid the term "merging" and > instead give the concept a new name, such as "combine" or "join". Oops, it didn't even occur to me I was re-using that word. Changed to "combine": https://hub.darcs.net/falsifian/misc-pub/patch/a8dcb051bd2febec297ae1611266e33234a3924e 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
On Thu, 2 Jul 2020 at 08:57, Ben Franksen wrote:
> > Definition: Let A=(a, b, (Qi), (nj), X, Y) be an patch sequence address
> > of length n (i.e. (nj) has n names in it). The /separation/ of A is a
> > sequence of n extended patches. Patch j in the sequence is the minimal
> > form of (a, b, (Qi), nj, X U {before}, Y U {after}), where {before} is
> > the set of names that came before j in the sequence and {after} is the
> > names that came after.
>
> Could explicitly state which sequence you refer to in the last sentence?
> I.e. do you mean (Qi) or (nj) here? The wording ("set of names")
> suggests that you refer to (nj). It would also be better if you would
> not use j for both the generic index and the particular index here. Here
> is a reformulation that is clearer IMO:
Yes, the names in the sequence (nj).
> Definition: Let A=(a, b, (Qi), (nj), X, Y) be a patch sequence address,
> where j ranges from 1 to l (i.e. (nj) has l names in it). The
> /separation/ of A is a sequence of l extended patches, such that patch k
> in the sequence is the minimal form of (a, b, (Qi), nk, Xk, Yk), where
> Xk = X U {nj|jk}.
Thanks, that's better. I put in your definition (but wrote [nk]
instead of nk) and also updated the proof of Proposition 3 to match
(and add a bit more explanation):
https://hub.darcs.net/falsifian/misc-pub/patch/17b04398d42f5c8ebf8f3aff79201cc766261503
___
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
On Thu, 2 Jul 2020 at 08:32, Ben Franksen wrote: > > Definition: A /patch sequence address/ is a tuple > > (a, b, (Qi), (nj), X, Y), where a and b are (primitive) contexts, (Qi) > > is a sequence of (primitive) patches going from a to b, nj is a sequence > > of unique names of patches in (Qi), and X and Y are a partition of the > > remaining names in (Qi). [...] > > > Definition: Two minimal patch sequence addresses are /equivalent/ if all > > their properties are the same except possibly the patch sequences (Qi), > > and those two patch sequences are permutations of each other that can be > > achieved in the primitive patch theory. > > Does that mean (a, b, (Pi), (nj), X, Y) and (a, b, (Qi), (mj), X, Y) are > not equivalent if (nj) and (mj) consist of the same set of names but in > a different order? If so, it may be worthwhile to say that explicitly. Right, the order has to be the same. Updated: https://hub.darcs.net/falsifian/misc-pub/patch/e4da914113bae54b38eab83be71ad9e38cddaf09 It would also be reasonable to let (nj) be a set instead of a sequence, so order doesn't matter, and call it a patch *set* address. I think the merge-permute-separate procedure in Chapter 5 could be revised to use a patch set address in place of a patch sequence address. I guess the desired new order of the patches would become a parameter of Step 3 (separation), and Step 2 would disappear. 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
On Thu, 2 Jul 2020 at 07:53, Ben Franksen wrote: > Am 02.07.20 um 00:37 schrieb James Cook: > >> The construction works by inductively taking any pair of incommutable > >> patches (in sequence, i.e. with a common middle state) and then > >> "formally" commuting it. The new node is represented as that pair of > >> patches. Is that, essentially, the idea? > > > > Sorry, I should add one note here: I'm not sure it's accurate to say > > the construction "inductively" makes pairs of incommutable patches > > commute. That sounds like you're saying everything's built out of > > transpositions. Maybe there's some equivalent formulation that works > > that way, but e.g. if you want to commute A;B;C to C;B;A there's > > nothing in my construction that says it's done one transposition at a > > time. Instead, you identify each patch in the sequence C;B;A with a > > "patch address", then simplify that patch address as much as you can. > > I see. But if you can prove permutivity (and from skimming through to > the end of your story it loks like you can) then it should be possible > to arrive at the same result(s) by doing it one transposition at a time. > > That is, we start with A;B;C, then first commute B;C to C';B', then A;C' > to C'';A'. The result C'';A';B' should be the same as if we do it in one > stroke and simplify as in the definition. Yes, once we've defined the extended patch universe, you can achieve any permutation through transpositions. I was concerned about the construction of the patch universe itself. If you start with the primitive patch theory, and then extend the theory one failed commutation at a time until you have a theory where all commutations are possible, then it probably ends up being the same theory but I'm not sure. 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
> Thanks for writing this down. I think you should add this example to > your text as it is a good illustration. Good idea; done at https://hub.darcs.net/falsifian/misc-pub/patch/5571a2e0c22659114fd5a919e06be844819afccc . 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
Am 01.07.20 um 05:09 schrieb James Cook:
> Definition: We associate a primitive context to every context address
> (and in particular to every extended context) (a, b, (Qi), X, Y) using
> the following recursive algorithm.
>
> * If X=Y={}, then the context is a (=b). This is an embedded primitive
> context.
>
> * If the sequence (Qi) can be permuted so that it starts with a patch P
> in X, then we recurse on (a', b, (Q'i), X \ {P}, Y), where a' is ending
> context of P and Q'i is the rest of the sequence.
>
> * Similarly, if (Qi) can be permuted so that it ends with a patch P in
> Y, then we recurse on (a, b', (Q'i), X, Y \ {P}), where b' is the
> starting context of P and (Q'i) is the rest of the sequence.
>
> * Otherwise, we have a minimal context address. Swap X and Y and recurse
> on the result (a, b, (Qi), Y, X).
As a possible simplification, wouldn't it be enough to define the
associated primitive context for minimal context addresses? This would
eliminate the second and third case. The fourth case would be
re-formulated as
* Otherwise swap X and Y, minimize, and recurse on the result.
It is clear that a minimal context address is no longer minimal if we
swap X and Y. Thus, the minimization actually makes it "smaller" ( i.e.
(Qi) becomes shorter), proving termination.
In general, I think it would be good to dwell a bit on this minimization
process early on. That is, given some arbitrary context address, how
exactly do we calculate a minimal version? I suspect this will be (at
least) quadratic in the length of the context address (see my earlier
remarks about calculating minimal contexts).
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
Am 01.07.20 um 05:09 schrieb James Cook: > The overall procedure is this: > > 1. Merge the individual patches to be permuted into a patch sequence > address (a, b, (Qi), (nj), X, Y). (You could merge a pair of adjacent > patches, the whole sequence of patches in the repo, or anything in > between.) I think it would be good if you pointed out that what you call "merging" here is unrelated to what is usually understood as merging patches or patch sequences. Even better would be to avoid the term "merging" and instead give the concept a new name, such as "combine" or "join". 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
> Definition: Let A=(a, b, (Qi), (nj), X, Y) be an patch sequence address
> of length n (i.e. (nj) has n names in it). The /separation/ of A is a
> sequence of n extended patches. Patch j in the sequence is the minimal
> form of (a, b, (Qi), nj, X U {before}, Y U {after}), where {before} is
> the set of names that came before j in the sequence and {after} is the
> names that came after.
Could explicitly state which sequence you refer to in the last sentence?
I.e. do you mean (Qi) or (nj) here? The wording ("set of names")
suggests that you refer to (nj). It would also be better if you would
not use j for both the generic index and the particular index here. Here
is a reformulation that is clearer IMO:
Definition: Let A=(a, b, (Qi), (nj), X, Y) be a patch sequence address,
where j ranges from 1 to l (i.e. (nj) has l names in it). The
/separation/ of A is a sequence of l extended patches, such that patch k
in the sequence is the minimal form of (a, b, (Qi), nk, Xk, Yk), where
Xk = X U {nj|jk}.
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
> Definition: A /patch sequence address/ is a tuple > (a, b, (Qi), (nj), X, Y), where a and b are (primitive) contexts, (Qi) > is a sequence of (primitive) patches going from a to b, nj is a sequence > of unique names of patches in (Qi), and X and Y are a partition of the > remaining names in (Qi). [...] > Definition: Two minimal patch sequence addresses are /equivalent/ if all > their properties are the same except possibly the patch sequences (Qi), > and those two patch sequences are permutations of each other that can be > achieved in the primitive patch theory. Does that mean (a, b, (Pi), (nj), X, Y) and (a, b, (Qi), (mj), X, Y) are not equivalent if (nj) and (mj) consist of the same set of names but in a different order? If so, it may be worthwhile to say that explicitly. 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
Am 02.07.20 um 00:37 schrieb James Cook: >> The construction works by inductively taking any pair of incommutable >> patches (in sequence, i.e. with a common middle state) and then >> "formally" commuting it. The new node is represented as that pair of >> patches. Is that, essentially, the idea? > > Sorry, I should add one note here: I'm not sure it's accurate to say > the construction "inductively" makes pairs of incommutable patches > commute. That sounds like you're saying everything's built out of > transpositions. Maybe there's some equivalent formulation that works > that way, but e.g. if you want to commute A;B;C to C;B;A there's > nothing in my construction that says it's done one transposition at a > time. Instead, you identify each patch in the sequence C;B;A with a > "patch address", then simplify that patch address as much as you can. I see. But if you can prove permutivity (and from skimming through to the end of your story it loks like you can) then it should be possible to arrive at the same result(s) by doing it one transposition at a time. That is, we start with A;B;C, then first commute B;C to C';B', then A;C' to C'';A'. The result C'';A';B' should be the same as if we do it in one stroke and simplify as in the definition. It could very well be that your approach is more efficient. Your proofs are surprisingly short which suggests that your "global" approach to commutation (define it immediately for sequences instead of first for pairs and then generalize inductively) has some advantages. But first I'll have to understand how extended patches commute in your theory and I still haven't come that far. 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
Am 02.07.20 um 00:29 schrieb James Cook:
> Definition: A /patch address/ is a patch sequence address where the
> sequence (nj) has length one.
>
> Sorry, there are a lot of definitions, but maybe you missed that one?
Oops. Yes, sorry. I was jumping around, trying to get a grip on the idea.
>> Indeed, given a minimal patch sequence address in its general form (a,
>> b, (Qi), (nj), X, Y), is this now a new *singular* patch in the extended
>> theory, regardless of how long the sequence Qi is? I don't see how how
>> this can work. Isn't that universe much larger than what was intended?
>
> I intended only to include patch addresses, i.e. where (nj) has length
> one. On the other hand, (Qi) is not restricted in length.
Okay, thanks.
>> I think calculating this for a small but non-trivial example would be
>> highly instructive. Say we have primitive patches A;B;C, where neither
>> A;B nor B;C commute. What does the extended universe look like here?
>
> I think that primitive patch theory has four contexts. Call them a, b,
> c, d: a A b B c C d.
>
> The new patch theory should have 2^3=8 contexts. Here are the
> remaining four. (I'm using patches and their names interchangeably.)
>
> (1) After just applying B: (a, c, [A, B], {B}, {A}). (This is the
> simple case of switching two patches.)
>
> (2) After just applying C: (a, d, [A, B, C], {C}, {A, B}). (We can't
> get C without A and B, so we need everything here.)
>
> (3) After applying A and C (missing B): (b, d, [B, C], {C}, {B}).
> (This is another example of the simple case of switching two patches.)
>
> (4) After applying B and C: (a, d, [A, B, C], {B, C}, {A}). (This
> situation is similar to (2), but with everything reversed.)
>
> The new patch theory should have 12 patches (a cube has 12 edges).
> Three are primitive, so there are 9 left to add.
>
> (a) B in the sequence B;A;C. (In other words, commute A and B and look
> at B.) This patch's starting context is a, its ending context is (1)
> above, and as a canonical patch address, it is represented as: (a, c,
> [A, B], [B], {}, {A}). The first three elements of the tuple tell us
> this patch lives somewhere on the square of edges between a and c, and
> the last three elements locate the patch within the square: the patch
> is named B; nothing comes before the patch; and A comes after the
> patch.
>
> (b) C in the sequence C;A;B (or C;B;A) is (a, d, [A, B, C], [C], {}, {A, B}).
>
> (c) A in the sequence B;A;C is (a, c, [A, B], {B}, {})
>
> (d) A in the sequence C;A;B is (a, d, [A, B, C], {C}, {B}).
>
> (e) B in the sequence C;B;A is (a, d, [A, B, C], [B], {C}, {A}).
>
> (f) C in the sequence A;C;B is (b, d, [B, C], {}, {B}).
>
> (g) C in the sequence B;C;A is (a, d, [A, B, C], {B}, {A}).
>
> (h) B in the sequence A,C;B is (b, d, [B, C], [B], {C}, {}).
>
> (i) A in the sequence B;C;A (or C;B;A) is (a, d, [A, B, C], [A], {B, C}, {}).
Thanks for writing this down. I think you should add this example to
your text as it is a good illustration.
I cannot comment yet on the rest because I still haven't read those
later sections.
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
> The construction works by inductively taking any pair of incommutable > patches (in sequence, i.e. with a common middle state) and then > "formally" commuting it. The new node is represented as that pair of > patches. Is that, essentially, the idea? Sorry, I should add one note here: I'm not sure it's accurate to say the construction "inductively" makes pairs of incommutable patches commute. That sounds like you're saying everything's built out of transpositions. Maybe there's some equivalent formulation that works that way, but e.g. if you want to commute A;B;C to C;B;A there's nothing in my construction that says it's done one transposition at a time. Instead, you identify each patch in the sequence C;B;A with a "patch address", then simplify that patch address as much as you can. 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
On Wed, 1 Jul 2020 at 21:14, Ben Franksen wrote:
> Am 01.07.20 um 18:45 schrieb James Cook:
> >> Just to check I understood the idea (up to this point): roughly
> >> speaking, you represent "unrepresentable" states by formally commuting
> >> patches.
> >>
> >> That is, if we regard the primitive states as vertices and primitive
> >> (named) patches as edges in a graph, then you extend the graph with new
> >> nodes and edges.
> >
> > That's exactly the intuition.
> >
> > If you had n patches that all commuted, this graph would be a
> > hypercube, i.e. the nodes are the 2^n subsets of patches and each edge
> > adds one patch.
> >
> > I think my theory always extends this graph exactly to that hypercube,
> > filling in exactly those nodes and edges that are missing. I haven't
> > thought carefully about that point of view so maybe that's not true.
> >
> >> The construction works by inductively taking any pair of incommutable
> >> patches (in sequence, i.e. with a common middle state) and then
> >> "formally" commuting it. The new node is represented as that pair of
> >> patches. Is that, essentially, the idea?
> >
> > Yes, that's exactly what happens when there are only two patches
> > involved and they don't commute.
>
> Okay, good. Now, you go on to define
>
> > Definition: Given any primitive patch theory, the /extended patch
> > universe/ is the set of all patch addresses. A primitive patch P going
> > from context a to b is embedded as (a, b, [P], name of P, {}, {}).
>
> Here you cleverly rename your concept. Before this point you talk about
> patch /sequence/ addresses, now it's only patch addresses. Perhaps just
> an ommision, but I suspect a bit of wishful thinking here.
Definition: A /patch address/ is a patch sequence address where the
sequence (nj) has length one.
Sorry, there are a lot of definitions, but maybe you missed that one?
> Indeed, given a minimal patch sequence address in its general form (a,
> b, (Qi), (nj), X, Y), is this now a new *singular* patch in the extended
> theory, regardless of how long the sequence Qi is? I don't see how how
> this can work. Isn't that universe much larger than what was intended?
I intended only to include patch addresses, i.e. where (nj) has length
one. On the other hand, (Qi) is not restricted in length.
> I think calculating this for a small but non-trivial example would be
> highly instructive. Say we have primitive patches A;B;C, where neither
> A;B nor B;C commute. What does the extended universe look like here?
I think that primitive patch theory has four contexts. Call them a, b,
c, d: a A b B c C d.
The new patch theory should have 2^3=8 contexts. Here are the
remaining four. (I'm using patches and their names interchangeably.)
(1) After just applying B: (a, c, [A, B], {B}, {A}). (This is the
simple case of switching two patches.)
(2) After just applying C: (a, d, [A, B, C], {C}, {A, B}). (We can't
get C without A and B, so we need everything here.)
(3) After applying A and C (missing B): (b, d, [B, C], {C}, {B}).
(This is another example of the simple case of switching two patches.)
(4) After applying B and C: (a, d, [A, B, C], {B, C}, {A}). (This
situation is similar to (2), but with everything reversed.)
The new patch theory should have 12 patches (a cube has 12 edges).
Three are primitive, so there are 9 left to add.
(a) B in the sequence B;A;C. (In other words, commute A and B and look
at B.) This patch's starting context is a, its ending context is (1)
above, and as a canonical patch address, it is represented as: (a, c,
[A, B], [B], {}, {A}). The first three elements of the tuple tell us
this patch lives somewhere on the square of edges between a and c, and
the last three elements locate the patch within the square: the patch
is named B; nothing comes before the patch; and A comes after the
patch.
(b) C in the sequence C;A;B (or C;B;A) is (a, d, [A, B, C], [C], {}, {A, B}).
(c) A in the sequence B;A;C is (a, c, [A, B], {B}, {})
(d) A in the sequence C;A;B is (a, d, [A, B, C], {C}, {B}).
(e) B in the sequence C;B;A is (a, d, [A, B, C], [B], {C}, {A}).
(f) C in the sequence A;C;B is (b, d, [B, C], {}, {B}).
(g) C in the sequence B;C;A is (a, d, [A, B, C], {B}, {A}).
(h) B in the sequence A,C;B is (b, d, [B, C], [B], {C}, {}).
(i) A in the sequence B;C;A (or C;B;A) is (a, d, [A, B, C], [A], {B, C}, {}).
In my opinion, the trickier part is arguing that extended patches can
be "merged" into extended patch sequences as described in Chapter 5,
in such a way that separating that sequence would recover the original
patches. We need the merge and separate operations in order to permute
the order of extended patches.
Let's try using this procedure to commute the primitive patches A;B
from their original places in the sequence. They should turn into (a)
and (c) above.
First, we merge the patches by following the proof of Proposition 4.
Conveniently, A and B have the same names. They are embedded as A=(a,
b, [A], [A], {}, {})
Re: [darcs-users] How to extend a patch theory to fully commute
Am 01.07.20 um 18:45 schrieb James Cook:
>> Just to check I understood the idea (up to this point): roughly
>> speaking, you represent "unrepresentable" states by formally commuting
>> patches.
>>
>> That is, if we regard the primitive states as vertices and primitive
>> (named) patches as edges in a graph, then you extend the graph with new
>> nodes and edges.
>
> That's exactly the intuition.
>
> If you had n patches that all commuted, this graph would be a
> hypercube, i.e. the nodes are the 2^n subsets of patches and each edge
> adds one patch.
>
> I think my theory always extends this graph exactly to that hypercube,
> filling in exactly those nodes and edges that are missing. I haven't
> thought carefully about that point of view so maybe that's not true.
>
>> The construction works by inductively taking any pair of incommutable
>> patches (in sequence, i.e. with a common middle state) and then
>> "formally" commuting it. The new node is represented as that pair of
>> patches. Is that, essentially, the idea?
>
> Yes, that's exactly what happens when there are only two patches
> involved and they don't commute.
Okay, good. Now, you go on to define
> Definition: Given any primitive patch theory, the /extended patch
> universe/ is the set of all patch addresses. A primitive patch P going
> from context a to b is embedded as (a, b, [P], name of P, {}, {}).
Here you cleverly rename your concept. Before this point you talk about
patch /sequence/ addresses, now it's only patch addresses. Perhaps just
an ommision, but I suspect a bit of wishful thinking here.
Indeed, given a minimal patch sequence address in its general form (a,
b, (Qi), (nj), X, Y), is this now a new *singular* patch in the extended
theory, regardless of how long the sequence Qi is? I don't see how how
this can work. Isn't that universe much larger than what was intended?
I think calculating this for a small but non-trivial example would be
highly instructive. Say we have primitive patches A;B;C, where neither
A;B nor B;C commute. What does the extended universe look like here?
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
> Definition: A context address (a, b, (Qi), X, Y) is a /simplification/ > of a context address (a', b', (Q'i), X', Y') if X and Y are subsets of > (or equal to) X' and Y' and the sequence (Q'i) can be permuted so that > it first follows the patches in X' \ X from a' to a, then follows the > sequence (Qi), then follows the patches in Y' \ Y from b to b'. > > Assumption 2: If a context address A has two different simplifications B > and B' that are both canonical addresses, then B = B'. (I suspect this > assumption may be false for Darcs 2 due to duplicate patches.) > > Remark: This is essentially saying that if you move as many patches in Y > as possible to the end of the sequence, and as many patches in X as > possible to the beginning, the final set of remaining patches you end up > with is deterministic. Two remarks. (1) I think you may be able to prove this assuming general permutivity for the primitive patch theory. (2) As you already remarked, canonicity here is not essential for the theory. For an equivalence class of things you can take an arbitrary element as representative. But what you *do* have to show is that (a) this is actually an equivalence class (easy, I think) and (b) that the choice of representative doesn't matter. (b) is usually the harder part. You also need to prove it for every operation you define on the equivalence classes (if you define it in terms of a representative member). In a practical implementation you would indeed have to fix a deterministic algorithm to choose the representative, but for the theory I think it is clearer to abstract over this choice. 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
> BTW, you don't say it explicitly, but since in several places you refer > to names, I was assuming that in your theory prim patches are always named. Yes, I'm assuming every prim patch has a unique name. Part of the tuple encoding an extended patch is the name of a prim patch. That could be used as the extended patch's name. 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
Am 01.07.20 um 18:39 schrieb James Cook: >> A well-known and quite natural way to identify the equivalence class of >> all patches that a given patch P can be commuted to, is to use the so >> called "minimal context". A minimal context C(P) for some patch P is a >> sequence of patches starting at the empty state and preceding P, and >> that is minimal in the sense that no subset of it is a valid context. In >> other words, no patch in C(P) can be commuted past P. Another way to >> look at it is to start with a patch P in /any/ context and then commute >> everything you can past P. It is easy to show that this can always be >> done and that the result is unique i.e. you always get the same /set/ of >> patches for the minimal context. > > I think I've found a case where darcs 2 violates that uniqueness > property. Yes, because this uniqueness is a consequence of permutivity. > In fact, I got darcs to crash after that, so I filed > http://bugs.darcs.net/issue2647 This is a well known bug in both darcs-1 and darcs-2 format. It is the infamous "duplicate prim patch" problem. If you don't track the identity of prim patches (such as is done in darcs-3, but not in darcs-1 and darcs-2), then commutation /cannot/ distinguish between equal prim patches. The camp paper explains that in Appendix B. > I added comments interspersed with the shell commands in that bug > explaining where I managed to change the minimal context of a patch. > Is that in itself a bug? Yes. This clearly violates permutivity. Whether patches commute must be independent of reordering. > This behaviour is behind the note I added to Assumption 2 about it > possibly being false for Darcs 2. When I originally discovered it, I > thought I just had to live with that, but based on your email, and the > fact that I've now actually crashed Darcs, I guess maybe the behaviour > is unintended. The behavior is definitely not intended. The fact that darcs crashes here shows that it internally expects permutivity to hold. BTW, you don't say it explicitly, but since in several places you refer to names, I was assuming that in your theory prim patches are always named. 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
> Just to check I understood the idea (up to this point): roughly > speaking, you represent "unrepresentable" states by formally commuting > patches. > > That is, if we regard the primitive states as vertices and primitive > (named) patches as edges in a graph, then you extend the graph with new > nodes and edges. That's exactly the intuition. If you had n patches that all commuted, this graph would be a hypercube, i.e. the nodes are the 2^n subsets of patches and each edge adds one patch. I think my theory always extends this graph exactly to that hypercube, filling in exactly those nodes and edges that are missing. I haven't thought carefully about that point of view so maybe that's not true. > The construction works by inductively taking any pair of incommutable > patches (in sequence, i.e. with a common middle state) and then > "formally" commuting it. The new node is represented as that pair of > patches. Is that, essentially, the idea? Yes, that's exactly what happens when there are only two patches involved and they don't commute. > It reminds me of the darcs-1 patch format, where a "merger" patch is > defined as the ordered pair consisting of both conflicting patches. I think I read about darcs-1 conflictors a long time ago, so that general idea has been on my mind for a while. 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
> A well-known and quite natural way to identify the equivalence class of > all patches that a given patch P can be commuted to, is to use the so > called "minimal context". A minimal context C(P) for some patch P is a > sequence of patches starting at the empty state and preceding P, and > that is minimal in the sense that no subset of it is a valid context. In > other words, no patch in C(P) can be commuted past P. Another way to > look at it is to start with a patch P in /any/ context and then commute > everything you can past P. It is easy to show that this can always be > done and that the result is unique i.e. you always get the same /set/ of > patches for the minimal context. I think I've found a case where darcs 2 violates that uniqueness property. In fact, I got darcs to crash after that, so I filed http://bugs.darcs.net/issue2647 I added comments interspersed with the shell commands in that bug explaining where I managed to change the minimal context of a patch. Is that in itself a bug? This behaviour is behind the note I added to Assumption 2 about it possibly being false for Darcs 2. When I originally discovered it, I thought I just had to live with that, but based on your email, and the fact that I've now actually crashed Darcs, I guess maybe the behaviour is unintended. 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
Am 01.07.20 um 17:59 schrieb Ben Franksen: > Am 01.07.20 um 17:13 schrieb James Cook: >> On Wed, 1 Jul 2020 at 10:21, Ben Franksen wrote: >>> Am 01.07.20 um 05:09 schrieb James Cook: The context address /points to/ a context c if there exists a permutation of (Qi) such that all the patches with names in X come before patches with names in Y, and c is the after-context of the k-th patch in the sequence (equivalently, the before-context of the (k+1)-th patch), where k = |X|. >>> >>> and later: >>> Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is impossible (in the primitive patch theory) to commute the sequence (Qi) so that it begins with a patch in X or ends with a patch in Y. >>> >>> Did you mix up X and Y here? I would have expected the sentence to say >>> "begins with a patch in Y or ends with a patch in X". >> >> I think this part is correct as written. I added some more >> explanation: >> https://hub.darcs.net/falsifian/misc-pub/patch/3bf868962261b8b275f81a82136106ee4c444dd1 >> >> The point of minimal addresses is that they "point" to contexts that >> aren't already part of the primitive patch theory. If a patch in X >> could be moved to the start, or a patch in Y could be moved to the >> end, then the address could be made even more minimal by leaving out >> that patch (the more minimal address would be called a >> "simplification" as defined in Chapter 4). > > Okay, I think I got it now. Thanks for the explanation. Just to check I understood the idea (up to this point): roughly speaking, you represent "unrepresentable" states by formally commuting patches. That is, if we regard the primitive states as vertices and primitive (named) patches as edges in a graph, then you extend the graph with new nodes and edges. The construction works by inductively taking any pair of incommutable patches (in sequence, i.e. with a common middle state) and then "formally" commuting it. The new node is represented as that pair of patches. Is that, essentially, the idea? It reminds me of the darcs-1 patch format, where a "merger" patch is defined as the ordered pair consisting of both conflicting patches. 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
Am 01.07.20 um 17:13 schrieb James Cook: > On Wed, 1 Jul 2020 at 10:21, Ben Franksen wrote: >> Am 01.07.20 um 05:09 schrieb James Cook: >>> The context address /points to/ a context c if there exists a >>> permutation of (Qi) such that all the patches with names in X come >>> before patches with names in Y, and c is the after-context of the k-th >>> patch in the sequence (equivalently, the before-context of the (k+1)-th >>> patch), where k = |X|. >> >> and later: >> >>> Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is >>> impossible (in the primitive patch theory) to commute the sequence (Qi) >>> so that it begins with a patch in X or ends with a patch in Y. >> >> Did you mix up X and Y here? I would have expected the sentence to say >> "begins with a patch in Y or ends with a patch in X". > > I think this part is correct as written. I added some more > explanation: > https://hub.darcs.net/falsifian/misc-pub/patch/3bf868962261b8b275f81a82136106ee4c444dd1 > > The point of minimal addresses is that they "point" to contexts that > aren't already part of the primitive patch theory. If a patch in X > could be moved to the start, or a patch in Y could be moved to the > end, then the address could be made even more minimal by leaving out > that patch (the more minimal address would be called a > "simplification" as defined in Chapter 4). Okay, I think I got it now. Thanks for the explanation. 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
On Wed, 1 Jul 2020 at 10:12, Ben Franksen wrote:
> I haven't fully digested everything you wrote but I guess a remark may
> be in order, lest you waste time on something that cannot be implemented
> efficiently. I am not claiming this is equivalent to what you aim at,
> but I think it is at least related.
>
> A well-known and quite natural way to identify the equivalence class of
> all patches that a given patch P can be commuted to, is to use the so
> called "minimal context". A minimal context C(P) for some patch P is a
> sequence of patches starting at the empty state and preceding P, and
> that is minimal in the sense that no subset of it is a valid context. In
> other words, no patch in C(P) can be commuted past P. Another way to
> look at it is to start with a patch P in /any/ context and then commute
> everything you can past P. It is easy to show that this can always be
> done and that the result is unique i.e. you always get the same /set/ of
> patches for the minimal context.
>
> In principle, we could represent patches as they appear in their minimal
> context, together with the set of patches in the minimal context. This
> would be a unique representation which could be stored hashed and thus
> would be fully tamper-proof.
>
> The problem is that computing minimal contexts is prohibitively
> expensive. Nobody has bever come up up with an algorithm that is better
> than O(n^3) in the worst case, where n is the size of the context you
> start with. The reason it is so hard to improve on this is that before
> we can commute two patches, we need to first bring them into proximity.
> Suppose half the patches in the starting context commute past, and the
> other half does not. The patches that do not commute past will
> accumulate before the patch P and all earlier patches you try to commute
> must be commuted past all these accumulated patches, one by one.
Wouldn't that result in O(n^2) commuting operations rather than
O(n^2)? Even so, not nice.
I do think this is related. I'll admit I haven't thought much about
efficiency. My initial impression is that efficiency would be a
problem with the theory as described, but that that could probably be
fixed.
Here are some notes (the last two might not mean much yet, depending
on how deep into the document you've waded).
* If you only ever add primitive patches, and you never commute
patches that would not commute in the primitive theory, then all the
patches keep their representation as primitive patches (technically,
as embedded primitive patches of the form (a, b, [P], [name of P], {},
{}) as described in the "extended patch universe" definition), and
commuting is essentially just primitive commuting. So, efficiency
could only be an issue where conflicts are involved.
* On the other hand, if there are conflicts, converting all of the
patch addresses to "canonical" form (Chapter 3) could cause efficiency
problems. I suspect commuting two patches won't take longer than O(n),
where n is the length of the (Qi) sequences involved (related to how
many patches are involved in the overall conflict) but I'd need to
think about it more.
* I've been assuming a repository will be represented as a sequence of
individual "extended patches". However, there's also a notion of a
"minimal patch sequence address" which could be used to represent the
entire repository. One advantage of the representation is that
permuting patches is trivial: you just permute a stored list of names.
One disadvantage is that if you want to remove a name from the end of
the sequence, you'll need to permute the internally stored sequence
(Qi) so that it ends with that name, and if you wanted to pull from
another similar repo, you'd need to permute one of the (Qi) sequences
so they're compatible with each other. This might end up being similar
to how Darcs already works. (In the document, I talk about "extended
patch sequences". These are the same as minimal patch sequence
addresses, but with an added requirement that (Qi) is kept in
canonical order. You'd want to drop that requirement if you were doing
this, for efficiency reasons.)
* Come to think of it, the "canonical" requirements I put in the
document are probably a bad idea. I think I only put them in so that
the representation of a patch P commuted to a particular starting
context a will always be the same no matter how it got there. I don't
think that's really needed, though; if you want to know whether two
patches are the same, you can just compare their names.
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
On Wed, 1 Jul 2020 at 10:21, Ben Franksen wrote: > Am 01.07.20 um 05:09 schrieb James Cook: > > The context address /points to/ a context c if there exists a > > permutation of (Qi) such that all the patches with names in X come > > before patches with names in Y, and c is the after-context of the k-th > > patch in the sequence (equivalently, the before-context of the (k+1)-th > > patch), where k = |X|. > > and later: > > > Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is > > impossible (in the primitive patch theory) to commute the sequence (Qi) > > so that it begins with a patch in X or ends with a patch in Y. > > Did you mix up X and Y here? I would have expected the sentence to say > "begins with a patch in Y or ends with a patch in X". I think this part is correct as written. I added some more explanation: https://hub.darcs.net/falsifian/misc-pub/patch/3bf868962261b8b275f81a82136106ee4c444dd1 The point of minimal addresses is that they "point" to contexts that aren't already part of the primitive patch theory. If a patch in X could be moved to the start, or a patch in Y could be moved to the end, then the address could be made even more minimal by leaving out that patch (the more minimal address would be called a "simplification" as defined in Chapter 4). 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
On Wed, 1 Jul 2020 at 09:44, Ben Franksen wrote:
> Am 01.07.20 um 05:09 schrieb James Cook:
> > Example: Suppose a is the starting context (empty repository), Q1
> > creates the file "foo" starting from a, Q2 creates the file "bar"
> > starting from there, and b and c are the contexts after P1 and then P2.
> > The address (a, c, [Q1, Q2], {}, {1, 2}) points to a,
> > (a, c, [P1, P2], {1}, {2}) points to b, and (a, c, [P1, P2], {2}, {1})
> > points to the new context you'd get if you applied just Q2 (the
> > repository has "bar" but not "foo").
>
> Did you mix up the Qs and Ps here? Or did you means that the Ps are the
> result of commuting the Qs? A clarification would help me understand
> this better.
I mixed up the Ps and Qs; they should all be Qs.
I started maintaining an updated version at
https://hub.darcs.net/falsifian/misc-pub/browse/misc/hms_patchfinder
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
Am 01.07.20 um 05:09 schrieb James Cook: > The context address /points to/ a context c if there exists a > permutation of (Qi) such that all the patches with names in X come > before patches with names in Y, and c is the after-context of the k-th > patch in the sequence (equivalently, the before-context of the (k+1)-th > patch), where k = |X|. and later: > Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is > impossible (in the primitive patch theory) to commute the sequence (Qi) > so that it begins with a patch in X or ends with a patch in Y. Did you mix up X and Y here? I would have expected the sentence to say "begins with a patch in Y or ends with a patch in X". 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
I haven't fully digested everything you wrote but I guess a remark may be in order, lest you waste time on something that cannot be implemented efficiently. I am not claiming this is equivalent to what you aim at, but I think it is at least related. A well-known and quite natural way to identify the equivalence class of all patches that a given patch P can be commuted to, is to use the so called "minimal context". A minimal context C(P) for some patch P is a sequence of patches starting at the empty state and preceding P, and that is minimal in the sense that no subset of it is a valid context. In other words, no patch in C(P) can be commuted past P. Another way to look at it is to start with a patch P in /any/ context and then commute everything you can past P. It is easy to show that this can always be done and that the result is unique i.e. you always get the same /set/ of patches for the minimal context. In principle, we could represent patches as they appear in their minimal context, together with the set of patches in the minimal context. This would be a unique representation which could be stored hashed and thus would be fully tamper-proof. The problem is that computing minimal contexts is prohibitively expensive. Nobody has bever come up up with an algorithm that is better than O(n^3) in the worst case, where n is the size of the context you start with. The reason it is so hard to improve on this is that before we can commute two patches, we need to first bring them into proximity. Suppose half the patches in the starting context commute past, and the other half does not. The patches that do not commute past will accumulate before the patch P and all earlier patches you try to commute must be commuted past all these accumulated patches, one by one. 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
Am 01.07.20 um 05:09 schrieb James Cook:
> Example: Suppose a is the starting context (empty repository), Q1
> creates the file "foo" starting from a, Q2 creates the file "bar"
> starting from there, and b and c are the contexts after P1 and then P2.
> The address (a, c, [Q1, Q2], {}, {1, 2}) points to a,
> (a, c, [P1, P2], {1}, {2}) points to b, and (a, c, [P1, P2], {2}, {1})
> points to the new context you'd get if you applied just Q2 (the
> repository has "bar" but not "foo").
Did you mix up the Qs and Ps here? Or did you means that the Ps are the
result of commuting the Qs? A clarification would help me understand
this better.
Cheers
Ben
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
