chiark / gitweb /
remove trailing ws
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:15:37 +0000 (15:15 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 15:15:37 +0000 (15:15 +0000)
article.tex

index 29d8ca9..e6cc12a 100644 (file)
@@ -109,7 +109,7 @@ $\set X$.
 
 \item[ $ C \ge D $ ]
 $C$ is a descendant of $D$ in the git commit
-graph.  This is a partial order, namely the transitive closure of 
+graph.  This is a partial order, namely the transitive closure of
 $ D \in \set X $ where $ C \hasparents \set X $.
 
 \item[ $ C \has D $ ]
@@ -129,18 +129,18 @@ is to be taken as applying to both $\py$ and $\pn$.
 None of these sets overlap.  Hence:
 
 \item[ $ \patchof{ C } $ ]
-Either $\p$ s.t. $ C \in \p $, or $\bot$.  
+Either $\p$ s.t. $ C \in \p $, or $\bot$.
 A function from commits to patches' sets $\p$.
 
 \item[ $ \pancsof{C}{\set P} $ ]
-$ \{ A \; | \; A \le C \land A \in \set P \} $ 
+$ \{ A \; | \; A \le C \land A \in \set P \} $
 i.e. all the ancestors of $C$
 which are in $\set P$.
 
 \item[ $ \pendsof{C}{\set P} $ ]
 $ \{ E \; | \; E \in \pancsof{C}{\set P}
   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
-  E \neq A \land E \le A \} $ 
+  E \neq A \land E \le A \} $
 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 
 \item[ $ \baseof{C} $ ]
@@ -154,13 +154,13 @@ $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 
 \item[ $ C \nothaspatch \p $ ]
 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
-~ Informally, $C$ has none of the contents of $\p$.  
+~ Informally, $C$ has none of the contents of $\p$.
 
 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
 includes commits on plain git branches made by applying a Topbloke
 patch.  If a Topbloke
 patch is applied to a non-Topbloke branch and then bubbles back to
-the relevant Topbloke branches, we hope that 
+the relevant Topbloke branches, we hope that
 if the user still cares about the Topbloke patch,
 git's merge algorithm will DTRT when trying to re-apply the changes.
 
@@ -173,7 +173,7 @@ $\displaystyle D \isin C \equiv
     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
     \text{otherwise} : & D \not\isin M
   \end{cases}
-$ 
+$
 
 \end{basedescript}
 \newpage
@@ -225,7 +225,7 @@ We maintain these each time we construct a new commit. \\
 }
 
 \[ \eqn{Exclusive Tip Contents:}{
-  \bigforall_{C \in \py} 
+  \bigforall_{C \in \py}
     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
       \Bigr]
 }\]
