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
