[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