@@ -270,7 +270,7 @@ xxx proof tbd
 \proof{
 The implication from right to left is trivial because
 $ \pends() \subset \pancs() $.
-For the implication from left to right: 
+For the implication from left to right:
 by the definition of $\mathcal E$,
 for every such $A$, either $A \in \pends()$ which implies
 $A \le M$ by the LHS directly,
@@ -288,9 +288,9 @@ by the LHS.  And $A \le A''$.
       \\
        C \not\in \p : & \displaystyle
        \left\{ E \Big|
-           \Bigl[ \Largeexists_{A \in \set A} 
+           \Bigl[ \Largeexists_{A \in \set A}
                        E \in \pendsof{A}{\set P} \Bigr] \land
-           \Bigl[ \Largenexists_{B \in \set A} 
+           \Bigl[ \Largenexists_{B \in \set A}
                        E \neq B \land E \le B \Bigr]
        \right\}
       \end{cases}
@@ -415,7 +415,7 @@ We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 Substitute into the contents of $C$:
 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
     \lor D = C \]
-Since $D = C \implies D \in \py$, 
+Since $D = C \implies D \in \py$,
 and substituting in $\baseof{C}$, this gives:
 \[ D \isin C \equiv D \isin \baseof{C} \lor
     (D \in \py \land D \le A) \lor
@@ -429,7 +429,7 @@ $\qed$
 
 \subsection{Base Acyclic}
 
-Need to consider only $A, C \in \pn$.  
+Need to consider only $A, C \in \pn$.
 
 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 
@@ -461,7 +461,7 @@ So:
 
 \subsubsection{For $A \nothaspatch P$:}
 
-Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
+Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 Thus $D \neq C$.
 
 Now by contents of $A$, $D \notin A$, so $D \notin C$.
@@ -673,7 +673,7 @@ $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 By Currently Included, $D \isin L$.
 
 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
-by Unique Tip, $D \le R^+ \equiv D \le L$.  
+by Unique Tip, $D \le R^+ \equiv D \le L$.
 So $D \isin R^+$.
 
 By Base Acyclic, $D \not\isin R^-$.
@@ -818,7 +818,7 @@ and calculate $\pendsof{C}{\pn}$.  So we will consider some
 putative ancestor $A \in \pn$ and see whether $A \le C$.
 
 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
-But $C \in py$ and $A \in \pn$ so $A \neq C$.  
+But $C \in py$ and $A \in \pn$ so $A \neq C$.
 Thus $A \le C \equiv A \le L \lor A \le R$.
 
 By Unique Base of L and Transitive Ancestors,
@@ -832,15 +832,15 @@ $A \le R \equiv A \le \baseof{R}$.
 But by Tip Merge condition on $\baseof{R}$,
 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
-Thus $A \le C \equiv A \le \baseof{R}$.  
+Thus $A \le C \equiv A \le \baseof{R}$.
 That is, $\baseof{C} = \baseof{R}$.
 
 \subsubsection{For $R \in \pn$:}
 
 By Tip Merge condition on $R$ and since $M \le R$,
 $A \le \baseof{L} \implies A \le R$, so
-$A \le R \lor A \le \baseof{L} \equiv A \le R$.  
-Thus $A \le C \equiv A \le R$.  
+$A \le R \lor A \le \baseof{L} \equiv A \le R$.
+Thus $A \le C \equiv A \le R$.
 That is, $\baseof{C} = R$.
 
 $\qed$
@@ -848,7 +848,7 @@ $\qed$
 \subsection{Coherence and Patch Inclusion}
 
 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
-This involves considering $D \in \py$.  
+This involves considering $D \in \py$.
 
 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
@@ -862,20 +862,20 @@ $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 
 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
- \equiv D \isin L \lor D \isin R$.  
+ \equiv D \isin L \lor D \isin R$.
 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 
 Consider $D \neq C, D \isin X \land D \isin Y$:
-By $\merge$, $D \isin C$.  Also $D \le X$ 
+By $\merge$, $D \isin C$.  Also $D \le X$
 so $D \le C$.  OK for $C \haspatch \p$.
 
 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
-By $\merge$, $D \not\isin C$.  
-And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
+By $\merge$, $D \not\isin C$.
+And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 OK for $C \haspatch \p$.
 
 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
-$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
+$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 OK for $C \haspatch \p$.
 
@@ -888,7 +888,7 @@ $M \nothaspatch \p \implies C \haspatch \p$.
 
 \proofstarts
 
-One of the Merge Ends conditions applies.  
+One of the Merge Ends conditions applies.
 Recall that we are considering $D \in \py$.
 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 We will show for each of
@@ -901,12 +901,12 @@ $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 
 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
-$D \le Y$ so $D \le C$.  
+$D \le Y$ so $D \le C$.
 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 
 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 $D \not\le Y$.  If $D \le X$ then
-$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
+$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 
@@ -934,7 +934,7 @@ $\qed$
 
 \subsection{Tip Contents}
 
-We need worry only about $C \in \py$.  
+We need worry only about $C \in \py$.
 And $\patchof{C} = \patchof{L}$
 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 of $C$, and its Coherence and Patch Inclusion, as just proved.