[darcs-devel] camp conflictors aka RepoPatchV3

[Ben Franksen]

Am 08.09.2018 um 19:34 schrieb Ben Franksen:
> Am 07.09.2018 um 19:31 schrieb Benjamin Franksen:
>> I am happy to announce that I finally managed to iron out the last bugs
>> from my implementation of camp conflictors in Darcs. All unit and
>> quickcheck tests pass with -q10000, for both V1 and FileUUID prims.
> 
> My enthusiasm was premature. I thought I had enabled all property tests
> but in fact a few were not checked, namely the permutivity tests, which
> indeed fail as I found out. Fixing permutivity is going to be hard but
> perhaps not impossible.

tl;dr: I managed to fix it by adding inverse conflictors and this time
made sure all property tests are enabled.

Long story: I had previously tried to invert conflictors by inverting
their internals in order to reduce the number of cases to consider for
merge and commute. The problem here is how to invert a contexted patch.
Contexted patches are defined as

data Contexted wX where
  Contexted :: FL p wX wY -> p wY wZ -> Contexted p wX

This is similar to a V2.Non but contains prim patches only (which is the
main difference between V2 and V3 and ensures there is no exponential
blow-up i.e. no nesting of conflictors within conflictors). These things
cannot be inverted in a straight-forward way. Ian's implementation in
camp (that I copied) uses a somewhat dubious trick: he flattens it to an
FL and then adds the result as context for p^. This works wrt type
witnesses but is semantically wrong, since it means that when we invert
a conflictor we add artificial dependencies for the conflictor's
identity and the set of patches it conflicts with... which causes
permutivity to break down.

I had earlier played with the idea of making Contexted patches
invertible in a first-class way by adding a "mirror-image" constructor

  ContextedR :: p wZ wY -> RL p wY wX -> Contexted p wX

However, this turned out to be too flexible: it is now possible for
normal contexted patches and inverted contexted patches to be mixed in
the same conflictor which causes the number of cases we need to consider
to explode beyond reason (instead of reducing it).

So I went back to the same trick that David used for V2: add a
constructor for inverse conflictors in such a way that 'invert' doesn't
touch the internals at all, then bite the bullet and add the missing
cases. Or rather, those that we expect to encounter in real
repositories: as for V2, I did not implement merge or the conflicted
commute involving inverse conflictors. ("Conflicted commute" means those
cases of commute that ensure that both branches of a conflicted merge
commute to each other i.e. those not handled by commuteNoConflicts.)

The implementation of the cases for inverse conflictors is a bit too
repetitive for my taste. I will try to find out if it can be refactored
to avoid that.

Cheers
Ben