Re: How to extend a patch theory to fully commute

On Sat, 4 Jul 2020 at 16:05, Ben Franksen <[email protected]> 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