[darcs-users] Formal documentation

Ganesh Sittampalam ganesh at earth.li
Thu Feb 3 23:59:12 UTC 2011


Hi,

On Fri, 4 Feb 2011, Michael Olney wrote:

> <iago.abal at gmail.com> wrote:
>> Finally, AFAIK only 2-3 people fully understand Darcs patch theory
>> implementation(1), and the only available "documentation" about some Darcs
>> advanced topics are some discussions in some old Darcs mailing list.
>
> There seems to be a general impression put forth by some that there
> are people who understand various aspects of patch theory to various
> extents. It seems impossible to validate that claim unless someone
> writes down those aspects in a precise form. I think some people have
> the impression that someone just needs to "get around" to writing them
> down.

The basic intuition behind patch theory is quite straightforward: define a 
primitive commute operation which satisfies some relatively obvious laws, 
derive a merge operation from it, now you've got a system you can use for 
putting a bunch of patches in any valid order and getting the same end 
result no matter what order you pick. That's the fundamental basis of 
darcs and the implementation basically follows that kind of strategy.

However, writing it down formally and pinning down the various pieces with 
precise definitions - e.g how patch identity is defined and what it means 
to be an inverse - is annoyingly fiddly, and so it's not just a matter of 
writing it down.

I think the important pieces are an appropriate set of definitions, a set 
of properties that all patch system should obey, a proof that the existing 
implementation of "primitive" patches in darcs obeys those properties, and 
a proof that anything that obeys those properties does indeed behave 
consistently when you commute and merge patches in it.

The wiki page about theory has a bunch of links to mostly half-finished 
attempts: http://wiki.darcs.net/Theory. Ian Lynagh's camp project 
(currently offline due to a compromised server, but should be back soon) 
and Judah Jacobson's papers probably deserve the most attention.

The other stumbling block is a good representation of conflicts, without 
which it's hard to make a usable VCS. Both of the implementations 
currently in darcs have some problems though they just about work out ok 
in practice, so essentially it's an unsolved problem in a theoretical 
sense. (I happen to be working on a solution off and on at the moment, but 
there've been many false dawns in this area...)

Cheers,

Ganesh


More information about the darcs-users mailing list