[darcs-devel] [issue2047] Falsifiable Darcs.Test.Patch.Properties.recommute

[Owen Stephens]

Owen Stephens <darcs at owenstephens.co.uk> added the comment:

Ok, so I've spent today finally figuring out this bug. Basically, it's
due to the interaction of Duplicates/Conflictors. In this particular
case, we commute a Conflictor past a Duplicate's context, but throw away
the resulting Conflictor, such that we can't do a reverse commute to
obtain the original patches.

Here's a dump of the whiteboard that Igloo and I twiddled with to
determine the problem:

We have an original context of "adddir ./dir1; addfile ./file1.txt"

Then we have two parallel branches, AB and CD:

A: rmdir ./dir1
B: conflictor [
   rmdir ./dir1
   ]
   |:
   move ./file1.txt ./dir1/file3.txt

C: rmdir ./dir1
D: move ./file1.txt ./file2.txt
  
We merge AB :\/: CD to obtain:
  
  A: rmdir ./dir1
  B: conflictor [
     rmdir ./dir1
     ]
     |:
     move ./file1.txt ./dir1/file3.txt
C'': duplicate
     |rotcilfnoc [
     |rmdir ./dir1
     |]
     ||:
     |move ./file1.txt ./dir1/file3.txt
     |adddir ./dir1
     |:
     rmdir ./dir1
D'': conflictor {{
     :
     move ./file1.txt ./dir1/file3.txt
     :
     rmdir ./dir1
     }} []
     :
     move ./file1.txt ./file2.txt

And now we try to commute (C'' :> D'') which results in:

D''':
conflictor {{
|:
move ./file1.txt ./dir1/file3.txt
|:
rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

C''':
duplicate
|rotcilfnoc [
|rmdir ./dir1
|move ./file1.txt ./file2.txt
|]
||:
|move ./file1.txt ./dir1/file3.txt
|adddir ./dir1
|:
rmdir ./dir1

By the definition of Commute (p :> Duplicate), we did a commute of (inv
p) and the "context" of the Duplicate's Non.

So, that is a commute of:

rotcilfnoc {{
|:
move ./file1.txt ./dir1/file3.txt
|:
rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

And:
rotcilfnoc {} [
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

We do this commute by first inverting, swithching order, then commuting,
then switching order, then inverting.
So, the commute we do is:

conflictor {} [
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

and

conflictor {{
    |:
    move ./file1.txt ./dir1/file3.txt
    |:
    rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

which (working out by hand) gives us:

move ./file1.txt ./file2.txt

and

conflictor {} [
    move ./file1.txt ./file2.txt
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

the second of which you can see in the resulting C'''.



However!! the only way of obtaining the original conflictor, is to
commute it back with 'move ./file1.txt ./file2.txt' - but we've thrown
that away, and can't get it back!

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/issue2047>
__________________________________