chiark / gitweb /
clarifications and fixes from reread
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 17:02:50 +0000 (17:02 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 17:57:19 +0000 (17:57 +0000)
article.tex

index 1a1e9d1..40c6518 100644 (file)
@@ -163,7 +163,7 @@ $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 ~ Informally, $C$ has none of the contents of $\p$.
 
-Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
+Commits on Non-Topbloke branches 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
@@ -247,6 +247,7 @@ $$
 }
 
 \subsection{Exclusive Tip Contents}
+Given Base Acyclic for $C$,
 $$
   \bigforall_{C \in \py}
     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
@@ -267,6 +268,7 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
 }\]
 
 \subsection{Tip Self Inpatch}
+Given Exclusive Tip Contents and Base Acyclic for $C$,
 $$
   \bigforall_{C \in \py} C \haspatch \p
 $$
@@ -281,9 +283,11 @@ $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 \subsection{Exact Ancestors}
 $$
   \bigforall_{ C \hasparents \set{R} }
+  \left[
   D \le C \equiv
     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
     \lor D = C
+  \right]
 $$
 \proof{ ~ Trivial.}
 
@@ -306,7 +310,7 @@ commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 by the LHS.  And $A \le A''$.
 }
 
-\subsection{Calculation Of Ends}
+\subsection{Calculation of Ends}
 $$
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
@@ -338,12 +342,13 @@ $$
   \left[
     {C \hasparents \set A} \land
    \\
+    \bigforall_{D}
     \left(
-      D \isin C \implies
+       D \isin C \implies
        D = C \lor
        \Largeexists_{A \in \set A} D \isin A
     \right)
-  \right] \implies \left[
+  \right] \implies \left[ \bigforall_{D}
     D \isin C \implies D \le C
   \right]
 $$
@@ -377,13 +382,14 @@ So $D \isin C \equiv D \le C$.
 
 \subsection{Totally Foreign Contents}
 $$
-  \bigforall_{C \hasparents \set A}
    \left[
+    C \hasparents \set A \land
     \patchof{C} = \bot \land
       \bigforall_{A \in \set A} \patchof{A} = \bot
    \right]
   \implies
    \left[
+  \bigforall_{D}
     D \le C
    \implies
     \patchof{D} = \bot
@@ -419,7 +425,7 @@ $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
 is in stated
 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
-for the ingredients $I$),
+for the ingredients $I$)
 in the proof of Coherence for each kind of commit.
 
 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
@@ -445,8 +451,7 @@ Topbloke strips the metadata when exporting.
 Ingredients Prevent Replay applies.  $\qed$
 
 \subsection{Unique Base}
-If $L, C \in \py$ then by Calculation of Ends for
-$C, \py, C \not\in \py$:
+If $L, C \in \py$ then by Calculation of Ends,
 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
 $\baseof{C} = \baseof{L}$. $\qed$
 
@@ -457,7 +462,7 @@ Substitute into the contents of $C$:
 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
     \lor D = C \]
 Since $D = C \implies D \in \py$,
-and substituting in $\baseof{C}$, this gives:
+and substituting in $\baseof{C}$, from Unique Base above, this gives:
 \[ D \isin C \equiv D \isin \baseof{C} \lor
     (D \in \py \land D \le L) \lor
     (D = C \land D \in \py) \]
@@ -522,7 +527,8 @@ Foreign Contents applies. $\qed$
 
 \section{Create Base}
 
-Given $L$, create a Topbloke base branch initial commit $B$.
+Given a starting point $L$ and a proposed patch $\pq$,
+create a Topbloke base branch initial commit $B$.
 \gathbegin
  B \hasparents \{ L \}
 \gathnext
@@ -558,7 +564,7 @@ $D \not\in \pqy$.  $\qed$
 
 \subsection{Coherence and Patch Inclusion}
 
-Consider some $D \in \p$.
+Consider some $D \in \py$.
 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
 and $D \le B \equiv D \le L$.
 
@@ -577,7 +583,8 @@ Not applicable.
 
 \section{Create Tip}
 
-Given a Topbloke base $B$, create a tip branch initial commit B.
+Given a Topbloke base $B$ for a patch $\pq$,
+create a tip branch initial commit B.
 \gathbegin
  C \hasparents \{ B \}
 \gathnext
@@ -607,9 +614,10 @@ Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
 
 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 
-If $D \neq C$, $D \isin C \equiv D \isin B$.
+If $D \neq C$, $D \isin C \equiv D \isin B$,
+which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
-So $D \isin C \equiv D \isin \baseof{B}$.
+
 
 $\qed$
 
@@ -711,7 +719,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 Tip Self Inpatch for $R^+$, $D \isin R^+ \equiv D \le R^+$, but by
 by Unique Tip, $D \le R^+ \equiv D \le L$.
 So $D \isin R^+$.
 
@@ -891,7 +899,7 @@ 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
-\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
+\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch for $L$).  So $D \neq C$.
 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 
 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
@@ -935,7 +943,7 @@ various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 
 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
-Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
+Self Inpatch for $L$, $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 $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.