[darcs-users] Formal documentation

[Sittampalam, Ganesh]

Gabriel Kerneis wrote:
>>> 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. 
> 
> But it is very unlikely you can prove that:
> http://tahoe-lafs.org/~zooko/badmerge/simple.html

That just means that the specification you would be able to prove
against is relatively weak. For example, you could probably still prove
that any textual lines in the source are kept in the result and that
some kind of loose ordering is preserved.

With darcs hunk patches you might be able to do a little better because
they are very concrete about where the change is located. There's a
classic problem with adding a new C function where the diff includes the
closing brace of the previous function rather than the closing brace of
the new function, leading to merges sometimes inserting things in the
wrong place if content was added to the old function in a parallel
change. With darcs hunk patches you know up front whether this has
happened or not.

Ganesh

Ganesh

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