Re: 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