[darcs-users] Conflict marking

[David Roundy]

On Wed, Nov 05, 2008 at 03:06:11AM +0000, Ian Lynagh wrote:
> 
> Hi all,
> 
> I'm trying to write down exactly how conflict marking works.
> I'd appreciate it if you'd let me know if you see any errors in the
> following.

Looks about right to me.

David

> If we have a repository
>     As
> then we can commute this to
>     Bs Cs
> where:
> * everything in Cs is a conflictor, and
> * Bs cannot be commuted to
>       Ds E
>   where E is a conflictor.
> 
> Let Fs^ be the effect of Cs. Then Bs can be commuted to
>     Gs Fs
> (proof by contradiction: If a patch in Gs depended on something in Fs,
> then whatever conflicted with that F would have also conflicted with
> that G).
> 
> Gs is the pristine state.
> 
> Now, we can imagine this repo as starting with the sequence Gs, and then
> having multiple forks:
> 
> One fork is
>     Fs
> 
> Forall patches in Cs, if Cs = Xs [effect, context:Y] Zs
> then
>     Fs effect(Xs) effect context Y
> is a fork (but commute anything you can past Y to make the conflict look
> as simple as possible).
> 
> Similarly, if one fork is subsumed by another then remove it.
> For example, in the merge
>     A + (B C)
> where A conflicts with B and C depends on B, we only need the forks
>     A and BC
> we don't need all of
>     A, B and BC
> 
> Note that in order to find the Fs fork we don't need to split Cs into
> Gs Fs, we can just get Fs from the effect of the conflictors.
> 
> Note also that we don't need to worry about what the conflictors
> conflict with, only what they are /first/ to conflict with (i.e. what is
> in their effect).
> 
> 
> The other half of the puzzle is how to show 2 or more forks to the user,
> but I haven't got that far yet. That's obviously dependent on exactly
> what types of primitive patches you have.
> 
> 
> Thanks
> Ian
> 

-- 
David Roundy
http://www.darcs.net