[darcs-devel] V3.commuteNoConflicts side conditions

Ben Franksen ben.franksen at online.de
Wed Aug 14 11:17:42 UTC 2019


Hi Ganesh

> I'm looking at the side-conditions on commuteNoConflicts in V3. As
> Ben suggested a little while ago, I'm paying special attention to
> whether they should cause commute failure or errors.

Thanks for doing that.

> One simple example is the Prim :> Conflictor case:
> 
> commuteNoConflicts (Prim p :> Conflictor s y q) | Just (s' :> p') <-
> commuteFL (p :> s) , Just q' <- commutePast p' q , Just y' <-
> S.fromList <$> mapM (commutePast p') (S.toList y) = Just (Conflictor
> s' y' q' :> Prim p')
> 
> I guess that the normal laws about commuting should apply to 
> commuteNoConflicts, in particular that two patches should
> consistently commute or not, no matter what context they are in?

Yes, definitely.

> If so, it suggests to me that once we have established that p and q 
> commute - i.e. that commutePast has succeded - any other commute 
> failures should be errors rather than just causing commuteNoConflicts
> to return Nothing.

Hmm. Indeed, the patches referenced by the set of conflicts y must live
somewhere in the past of p, so for p to become adjacent to the
conflictor, p must have already been commuted past them. I think Ian
made this argument somewhere in the paper where he discusses the commute
rules in detail. You could look that up and compare.

> Alternatively, maybe we should be using something like ctxAdd on the 
> last line (which will always succeed) instead of commutePast (which 
> might fail).

Correct.

> If any of the earlier commutes fail, it implies p and q can never
> live next to each other so it's correct for the commute to fail.

Yes, exactly. (This would be the contra-positive of my argument above. I
personally prefer direct proofs...)

> But we would need to make sure that in each case we are doing the
> minimum work necessary to get p next to q.

I don't understand this remark. Can you clarify?

Anyway, I would just make this change (and related ones; I agree that
replacing commutePast with ctxAdd here is the right thing to do) and run
the unit tests with -j4 -t RepoPatchV3 -q=10000. For me this usually
catches any inconsistencies in the implementation. If you are paranoid
(and perhaps need to brew coffee anyway) you can take -q=50000 ;-)

Cheers
Ben



More information about the darcs-devel mailing list