
\section{\label{sec:overview}Overview}

Camp is a version control system, similar in philosophy to darcs.
In this document we present a description of camp's patch theory.

This document is very much a work in progress. Some sections are more
readable than others. Some coq proofs are starting to appear, and where
they haven't there may be a (somewhat handwavey) hand proof.

In \refSection{notation} we quickly introduce some general
notation that we will be using.

In \refSection{unnamed_patches} we say define a set of unnamed
patches, and explain what behaviour we require that they satisfy. We
also introduce a concept of commutation for unnamed patches.

In \refSection{unnamed_patch_sequences} we define sequences of
unnamed, and some properties that they must satisfy.

In \refSection{sensible_unnamed_patch_sequences} we define a subset
of all the possible unnamed patch sequences, which we call sensible.

In \refSection{names} we introduce names.

Everything up to this point is an input to the paper. In other words, we
require that we are provided with unnamed patches, unnamed patch commute
and the notion of sensible unnamed patch sequences, which satisfy the
properties that we specify. Likewise, we require that we are given a
suitable set of names.

While it is possible to start from a lower level, and prove the
correctness of the operations on unnamed patches, that is not the goal
of this document.

In \refSection{named_patches} we build named patches out of names
and unnamed patches.

In \refSection{patch_sequences} we build sequences from these named
patches.

In \refSection{patch_merge} we take a break from the formal
definition, and give a description of how merges (of non-conflicting
changes) work.

In \refSection{patch_universes} we introduce the concept of
\emph{patch universes}. This is an algebraic structure that many kinds
of patches are examples of.

This actually give you all that you need in order to make a version
control system, provided that you never make conflicting changes that
you later want to merge.

In \refSection{contexted_patches} we introduce a ``contexted
patch'' datastructure.

In \refSection{catches} we define catches and repos, and make
conjectures that they satisfy properties that we want them to satisfy.

In \refSection{catch_patch_universe} we prove that catches form a
patch universe.

The result is a version control system in which it is always possible to
merge repos --- which is vital for a distributed version control system.

