Re: [darcs-users] Darcs equivalent of force-pushing and branching
On Fri, Sep 10, 2021 at 08:19:29PM +0900, Stephen J. Turnbull wrote: > James Cook writes: > > > For short-lived branches, I just use one clone per branch. I think this > > should work well for long-lived branches too, but I haven't tried. > > What's nice about the git storage model is that you can have a > "warehouse" repository with dozens of more or less active branches in > it, and two or three workspaces (which can even share the commit and > content storage of the warehouse, and the warehouse may not even have > a workspace). I've never wanted more than 3 workspaces, but when > doing release management stuff I've sometimes had as many as 10 active > branches I'm worried about in one session. > > git's storage model makes these workflows fast. Also, in the release > manager workflow, I often didn't need file content as such, I needed > diffs and merges, and the storage model makes it possible to diff and > merge across branches without a checkout (of course for merges the > target branch was always checked out, but in theory it didn't need to > be!) I've used git with multiple working directories, and it is nice. darcs uses hard links to save space, so having multiple clones should be relatively cheap. I only make light use of branches / work dirs / extra clones, but so far I have no complaints about using Darcs and just having one clone per workdir or branch. I don't know a nice command for diffing "branches" if the branches are Darcs repos, though. I guess I would use "diff -r" and filter out anything under _darcs. > All of this is obviously quite possible with Darcs. The problem is > getting the "accounting" right when separating the management of > *sets* of patches from the management of *histories*. IIRC, in Darcs > the history is in the patches, which means a bit of tedious surgery on > data structures needs to be done. I'm not sure what you mean by "histories" as distinct from "sets of patches". Shouldn't a branch just be a set of patches? -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Darcs equivalent of force-pushing and branching
> Is there a way to "cleanly" separate two different set of features, > let's say "production" and debug ? The only way I've found would be to > have 2 different repositories. For short-lived branches, I just use one clone per branch. I think this should work well for long-lived branches too, but I haven't tried. I think the developers are working on support for git-style lightweight branches, so this may eventually be the answer to your question. (Personally I like the simplicity of the one-clone-per-branch approach.) -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Tue, Jan 26, 2021 at 08:49:30PM +0100, Ben Franksen wrote:
> Am 24.01.21 um 12:03 schrieb Ben Franksen:
> > A /realization functor/ R is a functor from abstract patches (sequences
> > of names and contexts) to concrete patches (with a commute function),
> > such that
> >
> > (a) R maps abstract paths to concrete paths of the same length
> > (b) for any two parallel abstract paths ns and ms of length 2,
> > commute(R(ns))=Just(R(ms)) (here R is the mapping on arrows)
> > (c) there is a distinguished state E, such that E is an element of
> > R({}) (here R is the mapping on objects i.e. contexts)
This seems reasonable. For (b) I guess you mean any two /different/
paths of length 2?
> I just realized (pun, haha) that this functor has a name in Darcs: we
> call it 'effect'. I think I like that name better.
>
> Here is my picture of the overall structure of patch theory, when
> extended to the lower levels. We have three categories: abstract patches
> (AP), concrete patches (CP), and partial bijections (PB), and two functors:
>
> AP ---effect--> CP ---apply--> PB
>
> (While PB is a groupoid, CP is not, contrary to what I stated in my last
> mail, because that would mean pp^:s->s = id_s, which does not play well
> with commutation).
>
> The effect functor is understood to be relative to some choice of start
> state, see condition (c). Neither functor is injective (on morphisms;
> for objects I haven't checked this). I don't think the apply functor is
> surjective in any strict sense, but we should reasonably expect that for
> any two states s and t there is an arrow p in CP such that apply(p) is
> defined at s and apply(p)(s)=t. Indeed, the treeDiff function in Darcs
> gives a possible solution (the result depends on which diff algorithm is
> selected).
Thanks, this clears things up a bit for me. I hadn't realized you meant
CP and PB to be different, which might explain my confusion about
"patch theories that violate (b)" from my previous email.
One nitpick: the definition of "sensible" in the inverse semigroup
paper might be different from yours and from the Camp definition.
Definition 1.8 says a patch is sensible if it's effect isn't "0", which
I think just means its domain and range are nonempty.
Let me check my understanding of the picture you've painted:
* A "patch theory" or maybe "implemented patch theory" is a tuple
(State, Name, E, AP, CP, PB, commute, effect, apply) satisfying all
the following conditions.
* State and Name are sets, intended to denote the set of possible
states and names respectively. (E.g. type State = [Char] in your Jan
24 email.)
* E is an element of State: the "starting state".
* AP we've discussed a fair bit. It is a category. Its objects are
subsets of Name, its morphisms are labelled with sequences of names,
and we've previously listed some axioms AP must satisfy.
* PB: the objects are all possible subsets of State, and the morphisms
between any two objects are all possible bijections between those
sets. (PB is fully determined by the set State, so it could be left
out of the tuple defining the patch theory.)
* CP I'm less sure about. I guess it is any category whose objects are
the same as PB's objects. There are no constraints on its morphisms
other than what will be implied by our requirements on the effect
functor.
As a concrete example, in your toy patch theory, the morphisms in CP
between any objects S and T are triples (S, T, e) where e is an
element of [PrimPatch] for which apply(e)(S) = T (applying a function
to a set in the natural way). I include S and T as part of the
morphism so that the same e can appear in different morphisms.
Concatenating two morphisms (S, T, e) and (T, U, f) produces (S, U, e
++ f). The identity on S is (S, S, []).
* commute is a partial function on length-two paths in AP. (Maybe
"commute" could be out of the tuple, and instead be implied by the
effect functor. I haven't checked that this makes sense.)
* effect : AP -> CP is a functor satisfying the properties (a), (b) (c)
from your Jan 24 email ("realization functor").
* apply : CP -> PB is any functor.
Introducing conflictors to such a patch theory would mean the
following:
* Extending AP so the set of objects ("contexts") is closed under
union.
* Adding new morphisms to CP, called "conflictors".
* Extending the effect functor so it's defined on the newly expanded
AP, probably using the "conflictor" morphisms added in the previous
step.
* Extending the apply functor so it's defined on the morphisms
(conflictors) added to CP.
The first is a deterministic change; no decisions are required. The
rest requires careful design.
> The effect functor is surjective only if we restrict CP to sequences
> that are "sensible" relative to the chosen start state. For any sensible
> concrete patch sequence cp there is a sequence of names ap such that
> effect(ap)=cp, since this is precisely the condition under whic
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
Hi Ben,
Happy 2021! I let this thread drop for a while but trying to catch up now.
I think we had defined an abstract patch theory as a set of names, and
a set of possible "contexts" which are sets of names (or corners on the
hypercube), where the set of possible contexts satisfies (copying and
pasting from my earlier email):
(a) The empty set is a context.
(b) If c1 and c2 are contexts, then c1 ∩ c2 is a context.
(c) If c1, c2, c3 are contexts and c1 ⊆ c3 and c2 ⊆ c3, then c1 ∪ c2 is
a context.
(d) For every non-empty context c there is at least one element n of c
such that c\{n} is also a context.
This can be turned into a category: take your definition of an abstract
patch as a pair (c,n) (c is a context and n is a name) and then take
the free category over that.
Then the discussion turned to concrete representations of patches.
Long-winded (sorry) question below...
> > I'm not sure I understand. I guess a state is the content of the files
> > in the repository.
>
> Plus the directory structure. One concrete representation of states is
> the 'Tree' type in Darcs, see
> https://hub.darcs.net/darcs/darcs-screened/browse/src/Darcs/Util/Tree.hs#59
> up to line 84.
Yes, that makes sense.
> > Any concrete patch has exactly one start state and
> > one end state.
>
> Not at all. Unnamed prim patches can be applied to many states, indeed
> the domain is always infinite. For instance the domain of "addfile ./f"
> is the set of all trees which do not have "./f" as either file or
> directory. Its codomain is the set of all trees that do have "./f" as a
> file. Its inverse is "rmfile ./f" with domain and codomain swapped.
>
> > Do you mean that it's a partial bijection where the
> > domain and range are both sets of size 1?
>
> No, see above.
>
> > E.g. suppose the concrete patch P is:
> >
> > hunk ./file.txt 2
> > +world
> >
> > and in the context of p, file.txt has just one line "Hello".
> > I guess it's tempting to think of p as the following partial bijection
> > f: f always inserts the line "world" after the first line of file.txt.
>
> This is exactly how the above hunk is interpreted in Darcs.
>
> > But that's not really a useful representation of p; e.g. it doesn't
> > work if p gets commuted to a different context.
>
> Why not? If you commute the patch to a different context then its domain
> and codomain usually change, too. I would expect nothing less.
>
> But perhaps what you mean is that it is not a useful /generic/
> description of "what the patch does" /independent/ of commutation. This
> is true. If we had a representation of concrete patches that is truly
> context independent, then a lot of problems could be solved quite
> easily, see Pijul. In particular, I think we would not need names for
> patches.
>
> > So to me it makes more
> > sense to just say that concretely, p is the pair ("Hello\n",
> > "Hello\nworld\n").
>
> It is certainly possible to define hunks in this way. In Darcs, so
> called binary patches are defined in this way: they contain the old
> content and the new content.
>
> However, even if you do that, your hunks are still "polymorphic"
> relative to the "rest of the tree". And commuting such a hunk with a
> file rename patch may still have to modify the hunk.
>
> > I guess this is a long-winded way to just say I'm not sure what you
> > mean by concrete patches being bijections.
>
> As explained above, for each kind of prim patch in Darcs (hunk, binary,
> addfile, etc... but please ignore setpref patches) one can precisely
> define the set of trees that are their domain and codomain and they are
> designed so that the partial function defined by applying the patch is
> injective and thus can be inverted.
>
> > I guess you'd want to be able to commute concrete patches without
> > access to any information other than those two patches'
> > representations. Does your definition capture that?
>
> Absolutely. The full commute code for Darcs' prim patches is here:
> https://hub.darcs.net/darcs/darcs-screened/browse/src/Darcs/Patch/Prim/V1/Commute.hs.
> It could use a bit of streamlining but I think the overall picture of
> how commutation works on prim patches is recognizable.
I think I am closer to understanding what you mean by "concrete patch",
but I think I haven't got it completely.
Here's my understanding so far:
a) We begin with a set S of states. In the case of Darcs, that's the
Tree type.
b) A concrete patch is a bijection between two subsets of S. A
"concrete patch theory" gives a way of encoding some such bijections
as data. For example, every Darcs prim patch encodes such a
bijection, so Darcs prim patches (excluding names) are a "concrete
patch theory" in this sense.
c) If two Darcs prim patches are different (excluding names) then they
encode different bijections. This is probably not too hard to prove.
If it weren't true, Darcs wouldn't satisfy point (b) above.
d) Commuting two concrete patches (assuming it suc
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
> Interesting! So corners (potential contexts) have an inherent partial
> order, indeed they form a join-semilattice. You postulate that if two
> contexts have an uppper bound that is also a context, then the minimal
> upper bound must also be a context. I think the math term would be that
> contexts form a sub-semilattice of the corners.
I should credit my friend Sridhar Ramesh here. I was asking them
whether there's a name for some property involving pushouts, and
casually mentioned we might not need to distinguish morphisms with the
same domain and codomain, and Sridhar pointed out that's just a
pre-order.
> It's funny how this brings us all the way back to the ideas in your
> first paper: instead of focusing on patches or paths, we now focus
> almost completely on contexts.
That's a good point.
I think there's a straightforward connection to the "pseudo-contexts" I
had before. A pseudo-context was a path together with a partition of
the names in the path into a "before" part and and "after" part. You
can translate that to a corner of the hypercube by taking the names in
the start node of the path, and adding in the names in the "before"
set. This at least captures the idea I had in mind that the
pseudocontext comes "after" that set of names.
On Mon, Dec 14, 2020 at 03:30:50PM +0100, Ben Franksen wrote:
> Am 13.12.20 um 11:16 schrieb Ben Franksen:
> > However, remember your counter example of a patch universe with only two
> > paths with names abc and cba. From the presence of both {a} and {c} we
> > can deduce that of {a,c}, but it seems impossible to prove that {b} is
> > present. For that we need a fifth axiom (e) analogous to (d) but with
> > intersections instead of unions:
> >
> > e) If nodes c1 and c2 are present, then c1 ∩ c2 is also present.
>
> This is still not quite insufficient. With the natural numbers as the
> set of names, b={}, and t={1,2}, the set C={b,t} would be a valid set of
> contexts. But then there is no path from b to t (in fact we have no
> patches at all). In general I think we want the patch graph to be
> connected. A possible characterization in terms of contexts could be:
>
> (f) For every non-empty context c there is at least one element n of c,
> such that c\\{n} is also a context.
>
> It is then easy to show that a path p:s->t exists if and only if s is a
> subset of t.
Good points. So now with some rephrasing, the rules on the set of
contexts are:
(a) The empty set is a context.
(b) If c1 and c2 are contexts, then c1 ∩ c2 is a context.
(c) If c1, c2, c3 are contexts and c1 ⊆ c3 and c2 ⊆ c3, then c1 ∪ c2 is
a context.
(d) For every non-empty context c there is at least one element n of c
such that c\{n} is also a context.
I haven't found a definition for "sub-semilattice" but maybe that word
could encompass some of the above.
> Another interesting observation is that we can regard a name as a
> partial bijection between contexts. The action of the function is to add
> the name to the context and its inverse is to remove it. Its domain and
> range are given by
>
> domain(n)={c∈C|n∉c and c∪{n}∈C}, range(n)={c∈C|n∈c and c\{n}∈C}
>
> The reason I find this interesting is that it hints at a possibility to
> re-introduce /concrete/ patches (that is, /patch content/) into the
> picture. Concrete (primitive) patches can be seen as partial bijections
> on a set S of states, represented as data.
I'm not sure I understand. I guess a state is the content of the files
in the repository. Any concrete patch has exactly one start state and
one end state. Do you mean that it's a partial bijection where the
domain and range are both sets of size 1?
E.g. suppose the concrete patch P is:
hunk ./file.txt 2
+world
and in the context of p, file.txt has just one line "Hello".
I guess it's tempting to think of p as the following partial bijection
f: f always inserts the line "world" after the first line of file.txt.
But that's not really a useful representation of p; e.g. it doesn't
work if p gets commuted to a different context. So to me it makes more
sense to just say that concretely, p is the pair ("Hello\n",
"Hello\nworld\n").
I guess this is a long-winded way to just say I'm not sure what you
mean by concrete patches being bijections.
I guess you'd want to be able to commute concrete patches without
access to any information other than those two patches'
representations. Does your definition capture that?
> Here, too, we can generalize
> to finite sequences of patches, which then naturally form a category,
> and there is a (non-injective) functor (the "apply" functor) from that
> category to the groupoid of partial bijections on states that maps
> concatenation to function composition.
>
> We may want to study functors from an abstract patch theory to a
> concrete one.
That's neat.
> A functor maps both objects and arrows. For objects,
> F:C->S associates a concrete state to each context (this mapping is also
> not necessarily injective). For arr
Re: [darcs-users] If AB and B' are repos, does that imply A and B commute?
On Sat, Dec 12, 2020 at 10:09:23PM +0100, Ben Franksen wrote: > Am 12.12.20 um 18:54 schrieb James Cook: > >>> As far as I can tell, the example is consistent with the patch theory > >>> axioms in [0] and [1]: we can simply say that in our patch theory, > >>> nothing ever commutes, and then the axioms don't have much to say. > >>> > >>> The Camp theory pdf [2] makes a claim that seems to rule out the > >>> example: in section 8.1, "Merge preparation", it's asserted that as a > >>> first step toward merging two repos, we can move the common patches to > >>> the beginning. In this case, that would imply B can be moved to the > >>> beginning of the repo AB. However, I'm not sure where that's proved, > >>> and I also can't see why the above situation is inconsistent with the > >>> axioms in that write-up. (Admittedly, I haven't read it completely --- > >>> if someone can point me to the right parts, I'd appreciate it.) > >> > >> The property you need to rule this out is a global one: you must assume > >> that each newly recorded patch has a universally unique name. The patch > >> laws are all local properties, so they cannot give you that. > >> > >> Darcs tries to ensure this by adding a random number (taken from system > >> entropy i.e. cryptographically secure, as far as that is possible) to > >> the patch name when a patch is recorded (or amended etc). But it is > >> clear that this is no guarantee, since it cannot prevent someone from > >> manually creating a patch that has the same identity as a completely > >> unrelated patch somewhere else. If you pull such a patch, you repo > >> invariants are broken and you may get crashes (or worse: inconsistent > >> behavior). > >> > >> This is a great, perhaps the greatest, weakness of patch theories a la > >> Darcs. We have discussed this at great length during the past years on > >> darcs-devel in varying contexts. It crops up again and again. > > > > If we could easily commute a patch to its minimal context, would that > > solve the problem? > > Yes. > > > (E.g: the name of the patch is a hash of all the > > names in its minimal context together with the content of the patch > > when commuted to that minimal context.) > > Yes, exactly. > > > I remember you said earlier that there is no known way to efficiently > > compute that minimal context. Also, even if it were known, commuting > > the patch to that context could be expensive. Are those the reasons > > that scheme doesn't work? > > Yes. > > > Here's a sketch of an idea to try to overcome the computational > > concern, inspired by pijul. I don't know if it works because the > > details are lacking. (Also I wouldn't be surprised if something like > > this has already been discussed; this doesn't feel very original.) > > I don't think an idea like this has been floated before in the context > of Darcs. I think one reason for this may be that even if we could > compute minimal contexts for prim patches, we'd still have to extend > that to conflictors and then to the named "changeset" patches. But for > your tree patch model it may be enough to consider prim patches. > > Regarding Pijul, I think the decisive difference is that their patches > are such that they don't change at all when they are commuted. For > instance, a hunk that adds some lines does so by referring only to the > UUIDs of the lines before and after. And since the UUIDs are immutable a > patch never has to be adapted. Commutation is then merely a question of > determining /if/ commutation is allowed, and that information is of > course cached in the database. And since the patches never change, > minimal contexts aren't needed, since we can simply hash the (unique) > patch content and be done with it. I guess I was hoping there could be some limited sort of equivalence between Darcs hunks and pijul patches, which would allow Darcs to internally manage some things much closer to the way pijul does, without changing Darcs's outward behaviour except by fixing the naming problem. But it's just hot air from me at this point. Maybe I'll try to hack together a demonstration in the future if I have time. -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] If AB and B' are repos, does that imply A and B commute?
On Sun, Nov 22, 2020 at 10:08:45AM +0100, Ben Franksen wrote: > Am 21.11.20 um 20:39 schrieb James Cook: > > I've been trying to put together a proof, and ran into a strange > > example: what if AB and B' are both repositories, but A and B don't > > commute? I.e. A can only be applied if B hasn't been applied yet, but B > > doesn't depend on A. > > > > My questions: Is this situation disallowed by some existing patch > > theory formalization? Is there a good reason to rule it out? Is it > > actually possible in Darcs? (I doubt the last one.) > > TL;DR: > > I don't believe that any existing text on patch theory has ever fully > formalized this requirement, but I may be wrong e.g. the camp paper may > have. (It's been quite a while since I last looked at the paper.) > > There are very good reasons to rule this out, indeed it is essential to > do so, otherwise there is no point in naming primitive patches. > > It is possible in Darcs, but only if you manually craft patches and not > with darcs commands, unless you are exceptionally unlucky ;-) > > > As far as I can tell, the example is consistent with the patch theory > > axioms in [0] and [1]: we can simply say that in our patch theory, > > nothing ever commutes, and then the axioms don't have much to say. > > > > The Camp theory pdf [2] makes a claim that seems to rule out the > > example: in section 8.1, "Merge preparation", it's asserted that as a > > first step toward merging two repos, we can move the common patches to > > the beginning. In this case, that would imply B can be moved to the > > beginning of the repo AB. However, I'm not sure where that's proved, > > and I also can't see why the above situation is inconsistent with the > > axioms in that write-up. (Admittedly, I haven't read it completely --- > > if someone can point me to the right parts, I'd appreciate it.) > > The property you need to rule this out is a global one: you must assume > that each newly recorded patch has a universally unique name. The patch > laws are all local properties, so they cannot give you that. > > Darcs tries to ensure this by adding a random number (taken from system > entropy i.e. cryptographically secure, as far as that is possible) to > the patch name when a patch is recorded (or amended etc). But it is > clear that this is no guarantee, since it cannot prevent someone from > manually creating a patch that has the same identity as a completely > unrelated patch somewhere else. If you pull such a patch, you repo > invariants are broken and you may get crashes (or worse: inconsistent > behavior). > > This is a great, perhaps the greatest, weakness of patch theories a la > Darcs. We have discussed this at great length during the past years on > darcs-devel in varying contexts. It crops up again and again. If we could easily commute a patch to its minimal context, would that solve the problem? (E.g: the name of the patch is a hash of all the names in its minimal context together with the content of the patch when commuted to that minimal context.) I remember you said earlier that there is no known way to efficiently compute that minimal context. Also, even if it were known, commuting the patch to that context could be expensive. Are those the reasons that scheme doesn't work? Here's a sketch of an idea to try to overcome the computational concern, inspired by pijul. I don't know if it works because the details are lacking. (Also I wouldn't be surprised if something like this has already been discussed; this doesn't feel very original.) For simplicity, assume prim patches are all hunks and the repo is one text file. For every primitive patch in the repo, keep track of an interval of lines "touched" by the patch. When a patch p is first applied, its interval is the lines it added (and maybe one extra line before and after). As hunks are added, p's interval is adjusted in some appropriate way. If lines from the beginning or end of p's hunk are deleted or replaced by a later patch, p's interval shrinks. Eventually, p might be reduced to the empty interval, but we still keep track of the interval even then --- we think of p as living "between" two lines of the file. This is important because any later patch that touches that region depends on p. Updating every interval every time a patch is added could be expensive. Maybe this could be mitigated by assigning unique identifiers to the lines of the file, and recording the intervals in terms of those identifiers. Could these "touched" intervals be used to compute a minimal context for a new patch? The patch's name could be a hash of four things: that minimal context; the lines added; the unique ID of the line before the hunk is added; and metadata like the user-supplied description. -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Sat, Dec 12, 2020 at 02:32:07PM +0100, Ben Franksen wrote:
> Am 12.12.20 um 11:56 schrieb Ben Franksen:
> > Another aspect not covered is that for permutivity to hold, we need not
> > only ensure a /minimum/ number of parallel paths, but also a /maximum/
> > number of intermediate contexts. The extreme case is the commuting
> > hypercube of dimension n with n! different paths of length n (all
> > permutations of n), sharing 2^n contexts (the corners of the hypercube).
>
> Indeed, it should be possible to embed (inject) any patch graph into an
> N-dimensional hypercube, where N is the set of natural numbers. I find
> this view quite illuminating.
>
> (We have to restrict names and contexts to (at most) countable sets,
> which is not a serious limitation, since this will be the case in any
> practical implementation anyway.)
>
> The contexts correspond to corners i.e. elements of {0,1}^N, and the
> patches correspond to edges. Edges representing patches are considered
> directed "away from the origin". The names are the (mutually orthogonal)
> "directions" in our space: two patches have the same name if and only if
> they are /geometrically/ parallel as edges.
>
> We even get a distinguished "empty context" for free (the origin).
>
> Corners can be seen as sequences of bits (with only finitely many 1s),
> and a patch p:s->t with name m corresponds to the triple (s,t,m) where
> s(m)=0, t(m)=1, and s(i)=t(i) for all names i with i/=m.
This is similar to my attempt #2 from yesterday's email (in that
formulation, a context is a set of names, which could be thought of as
an element of {0,1}^N if you prefer).
> Given two arbitrary corners s and t, all paths p:s->t must have the same
> length n, which coincides with the size of name(p). In other words, they
> lie inside a finite n-dimensional hyperface of the full N-cube.
>
> What does permutivity mean in this picture? Or asked differently, how
> can we characterize the valid patch graphs as a subset of the N-cube?
>
> Cheers
> Ben
Translating my attempt #2 to these terms, I propose this
characterization:
a) First, we only use a subset of the nodes of the hypercube. Each node
is either "present" or not. (Think of a "not present" node as
representing a set of names with at least one conflict.)
b) The all-zero node is present.
c) An edge/patch exists iff its start and end nodes are present.
d) If nodes c1, c2, c3 are present, and c1 ⊆ c3 and c2 ⊆ c3, then
c1 ∪ c2 is also present.
For example, I think we can prove the following property from your
previous email:
[for any parallel paths p and q] for every n in name(p)=name(q), and
for each i in pos(p,n)..pos(q,n), there exists a parallel path r,
such that i=pos(r,n).
Proof:
Without loss of generality, assume pos(p,n) <= pos(q,n).
Write p = p0 a p1 and q = q0 a' q1 where name(a) = name(a') = n. So
length(p0) = pos(p,n) and length(q0) = pos(q,n).
Let q0' be a prefix of q0 such that |name(q0') ∪ name(p0)| = pos(q,n).
Let X = name(q0') ∪ name(p0). By property (d), node X is present in the
patch theory (taking c1 = end(q0'), c2 = end(p0), c3 = end(p) = end(q).
X ∪ {n} is also present, again by property (d) (taking c1 = end(q0') ∪
{n}, c2 = end(p0) ∪ {n}, c3 = end(p) = end(q)).
By Lemma 1 (below) there exists a path from start(p) to X, and also a
path from X ∪ {n} to end(p). By property (c), there's also an edge from
X to X ∪ {n} (with name n). Concatenate these three to get the desired path.
QED
Lemma 1
If the nodes/contexts c and d are present and c ⊆ d, there is a path
from c to d.
Proof
If c = d, take the empty path.
Otherwise, let n be any name in d \ c. By property (d), taking c1 = c,
c2 = c ∪ {n} and c3 = d, the node c ∪ {n} is present.
By property (c), there is an edge from c to c ∪ {n}. Use that as the
first edge of the path. Note that c ∪ {n} ⊆ d; we can apply the lemma
again (using induction) to complete the path.
QED
--
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Sat, Dec 05, 2020 at 06:50:45PM +0100, Ben Franksen wrote: > Hi James > > Thanks for your answers. It appears I had a completely wrong intuition > about what a tree patch is. I was under the impression that it roughly > corresponds to Darcs' named patches (changesets), but your definition > seems to be a lot more general. > > Cheers > Ben I went through a couple of simpler definitions before I settled on this one. Unfortunately the simpler definitions didn't have the properties I wanted (e.g. Corollary 2: there should be a tree patch corresponding to any merge resolution). I'm tempted to try implementing this. I'm not sure my current tree patch definition is the right choice, but maybe things will become more clear if I actually try to use them. Not sure if I'll have time, though. -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
> You are right. Such a scenario must not be allowed and the "global"
> definition of patch graph I gave is too weak to exclude it. If you
> analyse the counter example from the POV of permutations of names, what
> we have here is (indeed the simplest example of) a permutation group
> that is not generated by adjacent transpositions. If we build a patch
> theory bottom-up starting with commutation of single patches, then this
> cannot happen: the set of parallel paths from s to t always maps to a
> permutation group that is generated by adjacent transpositions.
>
> So one way to "fix" the theory could be to add that as a requirement.
> Formally, consider the map from paths to sequences of names. For each
> pair (s,t) of contexts, the image of the set of parallel paths from s to
> t under this map can be regarded as a subset of S_N (where N is the
> common path length). The requirement is that this is a subgroup
> generated by adjacent transpoisitions.)
I think something like that would work. I don't think describing it as
a "subgroup" works exactly. For one thing, the elements of the set are
sequences of names, which are not themselves permutations. You could
pick one "canonical" ordering and identify each other sequence with the
permutation that re-orders the canonical ordering into it, so at least
you have a set of permutations, but I don't know if it will be a
subgroup.
> At least I *think* that would fix the theory, i.e. allow to prove my
> conjectures about merges. However, it feels a bit heavy-weight and I
> would prefer a more elegant way to express this requirement.
Here are three more attempts. Not necessarily better than yours, but
maybe food for thought.
1.
I suspect the following two properties together may be equivalent to
(a fixed-up version of) your permutation-subgroup property:
a) name(pq') = name(p) U name(q) whenever pq' is a clean merge of p and
q (defining a clean merge as a pushout, as before).
b) Rule out this diagram:
> > *
> > a/ \b
> > / \
> >* *
> > d/|c c'|\d'
> > / | | \
> > * * * *
> > | \ / |
> > | b'\ /a' |
> > | * |
> > \ /
> > \ /
> > b''\ /a''
> > \ /
> > \ /
> > *
by saying that for every commuting square
*
a/ \b
/ \
* *
\ /
\ /
*
the pushout (clean merge) of a and b exists.
I haven't fully worked out a proof that (a) and (b) is equivalent to
something about transpositions, but it seems likely to be true. Maybe I
should think about it more.
2.
This is a more radical change, so I'll start from the beginning.
A patch theory consists of:
* a set N of names, and
* a set C of sets of names (i.e. C is a subset of the powerset of N)
(elements of C are called "contexts")
such that C contains the empty set, and for any c1, c2, c3 in C, if
c1 ⊆ c3 and c2 ⊆ c3, then c1 ∪ c2 is an element of C.
That's all. But we need to connect this to more familiar terms...
If we like, we can view this as a category using the order relation ⊆.
Specifically: the objects are contexts, and there is a single morphism
from c1 to c2 if c1 ⊆ c2, otherwise none.
A "patch" is just a morphism between two contexts that differ by the
inclusion of one name.
This is similar to your category view. The difference is that patch
sequences can no longer represented as morphisms (unless you're willing
to forget the order). Of course this doesn't prevent us from talking
about patch sequences.
3.
#3 is just a rephrasing of 2 to be more compatible with your
categorical point of view.
Define N and C as in 2 above (including the requirements I imposed on
C).
Define a graph G as follows. The nodes are all elements of C. The edges
are all pairs (c1, c2) where c2 and c1 differ by the inclusion of one
name (c2 = c1 ∪ {n}); the edge is labelled by that name n.
Define the free category on G as in your original formulation. Note
that the name of any path will just be the set difference of its
endpoints, so your requirement that parallel paths have the same name
is satisfied. The additional requirements on the set C (taken from #2)
will hopefully ensure that clean merges behave well.
--
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Tue, Nov 24, 2020 at 10:55:22PM +, Ganesh Sittampalam wrote: > Hi, > > On 24/11/2020 21:43, James Cook wrote: > > I wrote a description of how to store a repository as a tree of > > primitive patches with active and inactive branches, as an alternative > > to conflictors. For context, see recent discussion on the thread > > "How to extend a patch theory to fully commute". > > FYI I remember Petr Ročkai (mornfall) had a similar idea about > deactivating patches many years ago, but I can't remember any of the > details nor can I find what he wrote after searching online a bit. > > So this isn't a very helpful comment except perhaps as a pointer in case > someone else does a better job searching than me. > > Cheers, > > Ganesh Recording for the list: On IRC, mornfall found a link to the writeup in question: http://darcs.net/Ideas/NewRepositorySemantics They also pointed to a later idea they had which is written up at http://paradise.fi.muni.cz/~xrockai/dvs.html, with a note to "ignore the bit about whitespace on edges, that turned out to be a bad idea". -- James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Thu, Nov 26, 2020 at 02:32:08PM +0100, Ben Franksen wrote:
> Regarding Section 4.11, let me reformulate the main definition to make
> it a bit less awkward.
>
> A patch with name n is inactive with respect to a set of tree patches S
> if it is deactivated by any tree patch (P,D) in S (i.e. n is in D),
> subject to the side condition that there exists no patch name m (in any
> tree patch in S) that depends on n but is independent of P (that is, not
> included in P's dependencies).
>
> In other words, m re-activates n if it depends on n and is not depended
> on by any of the tree patches that deactivate n.
That sounds right. I tried to capture something like it in the sentence
following Definition 20. Maybe I could improve Definition 20 itself,
or move that sentence inside the definition, before the math.
> Suppose m depends on n and n is deactivated by a tree patch (P,D) i.e. n
> is in D. I wonder about the side condition and what it implies.
>
> If P depends on m, then there is a p in P that depends on m.
>
> Doesn't that imply that such a p is also a member of D?
Maybe it ought to, but under the current definitions it doesn't.
For one thing, a tree patch that results in an "impossible" signature
is still a tree patch. Continuing your example, if suppose we had the
tree patch repository
n m
*-->*-->*
with the single tree patch (P = {n, m}, D = {})
Then (P = {p, n}, D = {n}) fits the definition of "tree patch", even
though adding it to the repo would result in the impossible signature
(P = {n, m, p}, A = {m, p}).
But even if we say a tree patch cannot be applied if it results in an
impossible signature, there's still a counterexample. If we start
instead with
*
| n
v
*
| m
v
*
| p
v
*
with tree patch (P = {n, m, p}, D = {n, m, p}) (i.e. everything's
already deactivated) then adding the tree patch (P = {p, n}, D = {n})
would not change the signature.
> And that m is also in P, since n is in D which is a subset of P?
Why? Note that Definition 20 doesn't put any constraints on P.
> Also, is it true that m can reactivate another patch n only if m is active?
No. For example, if we start with just
*
| n
v
*
where n is inactive, the tree patch (P = {m}, D = {m}) re-activates n
even though m is inactive. You could also use (P = {n, m}, D = {m}).
> Cheers
> Ben
--
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Thu, Nov 26, 2020 at 02:12:56PM +0100, Ben Franksen wrote:
> I would start the whole thing with a slightly different definition.
This seems like a nice way to do things. I like the reuse of terms from
category theory.
Do you happen to know how much this has in common with "A Categorical
Theory of Patches" which pijul is based on? I have not read the paper
in detail, but I know they too talk about pushouts.
https://arxiv.org/abs/1311.3903
Maybe I should move my patch trees write-up to a separate document so
the old "Patch universes" stuff can stay where it is without getting in
the way.
A couple of comments below:
> We extend the three functions above to paths. The source of a path is
> the source of its first patch, the target is the target of its last
> patch, and the name of a path is the set of names of its patches:
> name(p1,...,pn)={name(p1),...,name(pn)}
>
> This is indeed an extension if we identfy a name with the singleton set
> consisting of just that name.
nit: The empty patch has no patches, so these definitions of source and
target don't work for it.
> We can define the clean merge of two paths as follows. Let p and q be
> paths with the same source. A clean merge of (p,q) is a then a pushout,
> in other words, another pair of paths (q',p'), such that pq' and qp' are
> parallel, and such that q',p' are minimal in the sense that for any
> other such pair (q'', p'') there is a unique path r such that q'',p''
> factors through r; that is, p''=p'r and q''=q'r. It follows from the
> defining property of a patch theory that name(pq')=name(qp'), but I
> think it should also be possible to deduce
>
> name(pq') = name(p) U name(q)
>
> using the universal property (minimality) of the merge. Indeed I think
> both definitions are equivalent. Note that any such merge must
> necessarily be unique (because pushouts are unique).
I think the following is a counterexample. Suppose this is the whole
patch theory. All edges go downward. a and a' have the same name and so
do b and b' and c and c'.
*
a/ \b
/ \
* *
|c|c'
| |
* *
\ /
b'\ /a'
*
In this case, the pushout of a and b is the whole diagram, so the merge
is acb' or bca', both of which include c's name.
Maybe an axiom could be added that name(pq') = name(p) U name(q)
whenever pq is a clean merge of p and q. I suspect it is strictly
weaker than my Assumption 4.1 but it is more succinct and maybe it is
enough.
(The example violates Assumption 4.1: conflict(a, b) must be true
because a and b can't be merged directly, but then the paths acb' and
bca' contain conflicting patches, which is not allowed. Maybe this can
be turned into a proof.)
Here's an example showing the name union axiom doesn't imply 4.1:
*
a/ \b
/ \
* *
d/|c c'|\d'
/ | | \
* * * *
| \ / |
| b'\ /a' |
| * |
\ /
\ /
b''\ /a''
\ /
\ /
*
Now there is no pushout of a and b, so the name union axiom has nothing
to say, but 4.1 is still violated.
> Cheers
> Ben
--
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Write-up on "tree repositories" as an alternative to conflictors
On Wed, Nov 25, 2020 at 12:53:24PM +0100, Ben Franksen wrote: > Two minor remarks. > > > 4.2.7 Reactivating a patch > > As promised in Section 4.1.3, it is possible to re-activate a previously > > deactivated patch p. First, it is likely the user will need to de-activate > > patches p conflicts with, as well as patches that conflict with p’s > > dependencies if those are also being re-activated. Section 4.2.6 explains > > how to deactivate these patches and the patches that depend on them. > > Obviously, dependencies of p /have/ to be reactivated along with p, so > the "if" is misleading here. Thanks; reworded: https://hub.darcs.net/falsifian/misc-pub/patch/2343bc9d163b31df5a5f29de85641ac4e71d645c (I originally put the "if" there since p's dependencies might already all be active.) > > • Insert p and its dependencies into the chosen resolution. We already have > > a copy of them somewhere: recall that a tree repository is a pair (T, C); T > > and C together contain all active and deactivated patches in the repository. > > Some commuting may be needed. (TODO: elabourate?) > > Indeed this should be elaborated! Hm, I think it would follow from something like the "weak converse" I mention in the Aside at the end of 4.2.1. Maybe I should turn that into a lemma and use it here. Note I haven't read your later emails yet; I'm not sure if you commented on 4.2.1. > Cheers > Ben > > ___ > darcs-users mailing list > darcs-users@osuosl.org > https://lists.osuosl.org/mailman/listinfo/darcs-users -- 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 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 resolut
[darcs-users] Write-up on "tree repositories" as an alternative to conflictors
I wrote a description of how to store a repository as a tree of primitive patches with active and inactive branches, as an alternative to conflictors. For context, see recent discussion on the thread "How to extend a patch theory to fully commute". It is Section 4 of this pdf: https://www.falsifian.org/a/xxOw/misc.pdf (I decided to add it to the end of the last pdf I sent to this list, but you can pretty much ignore the previous sections.) The tex source is at https://hub.darcs.net/falsifian/misc-pub/browse/patch_theory/misc.tex . I tagged this version as "2020-11-24_tree_repositories" but may push corrections. The write-up is pretty long. Part of that is because I put a long examples and motivation section at the start (Section 4.1); hopefully that at least should be easy to get through. Another reason is that my attempt in Section 4.2.11 to show you can view a "tree repository" as a set of "tree patches", in order to retain some of the advantages of "a repository is a set of patches" as in Darcs, turned out to be fairly complicated. I'm not completely satisfied with that section and listed a bunch of caveats at the end. -- 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 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 seque
Re: [darcs-users] If AB and B' are repos, does that imply A and B commute?
> Property: > > (Summary: any sequence of patch names can be realized as a sequence of > patches unless there's a specific conflict or violated dependency > preventing it.) > > Let N be the set of (positive) patch names and C(N) the set of finite > subsets of N. > > There exist: > - a function "minimal_context" : N -> C(N); > - a relation "conflict" on N x N; and > - a universal starting context "empty_repo" > such that the following properties hold. (Note that the above three > objects are independent of any particular repository, so I'm asserting > for example that minimal contexts are universal.) > > 1. conflict is symmetric (conflict(a,b) implies conflict(b, a)). > > 2. Consistency of minimal_context and conflict: > >For any names n1 and n2, at most one of the following is true: > >- n1 is in minimal_context(n2) >- n2 is in minimal_context(n1) >- conflict(n1, n2) > > 3. Let n_1, n_2, ..., n_k be a sequence of distinct patch names >satisfying the following: > >- No patches in the sequence conflict: for all 1 <= i < j <= k, > conflict(n_i, n_j) is false. >- Dependencies are satisfied: for all 1 <= i <= k, every element of > minimal_context(n_i) appears somewhere before n_i in the sequence. > >Then there exists a (unique) patch sequence P_1 ... P_k with names >n_1 ... n_k which can be applied starting at empty_repo. I should say two more things here: - P1 ... Pk does not include any conflictors. This property is intended to be about a primitive patch theory where we haven't added in conflictors. - The converse should also be asserted: if there are any conflicts or violated dependencies, then there is no sequence P1 ... Pk. Without this assertion, the property is trivially satisfied by saying all pairs of names conflict, i.e. "conflict" is the full product N x N. -- 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 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
[darcs-users] If AB and B' are repos, does that imply A and B commute?
I've been trying to put together a proof, and ran into a strange example: what if AB and B' are both repositories, but A and B don't commute? I.e. A can only be applied if B hasn't been applied yet, but B doesn't depend on A. My questions: Is this situation disallowed by some existing patch theory formalization? Is there a good reason to rule it out? Is it actually possible in Darcs? (I doubt the last one.) As far as I can tell, the example is consistent with the patch theory axioms in [0] and [1]: we can simply say that in our patch theory, nothing ever commutes, and then the axioms don't have much to say. The Camp theory pdf [2] makes a claim that seems to rule out the example: in section 8.1, "Merge preparation", it's asserted that as a first step toward merging two repos, we can move the common patches to the beginning. In this case, that would imply B can be moved to the beginning of the repo AB. However, I'm not sure where that's proved, and I also can't see why the above situation is inconsistent with the axioms in that write-up. (Admittedly, I haven't read it completely --- if someone can point me to the right parts, I'd appreciate it.) In practice, I suspect it can't happen in Darcs, but I could imagine maybe someone would want a patch theory where it's possible. For example, maybe A reverses the order of lines in a file, and B deletes that file. I'm interested in this because I think the following property would be useful for reasoning about repositories, but the example contradict it. Property: (Summary: any sequence of patch names can be realized as a sequence of patches unless there's a specific conflict or violated dependency preventing it.) Let N be the set of (positive) patch names and C(N) the set of finite subsets of N. There exist: - a function "minimal_context" : N -> C(N); - a relation "conflict" on N x N; and - a universal starting context "empty_repo" such that the following properties hold. (Note that the above three objects are independent of any particular repository, so I'm asserting for example that minimal contexts are universal.) 1. conflict is symmetric (conflict(a,b) implies conflict(b, a)). 2. Consistency of minimal_context and conflict: For any names n1 and n2, at most one of the following is true: - n1 is in minimal_context(n2) - n2 is in minimal_context(n1) - conflict(n1, n2) 3. Let n_1, n_2, ..., n_k be a sequence of distinct patch names satisfying the following: - No patches in the sequence conflict: for all 1 <= i < j <= k, conflict(n_i, n_j) is false. - Dependencies are satisfied: for all 1 <= i <= k, every element of minimal_context(n_i) appears somewhere before n_i in the sequence. Then there exists a (unique) patch sequence P_1 ... P_k with names n_1 ... n_k which can be applied starting at empty_repo. [0] Ganesh Sittampalam et al. "Some properties of darcs patch theory". November 7, 2005. Downloaded 2020-11-21 from https://urchin.earth.li/darcs/ganesh/darcs-patch-theory/theory/formal.pdf [1] Judah Jacobson, "A Formalization of Darcs patch theory using inverse semigroups". Downloaded 2020-06-21 from ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf [2] Camp theory.pdf, downloaded 2020-06-21 from https://archives.haskell.org/projects.haskell.org/camp/files/theory.pdf -- 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
> > 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
> >> 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
> 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 darcs-users@osuosl
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] RFC: Hiijacking Patches
On Fri, 25 Sep 2020 at 10:48, Ben Franksen wrote: > Hi Everyone > > I am thinking about changing the behavior and/or available options for > hijacking patches. > > Context: When working from home I have two identities in my > ~/.darcs/author file: one with my work email address and one with my > private email address. I want to decide which one to use per repo, once. > This works fine with the record command: darcs remembers the chosen > identity in _darcs/prefs/author and does not ask me again (for this > repo). But it does not work this way with amend or rebase i.e. when > (potentially) hijacking patches. > > As I see it, there are basically three options that make sense: > > (a) keep the original author > (b) change the author as specified via command line > (c) behave similar to 'darcs record': > * change the author to the default author > (either _darcs/prefs/author or else ~/.darcs/author) > * if there is no default author, prompt the user to specify one > * if there are multiple authors, prompt the user to select one > * in each case, remember the choice in the repo > > Currently (a) is the default behavior and (b) can be chosen by passing > --author . (c) is not implemented; instead we have > --select-author which does not remember the choice and does not check if > we have already made a choice (for this repo). IMO this is not very > useful. I guess it is quite uncommon that a user wants to edit a patch > with an author that is different from both the original author and her > chosen default identity for the project; in this uncommon case it would > be okay to require the user to specify the identity explicitly using > --author. > > Thus, I propose we change --select-author in such a way that it behaves > as option (c) above. > > This change is not 100% compatible, so I'd like to have feedback on > whether you think this would hurt. > > A more disruptive but ultimately more consistent alternative would be to > make option (c) the default behavior, and require an explicit command > line switch --keep-author to get behavior (a), similar to the existing > --keep-date option. The --select-author option could then be used to > override a previous --author or --keep-author in case a user has set one > of these options in their ~/.darcs/defaults. Is hijacking patches a common operation for anyone? The least surprising behaviour would be to always ask the user what to do if they haven't explicitly chosen an option on the command line; I'd certainly prefer that. But I've never needed to hijack a patch, so take my opinion with a grain of salt. 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
> 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
> > 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 t
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
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
> 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 wr
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
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
> > 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
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 c
[darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
Hi darcs-users, I'm trying to learn more about how darcs force commutes work. What I'd like to do is create a repository R1 with patches A and B, and then look at the patches that result if A and B get force-commuted. E.g. if I could pull just patch B and not A to a new repository, I think that would do the trick, but of course darcs pull won't let me do that because B depends on A. Question 1: Is there a simple way to make darcs do this? I can think of two complicated ways, which I might resort to: (a) Play with the darcs source code. (b) Set up contrived situations involving merges to force darcs to do the force-commutes I'm looking for. Question 2: Is there a way to make "darcs changes" show the patch contents? For now, I've been manually examining files in _darcs/patches. I vaguely remember there's an option to darcs changes or a related command to show the patch contents, but I can't seem to find it now. Thanks, 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 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
> > 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
> > 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
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
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
> 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
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
> 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
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
[darcs-users] How to extend a patch theory to fully commute
== Prologue ==
This is a story about how to extend a patch theory into one where any
sequence of patches can be permuted into any other order.
In particular, this means every merge is a clean merge in the new
theory. One small catch: after a conflict, it's not possible to continue
applying ordinary patches until a special "mark resolved" patch has been
applied to return the repository to a normal state (i.e. a context that
exists in the primitive patch theory). As explained in the remark at the
end, this could be viewed as an advantage, since it helps determine
whether pulling in additional conflicting patches should be considered a
new conflict, or just adding more to the current conflict.
It's long. I'd be happy to get comments even if you've only read a
prefix, and feel free to skip the story parts and just read the
definitions, propositions etc. The main idea is minimal context
addresses, defined in the first two chapters; the rest mostly seems to
fall out of that naturally.
Caveats: I've marked a few places I'm not sure about with the words
"Conjecture" or "Assumption". I suspect Assumption 2 in particular may
be false in the case of Darcs 2 due to duplicate patches, but maybe that
can be addressed somehow. Besides that, this is probably full of
mistakes, and turn out to just not work for some reason. The notation
and proofs are kind of dense. Sorry about that.
The setting: there's a universe of primitive contexts C, and a universe
U of primitive patches which go between contexts in C.
Now, suppose we have a sequence of n patches P1 ... Pn, and the n+1
contexts c0 ... cn which go between them. Our goal is to be able to
permute the patches at will.
== Chapter 1: Context Addresses ==
We begin by extending the set of contexts beyond C. To understand how
this works, let's follow the voyages of Vice Captain (VC) D'Arcs as she
sails the HMS Patchfinder from c0 to cn.
There is an old and well-mapped passage from c0 to cn via the patches P1
... Pn in order. Most VCs are content to follow that when making the
trip, stopping at Contexts c1 ... c(n-1) along the way, where the locals
have well-established businesses restocking ships passing through. Each
context has its own (usually unique) character and appearance,
technically called a Repository State.
VC D'Arcs, unlike the others, likes to use her knowledge of Commutation
to plot a new path from c0 to cn each time. Commutation allows her to
build new sequences of patches Q1 ... Qn, with the same names as P1 ...
Pn but in a different order.
When she follows a new sequence, she finds new contexts along the way.
One month, following a particularly difficult permutation, she came
across a context with an old and beautiful tradition of wireframe
sculpture which the locals claimed had magical properties. She keeps in
her quarters a top in the form of a wireframe cube that she obtained on
that trip.
When a newly-discovered context is notable, VC D'Arcs keeps a record of
its location. She does this as follows: first, she records the overall
starting and ending contexts c0 and cn, and the standard route P1...Pn.
Then, she records the set of names of patches she followed to get from
c0 to that new context (call the new context d).
Definition: A /context address/ is a tuple (a, b, (Qi), X, Y), where a
and b are (primitive) contexts, (Qi) is a sequence of patches going from
a to b, and X and Y are a partition of the names of the patches in (Qi).
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|.
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").
Conjecture 1: Every context address points to at most one context.
== Chapter 2: Pseudo-Contexts and Minimal Addresses ==
VC D'Arcs respects the limitations of commutation. Sometimes, a
particular permutation of the patches P1 ... Pn is impossible.
Late one night, D'Arcs put her apprentice Pseudo in charge of navigation
and retired to her quarters. As she drowsily spun her cube-shaped top,
she thought about what strange new contexts she might encounter if she
were able to follow an impossible permutation.
In the morning, she emerged on deck to a strange sight. The Patchfinder
had arrived at a context that looked almost the same as the one they
should have arrived at (context ci), but it had a ghostly, shimmering
quality to it. The repository state was exactly the same as ci's, but
this context had a
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> It had never occurred to me to think of that as a possible solution. > Sometimes it helps to get input from someone who is not as deeply > involved and who can come up with fresh ideas. Many thanks for sharing them! Glad it turns out to be at least plausible. Thanks for taking the time to respond to all my questions so far. James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> Another problem is that even supposing commutation does not change prim > patches, in darcs you still have conflictors. And conflictors > /definitely/ have to change representation when we commute them: the > merge-commute law obviously requires that. Could the conflictors be re-computed? In more detail: Suppose we've managed to make it so primitive patches never change representation. I tell you I built my repo by pulling the primitive patches A, B and C in some arbitrary order, changing them into conflictors when necessary. (I might also have done some other operations, like adding and later obliterating patches, or commuting things.) I also tell you that the final order of patches in my repo is AB'C', where B' is either B itself or a conflictor keeping B's identity (and same for C'). Could there ever be more than one possible answer for what B' and C' end up being? If not, doesn't that mean that the identities of A, B and C are enough to verify we've got the same repo? I take your point, though, that maintaining metadata in the repository state, as required for all this, would be hard. > > In theory, you could > > even allow plugins that implement new patch types, with the basic > > principle that patches communicate with each other through > > modifications to the repo metadata. > > That may be possible, especially for a completely new project that is > designed around these notions from the start. Sorry to extend this tangent even further (if you keep responding to my emails, I'll likely keep sending them :-P), but I had another thought: you don't actually need to store the metadata with the repo state. You could instead put some metadata into the patches, and allow patches to modify each others' metadata when they try to commute. Well, at least I think it would work... let me know if you want details. This loses global uniqueness (since patch metadata changes when commuting), but might help (a) if you want to allow plugins but don't want to deal with metadata being part of the repo state, or (b) if you're trying to reason about a complicated primitive patch theory and want a way to avoid considering n^2 cases. (Based on your email, it sounds like (b) is not a practical concern, though.) James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> There is also more than just hunks. What about file renames? A file > rename commutes with a hunk that changes the file, and in darcs this > changes the hunk patch to refer to the renamed file. You need to change > the internal representation to refer to files using UUIDs to get around > that. And as soon as you do that you get the same problems with global > uniqueness invariants that you previously had for patches. There is a > reason why git cannot track file renames: they store just trees and > identify them by their content hash. This is secure and quite efficient, > but properly tracking file renames is not possible in such a model. > AFAIK Pijul suffers from a similar limitation and for the same reason > i.e. there is no primitive "rename" patch, only file-remove and file-add. I think Pijul does handle renames intelligently. (I just tested: merging a rename "f -> g" with an edit to f results in editing g.) A while ago I poked at Pijul's patch representation and inferred that it indeed gives each file a unique ID, and that ID is based on the ID of the patch that created it. I think it does something similar to assign identities to individual lines in files. I imagine it does the same thing for directories. Don't quote me on this, though. James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> This in turn led me to the more general question of how to detect > inconsistencies when exchanging patches between repos. The problem here > is that darcs currently relies on global uniqueness properties that are > quite easy to invalidate (e.g. by manually editing patches, and as > hinted above also when we independently convert branches of a repo). > Specifically, we rely on the following global property: if two patches > have the same name/identity, then (a) they can always be commuted to a > common context and (b) they are equal (content-wise) after commuting > them to any such common context. (The context of a patch is defined as > the set of patches preceding it.) Effectively this property means that > patches with the same name/identity are really just commuted/merged > versions of one and the same original patch. > > I have an (efficient) algorithm in mind that validates these assumptions > whenever we exchange patches between repos. Implementing this requires a > pretty deep refactor though. I was wondering if global uniqueness could be solved by borrowing from Pijul. If you include some metadata as part of the repository state (e.g. the identity of the hunk responsible for every line of every text file) then I think you could make it so that a primitive patch's representation doesn't change when it's commuted. I suspect pretty much any primitive patch theory could be adapted to work this way. (Note I'm not claiming this will make everything actually commute like in Pijul.) Besides giving unique names, another nice thing about this is that you shouldn't need to implement n^2 different patch commuting functions for n types of primitive patch. (I don't know if darcs actually needs to do this; I'm just assuming.) If you have access to the repo state, you can tell if two patches commute just by trying to apply them in the opposite order and seeing if they complain. In theory, you could even allow plugins that implement new patch types, with the basic principle that patches communicate with each other through modifications to the repo metadata. A slightly less radical version of this would be to keep the current primitive patch representation, but use this idea when generating the patch names. E.g. a hunk's name is a hash involving the identities of the hunks responsible for the lines it deletes. You'd still need to keep some metadata around to be able to do that, though. James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> Converting existing repos to darcs-3 is unfortunately one of the things > we havent't done yet. I have implemented a number of conversion schemes > but they all fail in some situations. There are two hard problems to > solve here: > > (1) What to do about so called "Duplicates" in the darcs-2 format. These > have no equivalent in the darcs-3 format (in darcs-3 duplicate prim > patches conflict). > > (2) How to ensure separately converted branches of a project remain > interoperable. The existing 'convert darcs-2' command gives up on this > and simply assigns new identities for all patches. This means you cän > convert at most one branch and have to throw away all others. (Or first > merge them all into a single repo, but that typically hits the dreaded > eponential behavior in the darcs-1 format, so in practice normally > doesn't work.) I always found this to be an extremely poor user > experience! It is one of the reasons many people never converted their > repos to the darcs-2 format. As an attempt to solve problem (2) ignoring problem (1), what would happen if you used the entire darcs-2 patch theory, including conflictors, as the primitive patch theory for darcs-3? The idea being that you avoid creating any new darcs-2 conflictors going forward, but if you do encounter them, they're just a legacy type of primitive patch. Or does the existence of darcs-2 style conflictors make the patch theory unsuitable? As an even more desparate attempt to solve (1), what if you said the primitive patch theory is a disjoint union of (a) "old-style" darcs-2 patches and (b) "new-style" darcs-3 primitive patches, and type (a) and (b) patches never commute? In practice you'd get awful conflicts if you tried to interleave darcs-2 and darcs-3 work, but in theory could that conversion be lossless? (Maybe old-style and new-style patches could sometimes commute. I'm trying to treat them as black boxes, making no assumptions.) James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> That said, you should be advised that both patch theory implementations
> ("formats") currently in use, namely darcs-1 and darcs-2, have bugs. In
> practice that means you may not be able to do such a separation for
> complicated conflict scenarios, though I think if it succeeds then the
> resulting repos should be equivalent. We have implemented a new one,
> darcs-3, which closely follows the camp paper and does not have any of
> these bugs. But that is not yet released. You can play with it using our
> development version at http://darcs.net/screened, but please don't use
> it for serious work, because the on-disk format may still change.
I'm glad to hear about darcs-3. I was worried work on implementing
Camp had stopped completely.
Is testing helpful at this point? I could try cloning and converting
my repos to darcs-3.
> I'd be interested to hear more about your patch theory.
Unsurprisingly, I'm learning about all sorts of interesting pitfalls
while trying to make it concrete.
I still might manage to make something worth sharing, though.
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
> > I've been reading about patch theory [0]. I *thought* what's supposed > > to happen is this: > > > > * The effect of B' is the same as the effect of A. (i.e. create the file) > > * The effect of A' is the same as the effect of B. (i.e. add "some text") > > * Therefore, B'A' does the same thing as AB. > > * B' and A' include some information about the conflict, in addition > > to their effects described above. (They are "conflictor" patches.) > > * If I commute B' and A' again, I get back AB, since <-> is a > > symmetric relation. > > I understand. However, there is no patch theory I am aware of that is > able to make this work, except those where *any* two patches commute, so > there are no dependencies and patches never conflict. Thank you. I've learned a lot from your reply. I have an idea for a patch theory that would satisfy these properties, and may have other advantages and might even be backward-compatible with darcs. I am not confident that it works, but I would love to have some feedback, if someone finds the time to read it. Is this list a good place to post something like that? > As I said in the beginning, there is no force-commute command in darcs > because that would be unsound. By definition, if B depends on A this > means A;B does /not/ commute. In the theory, one starts with primitive > patches for which there is no total merge operation, only a partial > clean-merge that may fail. If you have two independently recorded > patches A and B in the same context (we write this as A\/B), then > clean-merge succeeds iff A^;B commutes (where ^ means inversion). If > clean-merge(A\/B) does not succeed, then A\/B are said to be in conflict. Does darcs satisfy the property that if I merge two arbitrary repositories R and S to produce a new repository M, then separate out the patches again (i.e. pull just R's patches or just S's patches from M to a fresh repo) then I get back R and S? I hope the question makes sense. I can write a concrete sequence of commands if it doesn't. I had assumed this property was true because I thought force-commuting satisfied the magical properties in my previous email. I hope it is still true despite me being wrong about force-commuting. > When we add conflictors, we extend the set/type of primitive patches to > a larger set, such that now any two patches can be merged. However, we > must require that this extension preserves commutation behavior. In > particular, if A;B does not commute, then their embeddings in the larger > set of patches must commute neither. Ah, I had a different picture in mind. I thought that after adding in conflictors, then technically you end up with a universe of patches where everything commutes, but the patches end up looking ugly and unintuitive if you commute things that aren't "supposed" to. I thought a "force-commute" was simply a commute that wouldn't have been possible before adding conflictors to your universe of patches. This is what I hope my patch theory accomplishes. James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
Thanks, Ben! Responses inline. If you have the time, I'd be curious to hear about why my expectations didn't match what darcs actually did. > > What I'd like to do is create a repository R1 with patches A and B, > > and then look at the patches that result if A and B get > > force-commuted. > > > > E.g. if I could pull just patch B and not A to a new repository, I > > think that would do the trick, but of course darcs pull won't let me > > do that because B depends on A. > > The main question here is: What do you expect the result of such a > force-commute would be? > > Let us take a very simple example: > > A = addfile ./foo > B = hunk ./foo 1 [] ["some text"] > > where the hunk notation is simplified but hopefully understandable (the > hunk here removes no lines and adds the line "some text"). > > Suppose you had a 'darcs force-commute' command, and you force-commuted > A;B to B';A'. What would you expect the B' then A' to be? I've been reading about patch theory [0]. I *thought* what's supposed to happen is this: * The effect of B' is the same as the effect of A. (i.e. create the file) * The effect of A' is the same as the effect of B. (i.e. add "some text") * Therefore, B'A' does the same thing as AB. * B' and A' include some information about the conflict, in addition to their effects described above. (They are "conflictor" patches.) * If I commute B' and A' again, I get back AB, since <-> is a symmetric relation. However, that doesn't seem to be what happened (see below). Even if that were correct, it still doesn't leave me with a complete picture of what darcs actually does, so I wanted to experiment. > > Question 1: Is there a simple way to make darcs do this? > > Not exactly simple, but it is possible: > > darcs clone . ../saved > darcs rebase suspend # select B and A > darcs rebase obliterate # select A > darcs rebase unsuspend # select B > darcs pull ../saved # select A > > You should expect to get conflicts first when you unsuspend B (after > obliterating A) and then also when you re-pull A from the clone. You > will probably want to amend the conflict resolution into the conflicted > patch. Thanks, that seems to have worked. (I only got the first conflict, not the second.) But now I'm confused. Based on, for example, the "Forced commutation" section of https://en.wikibooks.org/wiki/Understanding_Darcs/Patch_theory_and_conflicts , I expected B' to add the file "foo", and A' to add "some text" (so, B' has the effect of A and A' has the effect of B). Instead of that, I get this: (a) If I follow your advice and amend the conflict resolution into B' before pulling, then (the amended) B' has the effect of AB, and A' has no effect. (b) If I run "darcs revert" instead of amending the conflict resolution into B', then B' has the effect of A and A' still has no effect. Confusingly, darcs offers to pull B from ../saved --- I thought darcs should consider it to already be present (as B'). I also noticed that if I run the swap a second time, I don't exactly get A and B back. (In the (a) case, I get patches with the same effects, but the new B starts with "duplicate"). I thought commutation was always supposed to be symmetric. Does that not apply when conflictors are involved? > Cheers > Ben Thanks, James [0] "Understanding darcs" on Wikibooks, "A formalization of Darcs patch theory using inverse semigroups", and some of Camp's "theory.pdf" ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] Make darcs force-commute patches from CLI, to learn about darcs?
(re-sending 3 days later; sorry if this arrives twice) Hi darcs-users, I'm trying to learn more about how darcs force commutes work. What I'd like to do is create a repository R1 with patches A and B, and then look at the patches that result if A and B get force-commuted. E.g. if I could pull just patch B and not A to a new repository, I think that would do the trick, but of course darcs pull won't let me do that because B depends on A. Question 1: Is there a simple way to make darcs do this? I can think of two complicated ways, which I might resort to: (a) Play with the darcs source code. (b) Set up contrived situations involving merges to force darcs to do the force-commutes I'm looking for. Question 2: Is there a way to make "darcs changes" show the patch contents? For now, I've been manually examining files in _darcs/patches. I vaguely remember there's an option to darcs changes or a related command to show the patch contents, but I can't seem to find it now. Thanks, James ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
