Re: How to extend a patch theory to fully commute

Am 03.07.20 um 23:44 schrieb Ben Franksen:
> Am 03.07.20 um 22:22 schrieb James Cook:
>> I think I've found a new problem with Proposition 5, though.
>>
>> Suppose A, B and C are three mutually conflicting patches with
>> starting context s.
>>
>> Suppose I merge A and B, then I use Proposition 5 to navigate back to
>> the starting context s so that I can continue recording new patches.
>>
>> The problem: now if I pull in C, it looks just like any other new
>> patch to be recorded starting at context s. So, by marking the A\/B
>> conflict as resolved, I've made my repository unaware that C should be
>> considered to be a conflict.
> 
> I'd say this is a feature, not a bug. If you mark the conflict between A
> and B as resolved, *without* recording a new patch, then this means you
> are satisfied with the resolution that reverts both changes. There is no
> reason why pulling C should conflict now. If, on the other hand, you are
> not satisfied with this resolution, you may want record a "proper"
> resolution, usually a mixture of A and B. This will then typically
> conflict with C.
> 
> That said, there is a problem here. To arrive at the default resolution
> (revert the conflicting prim patches) you add inverse patches to the
> repo. But what does "adding a patch to a repo" mean, precisely, if
> inverses are involved? Is a repo still a sequence of patches? Is A;A^;A
> the same as A? That would be bad because resolving a conflict would then
> be the same as obliterating the conflicting patches. So inverse pairs
> cannot simply be cancelled.

An afterthought: what if you do not simply add the inverse for the
resolution, but instead record a new patch with the same effect as the
inverse? In other words, you add the inverse, but give it a new
(positive) name, so that it cannot cancel. Just an idea.

Cheers
Ben