[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