darcs

Issue 2047 Falsifiable Darcs.Test.Patch.Properties.recommute

Title Falsifiable Darcs.Test.Patch.Properties.recommute
Priority bug Status needs-reproduction
Milestone Resolved in
Superseder Nosy List Serware, ganesh, iago
Assigned To
Topics Conflicts, Darcs2

Created on 2011-02-22.13:11:57 by iago, last changed 2012-03-30.18:26:10 by owst.

Files
File name Uploaded Type Edit Remove
falsifiable_recommute iago, 2011-02-22.13:11:56 application/octet-stream
falsifiable_recommute2 iago, 2011-02-24.17:58:14 application/octet-stream
unnamed iago, 2011-02-24.17:58:14 text/html
Messages
msg13725 (view) Author: iago Date: 2011-02-22.13:11:56
Running QuickCheck tests I have found a possible bug (I guess in 
commutation/merging of V2 patches) which breaks recommute property.
I have found the same bug twice, in both cases the problem looks related 
with a conflictor between "move a file into a directory" and "remove that 
directory".
Attachments
msg13755 (view) Author: kowey Date: 2011-02-24.13:46:35
I think we need somebody to study this log and figure out if it's an 
actual bug, turn it into English, and can it.
msg13756 (view) Author: iago Date: 2011-02-24.17:58:14
Another counter-example, may help. In this case the problem appears due to a
conflictor between "edit/remove a file inside a directory" and "remove that
directory".

On Thu, Feb 24, 2011 at 1:46 PM, Eric Kow <bugs@darcs.net> wrote:

>
> Eric Kow <kowey@darcs.net> added the comment:
>
> I think we need somebody to study this log and figure out if it's an
> actual bug, turn it into English, and can it.
>
> ----------
> nosy: +Serware
> priority:  -> bug
> status: unknown -> need-action
> topic: +Conflicts, Darcs2
>
> __________________________________
> Darcs bug tracker <bugs@darcs.net>
> <http://bugs.darcs.net/issue2047>
> __________________________________
>



-- 
Iago Abal Rivas
Attachments
msg15432 (view) Author: owst Date: 2012-03-30.18:26:09
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!
History
Date User Action Args
2011-02-22 13:11:57iagocreate
2011-02-24 13:46:37koweysetpriority: bug
status: unknown -> needs-reproduction
topic: + Conflicts, Darcs2
messages: + msg13755
nosy: + Serware
2011-02-24 17:58:14iagosetfiles: + unnamed, falsifiable_recommute2
messages: + msg13756
2012-03-30 18:26:10owstsetmessages: + msg15432