Understanding Darcs/Patch theory
Math and computer science nerds only
[edit | edit source](The occasional physicist will be tolerated)
Casual users be warned, the stuff you're about to read is not for the faint of heart! If you're a day-to-day darcs user, you probably do not need to read anything from this page on. However, if you are interested in learning how darcs really works, we invite you to roll up your sleeves, and follow us in this guided tour of the growing Theory of Patches.
What is the theory of patches?
[edit | edit source]The darcs patch formalism is the underlying "math" which helps us understand how darcs should behave when exchanging patches between repositories. It is implemented in the darcs engine as data structures for representing sequences of patches and Haskell functions equivalent to the operations in the formalism. This section is addressed at two audiences: curious onlookers and people wanting to participate in the development of the darcs core. My aim is to help you understand the intuitions behind all this math, so that you can get up to speed with current conflictors research as fast as possible and start making contributions. You should note that I myself am only starting to learn about patch theory and conflictors, so there may be mistakes ahead.
Why all this math?
[edit | edit source]One difference between centralized and distributed version control systems is that "merging" is something that we do practically all the time, so it is doubly important that we get merging right. Turning the problem of version control into a math problem has two effects: it lets us abstract all of the irrelevant implementation details away, and it forces us to make sure that whatever techniques we come up with are fundamentally sound, that they do not fall apart when things get increasingly complicated. Unfortunately, math can be difficult for people who do not make use of it on a regular basis, so what we attempt to do in this manual is to ease you into the math through the use of concrete, illustrated examples.
A word of caution though, "getting merging right" does not necessarily consist of having clever behaviour with respect to conflicts. We will begin by focusing on successful, non-conflicting merges and move on to the darcs approach to handling conflicts.
Note that the notation we use follows that from FOSDEM 2006, and not the darcs patch theory appendix. Namely, patch composition is written left to right. means that B is applied after A |
Context, patches and changes
[edit | edit source]Let us begin with a little shopping. Arjan is working to build a shopping list for the upcoming darcs hackathon. As we speak, his repository contains a single file s_list with the contents
1 apples 2 bananas 3 cookies 4 rice
Note:the numbers you see are just line numbers; they are not part of the file contents
As we will see in this and other examples in this book, we will often need to assign a name to the state of the repository. We call this name a context. For example, we can say that Arjan's repository is a context , defined by there being a file s_list with the contents mentioned above.
Arjan makes a modification which consists of adding a line in s_list. His new file looks like this:
1 apples 2 bananas 3 beer 4 cookies 5 rice
When Arjan records this change (adding beer), we produce a patch which tells us not only what contents Arjan added ("beer") but where he added them, namely to line 3 of s_list. We can say that in his repository, we have moved from context to context via a patch A. We can write this using a compact notation like or using the graphical representation below:
Sequential patches
[edit | edit source]Starting from this context, Arjan might decide to make further changes. His new changes would be patches that apply to the context of the previous patches. So if Arjan makes a new patch on top of this, it would take us from context to some new context . The next patch would take us from this context to yet another new context , and so on and so forth. Patches which apply on top of each other like this are called sequential patches. We write them in left to right order as in the table below, either representing the contexts explicitly or leaving them out for brevity:
with context | sans context (shorthand) |
---|---|
All darcs repositories are simply sequences of patches as above; however, when performing a complex operation such as an undo or exchanging patches with another user, it becomes absolutely essential that we have some mechanism for rearranging patches and putting them in different orders. Darcs patch theory is essentially about giving a precise definition to the ways in which patches and patch-trees can be manipulated and transformed while maintaining the coherence of the repository.
Inverses
[edit | edit source]Let's return to the example from the beginning of this module. Arjan has just added beer to our hackathon shopping list, but in a sudden fit of indecisiveness, he reconsiders that thought and wants to undo his change. In our example, this might consist of firing up his text editor and remove the offending line from the shopping list. But what if his changes were complex and hard to keep track of? The better thing to do would be to let darcs figure it out by itself. Darcs does this by computing an inverse patch, that is, a patch which makes the exact opposite change of some other patch:
Definition (Inverse of a patch):
The Inverse of patch is , which is the patch for which the composition makes no changes to the context and for which the inverse of the inverse is the original patch.
So above, we said that Arjan has created a patch which adds beer to the shopping list, passing from context to , or more compactly, . Now we are going to create the inverse patch , which removes beer from the shopping list and brings us back to context . In the compact context-patch notation, we would write this as . Graphically, we would represent the situation like this:
Patch inverses may seem trivial, but as we will see later on in this module, they are a fundamental operation and absolutely crucial to make some of the fancier stuff -- like merging -- work correctly. One of the rules we impose in darcs is that every patch must have an inverse. These rules are what we call patch properties. A patch property tells us things which must be true about a patch in order for darcs to work. People often like to dream up new kinds of patches to extend darcs's functionality, and defining these patch properties is how we know that their new patch types will behave properly under darcs. The first of these properties is dead simple:
Patch property: Every patch must have an inverse |
Commutation
[edit | edit source]Arjan was lucky to realise that he wanted to undo his change as quickly as he did. But what happens if he was a little slower to realise his mistake? What if he makes some other changes before realising that he wants to undo the first change? Is it possible to undo his first change without undoing all the subsequent changes? It sometimes is, but to do so, we need to define an operation called commutation.
Consider a variant of the example above. As usual, Arjan adds beer to the shopping list. Next, he decides to add some pasta on line 5 of the file:
The question is how darcs should behave if Arjan now decides that he does not want beer on the shopping list after all. Arjan simply wants to remove the patch that adds the beer, without touching the one which adds pasta. The problem is that darcs repositories are simple, stupid sequences of patches. We can't just remove the beer patch, because then there would no longer be a context for the pasta patch! Arjan's first patch takes us to context like so: , and his second patch takes us to context , notably starting from the initial context : . Removing patch would be pulling the rug out from under patch . The trick behind this is to somehow change the order of patches and . This is precisely what commutation is for:
The commutation of patches and is represented by , where and are intended to perform the same change as and |
Why not keep our old patches?
[edit | edit source]To understand commutation, you should understand why we cannot keep our original patches, but are forced to rely on evil step sisters instead. It helps to work with a concrete example such as the beer and pasta one above. While we could write the sequence to represent adding beer and then pasta, simply writing for pasta and then beer would be a very foolish thing to do.
Put it this way: what would happen if we applied before ? We add pasta to line 5 of the file:
1 apples 2 bananas 3 cookies 4 rice 5 pasta
Does something seem amiss to you? We continue by adding beer to line 3. If you pay attention to the contents of the end result, you might notice that the order of our list is subtly wrong. Compare the two lists to see why:
(wrong!) | (right) |
---|---|
1 apples 2 bananas 3 beer 4 cookies 5 rice 6 pasta |
1 apples 2 bananas 3 beer 4 cookies 5 pasta 6 rice |
It might not matter here because it is only a shopping list, but imagine that it was your PhD thesis, or your computer program to end world hunger. The error is all the more alarming because it is subtle and hard to pick out with the human eye.
The problem is one of context, specifically speaking, the context between and . In order for instructions like "add pasta to line 5 of s_list" to make any sense, they have to be in the correct context. Fortunately, commutation is easy to do, it produces two new patches and which perform the same change as and but with a different context in between.
Exercises |
---|
Patch is identical to . It adds "beer" to line 3 of the shopping list. But what should patch do? |
One more important detail to note though! We said earlier that getting the context right is the motivation behind commutation -- we can't simply apply patches in a different order, because that would get the context all wrong. But context does not have any effect on whether A and B can commute (or how they should commute). This is strictly a local affair. Conversely, the commutation of A and B does not have any effect either on the global context: the sequences and (where the latter is the commutation of the former) start from the same context and end in the same context.
The complex undo revisited
[edit | edit source]Now that we know what the commutation operation does, let's see how we can use it to undo a patch that is buried under some other patch. The first thing we do is commute Arjan's beer and pasta patches. This gives us an alternate route to the same context. But notice the small difference between and !
The purpose of commuting the patches is essentially to push patch on to end of the list, so that we could simply apply its inverse. Only here, it is not the inverse of that we want, but the inverse of its evil step sister . This is what applying that inverse does: it walks us back to the context , as if we had only applied the pasta patch, but not the beer one.
And now the undo is complete. To sum up, when the patch we want to undo is buried under some other patch, we use commutation to squeeze it to the end of the patch sequence, and then compute the inverse of the commuted patch. For the more sequentially minded, this is what the general scheme looks like:
Exercises |
---|
Imagine the opposite scenario: Arjan had started by adding pasta to the list, and then followed up with the beer.
|
Commutation and patches
[edit | edit source]Every time we define a type of patch, we have to define how it commutes with other patches. Most of time, it is very straightforward. When commuting two hunk patches, for instance, we simply adjust their line offset. For instance, we want to put something on line 3 of the file, but if we use patch to insert a single line before that, what used to be line 3 now becomes line 4! So patch inserts the line "x" into line 4, much like inserts it into line 3.
Some patches cannot be commuted. For example, you can't commute the addition of a file with adding contents to it. But for now, we focus on patches which can commute.
Merging
[edit | edit source]- Note: this might be a good place to take a break. We are moving on to a new topic and new (but similar) examples
We have presented two fundamental darcs operations: patch inverse and patch commutation. It turns out these two operations are almost all that we need to perform a darcs merge.
Arjan and Ganesh are working together to build a shopping list for the upcoming darcs hackathon. Arjan initialises the repository and adds a file s_list with the contents
1 apples 2 bananas 3 cookies 4 rice
He then records his changes, and Ganesh performs a darcs get
to obtain an identical copy of his repository. Notice that Arjan and Ganesh are starting from the same context
Arjan makes a modification which consists of adding a line in s_list. His new file looks like this:
1 apples 2 bananas 3 beer 4 cookies 5 rice
Arjan's patch brings him to a new context :
Now, in his repository, Ganesh also makes a modification; he decides that s_list is a little hard to decipher and renames the file to shopping. Remember, at this point, Ganesh has not seen Arjan's modifications. He's still starting from the original context , and has moved a new context , via his patch :
Parallel patches
[edit | edit source]At this point in time, Ganesh decides that it would be useful if he got a copy of Arjan's changes. Roughly speaking we would like to pull Arjan's patch A into Ganesh's repository B. But, there is a major problem! Namely, Arjan's patch takes us from context to context . Pulling it into Ganesh's repository would involve trying to apply it to context , which we simply do not know how to do. Put another way: Arjan's patch tells us to add a line to file s_list; however, in Ganesh's repository, s_list no longer exists, as it has been moved to shopping. How are we supposed to know that Arjan's change (adding the line "beer") is supposed to apply to the new file shopping instead?
Arjan and Ganesh's patches start from the same context o and diverge to different contexts a and b. We say that their patches are parallel to each other, and write it as . In trying to pull patches from Arjan's repository, we are trying to merge these two patches. The basic approach is to convert the parallel patches into the sequential patches , such that does essentially the same change as does, but within the context of b. We want to produce the situation
Performing the merge
[edit | edit source]Converting Arjan and Ganesh's parallel patches into sequential ones requires little more than the inverse and commutation operations that we described earlier in this module:
- So we're starting out with just Ganesh's patch. In context notation, we are at
- We calculate the inverse patch . The sequence consists of moving s_list to shopping and then back again. We've walked our way back to the original context:
- Now we can apply Arjan's patch without worries: , but the result does not look very interesting, because we've basically got the same thing Arjan has now, not a merge.
- All we need to do is commute the last two patches, , to get a new pair of patches . Still, the end result doesn't seem to look very interesting since it results in exactly the same state as the last step:
- However, one crucial difference is that the second to last patch produces just the state we're looking for! All we now have to do to get at it is to ditch the patch, which is only serving to undo Ganesh's precious work anyway. That is to say, by simply determining how to produce an which will commute with , we have determined the version of which will update Ganesh's repository.
The end result of all this is that we have the patch we're looking for, and a successful merge.
Merging is symmetric
[edit | edit source]Concretely, we've talked about Ganesh pulling Arjan's patch into his repository, so what about the other way around? Arjan pulling Ganesh's patch into his repository would work the same exact way, only that he is looking for a commuted version of Ganesh's patch that would apply to his repository. If Ganesh can pull Arjan's patch in, then Arjan can pull Ganesh's one too, and the result would be exactly the same:
Definition (Merge of two patches):
The result of a merge of two patches and is one of two patches and , which satisfy the relationship
The merge definition describes what should happen when you combine two parallel patches into a patch sequence. The built-in symmetry is essential for darcs because a darcs repository is defined entirely by its patches. Put another way,
- To be written
The commutation with inverse property
[edit | edit source]The definition of a merge tells us what we want merging to look like. How did we know how to actually perform that merge? The answer comes out of the following property of commutation and inverse: if you can commute the inverse of a patch with some other patch , then you can also commute the patch itself against .
if and only if , provided both commutations succeed. |
Note how the left hand side of this property exactly matches the relationship demanded by the definition of a merge. To see why this all works,
- To be written
Definitions and properties
[edit | edit source]definition of inverse | has no effect |
inverse of an inverse | |
inverse composition property | |
definition of commutation | |
definition of a merge | |
commutation with inverse property | if and only if |