[darcs-users] Formal documentation

Gabriel Kerneis kerneis at pps.jussieu.fr
Fri Feb 4 08:17:29 UTC 2011


> > 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

-- 
Gabriel


More information about the darcs-users mailing list