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

[Ben Franksen]

Am 01.07.20 um 18:39 schrieb James Cook:
>> A well-known and quite natural way to identify the equivalence class of
>> all patches that a given patch P can be commuted to, is to use the so
>> called "minimal context". A minimal context C(P) for some patch P is a
>> sequence of patches starting at the empty state and preceding P, and
>> that is minimal in the sense that no subset of it is a valid context. In
>> other words, no patch in C(P) can be commuted past P. Another way to
>> look at it is to start with a patch P in /any/ context and then commute
>> everything you can past P. It is easy to show that this can always be
>> done and that the result is unique i.e. you always get the same /set/ of
>> patches for the minimal context.
> 
> I think I've found a case where darcs 2 violates that uniqueness
> property.

Yes, because this uniqueness is a consequence of permutivity.

> In fact, I got darcs to crash after that, so I  filed
> http://bugs.darcs.net/issue2647

This is a well known bug in both darcs-1 and darcs-2 format. It is the
infamous "duplicate prim patch" problem. If you don't track the identity
of prim patches (such as is done in darcs-3, but not in darcs-1 and
darcs-2), then commutation /cannot/ distinguish between equal prim
patches. The camp paper explains that in Appendix B.

> I added comments interspersed with the shell commands in that bug
> explaining where I managed to change the minimal context of a patch.
> Is that in itself a bug?

Yes. This clearly violates permutivity. Whether patches commute must be
independent of reordering.

> This behaviour is behind the note I added to Assumption 2 about it
> possibly being false for Darcs 2. When I originally discovered it, I
> thought I just had to live with that, but based on your email, and the
> fact that I've now actually crashed Darcs, I guess maybe the behaviour
> is unintended.

The behavior is definitely not intended. The fact that darcs crashes
here shows that it internally expects permutivity to hold.

BTW, you don't say it explicitly, but since in several places you refer
to names, I was assuming that in your theory prim patches are always named.

Cheers
Ben