[darcs-users] Formal documentation

[Sittampalam, Ganesh]

Michael Olney wrote:
>> The key property is that any given set of patches, you get the same
>> repository state no matter what order those patches are currently
>> stored in. That underpins the "first-class cherry-picking" and "no
>> fresh commit 
>> for merges" that darcs has and other VCS systems don't.
> 
> I guess I'm not clear as to who these proofs are supposed to
> convince, and of what.

Concretely, if you unpull and pull patches in an arbitary order in a
repository (from any remote source), getting to some given set of
patches X, the result will be the same no matter what order you do those
unpulls and pulls.

> Without a more specific interpretation of the
> theory or more properties it doesn't seem possible to prove, for
> example, that I'm not going to lose any important information during
> the merging process.

The unique result of the merging/commuting process might indeed be
nonsense. A separate aspect of formalising a VCS might be to provide
some formal definition of what it means to keep "important information",
but I think that's mostly orthogonal to the issue of commuting and
merging, and not so specific to darcs. For example I think if you could
prove that diff3 based merging doesn't lose information in some sense,
that result could be adapted to darcs hunk patches.

Ganesh


=============================================================================== 
Please access the attached hyperlink for an important electronic communications disclaimer: 
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html 
===============================================================================