Theory

Motivation and examples

Patch theory in the past/present/future

Past: Darcs 1 - Mergers

  • An explanation of mergers (and what conflictors were meant to be)
  • Merges Documentation An old theory document that was included in the darcs source, from around when mergers were in use. Explains unwinding and mergers to some extent. Written by David Roundy.

Present: Darcs 2 - Conflictors

Future? Darcs 3 - ?

Ian and Ganesh want a minimal ‘toy’ implementation of the core patch theory stuff (which could eventually be plugged into darcs 3). The point is to prove things about patch theory. One it would make everybody feel a lot better, two we could then do things like simplify it whilst proving that things still work. With that in mind:

  • Camp is a project to develop and prove correct a darcs-like patch theory, which will hopefully form the basis for darcs 3. The theory is similar to that of darcs 2, so reading the paper on the camp site will also give an insight into how the current darcs patch theory works.
  • Judah Jacobson wrote up his work on formalizing darcs 2-and-beyond patch theory on ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf
  • Homotopical Patch Theory, Carlo Angiuli, Ed Morehouse, Daniel R. Licata, Robert Harper, ICFP 2014
  • A Categorical Theory of Patches, Samuel Mimram and Cinzia Di Giusto, 2013
  • Graphictors are an evolution of Conflictors.
  • also check out Pijul

See also