[darcs-devel] [patch1946] WIP: introduce concept of unwinding a conflict

[Benjamin Franksen]

Hi Ganesh

sorry for dropping out of darcs development for quite a while, in
particular for not responding to this message earlier.

Am 05.12.19 um 08:16 schrieb Ganesh Sittampalam:
> I made a generator for Named based on the latest on that generates
> conflict resolutions (arbitrarySequence). [...]
> 
> The upshot is that I have an implementation of fullUnwind that works for
> V2 and V3 patches but fails for some V1 patches.

Hey, that sounds pretty good.

Which features are used to achieve this? To elaborate, suppose, for the
sake of discussion, we disregard V1 and V2, could the squashing /
reordering be done with /named/ prim patches a la V3 alone? If not,
which methods from the raw prim patch interfaces are you using?

> For the V1 failures, I have a test case with 5 patches where the effect
> of the two routes through a merge square is different, even after
> collapsing inverses and commuting. I think this is a clear bug in V1;

IIUC, you claim there are situations where we have patch sequences p and
q, such that

  merge (p:\/:q) = q':/\:p'  &&  effect (p:>q') /= effect (q:>p')

This is definitely a bug.

> From this test case, adding a 6th patch leaves us with a conflict that
> unwinds incorrectly and then can't be squashed with the previous one.
> However, darcs would not necessarily crash in normal operation with
> these patches.
> 
> Once I exclude test cases that break the "merge square effect" property,
> fullUnwind works consistently on V1 patches too.

Good!

> I've verified all of this with 100K test cases for each patch type:
> while quantity does not prove quality, QuickCheck was pretty effective
> at finding problems in my fullUnwind implementation and the cases where
> V1 doesn't work.

I have been relying on QC tests with a large number of tests, too. This
was extremely useful to uncover bugs, not only in the implementation of
V3 (and of course V1 and V2, too) but also in the spec i.e. invariants I
assumed but that that are in fact not valid.

> I think it's plausible that a user could actually hit the V1 case in
> practice, so just making it impossible for them to suspend the patch
> seems a bit unfriendly. But equally it's a legacy edge case so I don't
> think it should unnecessarily constrain our design choices.

Right. We can, perhaps, add work-arounds for V1, but I agree that this
should not influence the design.

> So what I propose is making fullUnwind able to report a failure, and
> then have darcs fall back to something else in that case. An easy option
> would be to just take any fixups that don't commute and put them in the
> main "to edit" patch. Or it could make multiple "to edit" patches like
> one of my prototypes did.

Both seem like acceptable solutions to me.

> I think to keep things reasonably simple I would just have darcs do that
> automatically but print out a message. An alternative would be for it to
> have a special flag to get that behaviour and to mention the existence
> of the flag when the normal behaviour fails. That seems like overkill to
> me though.

Agreed, just printing the warning should be enough.

Cheers
Ben