Re: How to extend a patch theory to fully commute
Ben Franksen <[email protected]> Thu, 2 Jul 2020 20:41:02 +0200
| Newsgroups | gmane.comp.version-control.darcs.user |
|---|---|
| Message-ID | <[email protected]> |
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