X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=ac2a99ed41eca78debab5d0cf759c11a5a373bac;hb=fc96ba0c73d771839a025fc5cb771554cf178eaa;hp=1dd625fb915d87f34687753e19ec98647e753ebe;hpb=8d7b149b51ee761db2300244444a0dd09b612b27;p=topbloke-formulae.git

diff --git a/article.tex b/article.tex
index 1dd625f..ac2a99e 100644
--- a/article.tex
+++ b/article.tex
@@ -8,6 +8,13 @@
 \usepackage{mdwlist}
 %\usepackage{accents}
 
+\usepackage{fancyhdr}
+\pagestyle{fancy}
+\lhead[\rightmark]{}
+
+\let\stdsection\section
+\renewcommand\section{\newpage\stdsection}
+
 \renewcommand{\ge}{\geqslant}
 \renewcommand{\le}{\leqslant}
 \newcommand{\nge}{\ngeqslant}
@@ -126,7 +133,7 @@ A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 are respectively the base and tip git branches.  $\p$ may be used
 where the context requires a set, in which case the statement
 is to be taken as applying to both $\py$ and $\pn$.
-None of these sets overlap.  Hence:
+All of these sets are disjoint.  Hence:
 
 \item[ $ \patchof{ C } $ ]
 Either $\p$ s.t. $ C \in \p $, or $\bot$.
@@ -156,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
@@ -207,8 +214,8 @@ We maintain these each time we construct a new commit. \\
 
 \section{Some lemmas}
 
-\[ \eqn{Alternative (overlapping) formulations defining
-  $\mergeof{C}{L}{M}{R}$:}{
+\subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
+$$
  D \isin C \equiv
   \begin{cases}
     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
@@ -217,7 +224,7 @@ We maintain these each time we construct a new commit. \\
     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
     \text{as above with L and R exchanged}
   \end{cases}
-}\]
+$$
 \proof{ ~ Truth table (ordered by original definition): \\
   \begin{tabular}{cccc|c|cc}
      $D = C$ &
@@ -239,11 +246,13 @@ We maintain these each time we construct a new commit. \\
   And original definition is symmetrical in $L$ and $R$.
 }
 
-\[ \eqn{Exclusive Tip Contents:}{
+\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 )
       \Bigr]
-}\]
+$$
 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 
 \proof{
@@ -258,9 +267,11 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
   \end{cases}
 }\]
 
-\[ \eqn{Tip Self Inpatch:}{
+\subsection{Tip Self Inpatch}
+Given Exclusive Tip Contents and Base Acyclic for $C$,
+$$
   \bigforall_{C \in \py} C \haspatch \p
-}\]
+$$
 Ie, tip commits contain their own patch.
 
 \proof{
@@ -269,18 +280,22 @@ $ \bigforall_{C \in \py}\bigforall_{D \in \py}
   D \isin C \equiv D \le C $
 }
 
-\[ \eqn{Exact Ancestors:}{
+\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
-}\]
-xxx proof tbd
+  \right]
+$$
+\proof{ ~ Trivial.}
 
-\[ \eqn{Transitive Ancestors:}{
+\subsection{Transitive Ancestors}
+$$
   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
-}\]
+$$
 
 \proof{
 The implication from right to left is trivial because
@@ -295,7 +310,8 @@ commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 by the LHS.  And $A \le A''$.
 }
 
-\[ \eqn{Calculation Of Ends:}{
+\subsection{Calculation of Ends}
+$$
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
       \begin{cases}
@@ -305,26 +321,37 @@ by the LHS.  And $A \le A''$.
        \left\{ E \Big|
            \Bigl[ \Largeexists_{A \in \set A}
                        E \in \pendsof{A}{\set P} \Bigr] \land
-           \Bigl[ \Largenexists_{B \in \set A}
-                       E \neq B \land E \le B \Bigr]
+           \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
+                       E \neq F \land E \le F \Bigr]
        \right\}
       \end{cases}
-}\]
-xxx proof tbd
+$$
+\proof{
+Trivial for $C \in \set P$.  For $C \not\in \set P$,
+$\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
+So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
+Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
+specified, then either $F$ is going to be in our result and
+disqualifies $E$, or there is some other $F'$ (or, eventually,
+an $F''$) which disqualifies $F$.
+Otherwise, $E$ meets all the conditions for $\pends$.
+}
 
-\[ \eqn{Ingredients Prevent Replay:}{
+\subsection{Ingredients Prevent Replay}
+$$
   \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]
-}\]
+$$
 \proof{
   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
   By the preconditions, there is some $A$ s.t. $D \in \set A$
@@ -332,16 +359,19 @@ xxx proof tbd
   $A \le C$ so $D \le C$.
 }
 
-\[ \eqn{Simple Foreign Inclusion:}{
+\subsection{Simple Foreign Inclusion}
+$$
   \left[
     C \hasparents \{ L \}
    \land
     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
   \right]
  \implies
+  \left[
    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
      D \isin C \equiv D \le C
-}\]
+  \right]
+$$
 \proof{
 Consider some $D$ s.t. $\patchof{D} = \bot$.
 If $D = C$, trivially true.  For $D \neq C$,
@@ -350,19 +380,21 @@ And by Exact Ancestors $D \le L \equiv D \le C$.
 So $D \isin C \equiv D \le C$.
 }
 
-\[ \eqn{Totally Foreign Contents:}{
-  \bigforall_{C \hasparents \set A}
+\subsection{Totally Foreign Contents}
+$$
    \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
    \right]
-}\]
+$$
 \proof{
 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
@@ -393,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,
@@ -407,9 +439,9 @@ because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 
 A simple single-parent forward commit $C$ as made by git-commit.
 \begin{gather}
-\tag*{} C \hasparents \{ A \} \\
-\tag*{} \patchof{C} = \patchof{A} \\
-\tag*{} D \isin C \equiv D \isin A \lor D = C
+\tag*{} C \hasparents \{ L \} \\
+\tag*{} \patchof{C} = \patchof{L} \\
+\tag*{} D \isin C \equiv D \isin L \lor D = C
 \end{gather}
 This also covers Topbloke-generated commits on plain git branches:
 Topbloke strips the metadata when exporting.
@@ -419,24 +451,23 @@ Topbloke strips the metadata when exporting.
 Ingredients Prevent Replay applies.  $\qed$
 
 \subsection{Unique Base}
-If $A, C \in \py$ then by Calculation of Ends for
-$C, \py, C \not\in \py$:
-$\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
-$\baseof{C} = \baseof{A}$. $\qed$
+If $L, C \in \py$ then by Calculation of Ends,
+$\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
+$\baseof{C} = \baseof{L}$. $\qed$
 
 \subsection{Tip Contents}
-We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
-\[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
+We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
+\[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
 Substitute into the contents of $C$:
-\[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
+\[ 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 A) \lor
+    (D \in \py \land D \le L) \lor
     (D = C \land D \in \py) \]
 \[ \equiv D \isin \baseof{C} \lor
-   [ D \in \py \land ( D \le A \lor D = C ) ] \]
+   [ D \in \py \land ( D \le L \lor D = C ) ] \]
 So by Exact Ancestors:
 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 ) \]
@@ -444,12 +475,12 @@ $\qed$
 
 \subsection{Base Acyclic}
 
-Need to consider only $A, C \in \pn$.
+Need to consider only $L, C \in \pn$.
 
 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 
-For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
-$A$, $D \isin C \implies D \not\in \py$.
+For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
+$L$, $D \isin C \implies D \not\in \py$.
 
 $\qed$
 
@@ -457,7 +488,7 @@ $\qed$
 
 Need to consider $D \in \py$
 
-\subsubsection{For $A \haspatch P, D = C$:}
+\subsubsection{For $L \haspatch P, D = C$:}
 
 Ancestors of $C$:
 $ D \le C $.
@@ -465,24 +496,24 @@ $ D \le C $.
 Contents of $C$:
 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 
-\subsubsection{For $A \haspatch P, D \neq C$:}
-Ancestors: $ D \le C \equiv D \le A $.
+\subsubsection{For $L \haspatch P, D \neq C$:}
+Ancestors: $ D \le C \equiv D \le L $.
 
-Contents: $ D \isin C \equiv D \isin A \lor f $
-so $ D \isin C \equiv D \isin A $.
+Contents: $ D \isin C \equiv D \isin L \lor f $
+so $ D \isin C \equiv D \isin L $.
 
 So:
-\[ A \haspatch P \implies C \haspatch P \]
+\[ L \haspatch P \implies C \haspatch P \]
 
-\subsubsection{For $A \nothaspatch P$:}
+\subsubsection{For $L \nothaspatch P$:}
 
-Firstly, $C \not\in \py$ since if it were, $A \in \py$.
+Firstly, $C \not\in \py$ since if it were, $L \in \py$.
 Thus $D \neq C$.
 
-Now by contents of $A$, $D \notin A$, so $D \notin C$.
+Now by contents of $L$, $D \notin L$, so $D \notin C$.
 
 So:
-\[ A \nothaspatch P \implies C \nothaspatch P \]
+\[ L \nothaspatch P \implies C \nothaspatch P \]
 $\qed$
 
 \subsection{Foreign Inclusion:}
@@ -496,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
@@ -507,11 +539,8 @@ Given $L$, create a Topbloke base branch initial commit $B$.
 
 \subsection{Conditions}
 
-\[ \eqn{ Ingredients }{
- \patchof{L} = \pa{L} \lor \patchof{L} = \bot
-}\]
 \[ \eqn{ Create Acyclic }{
- L \not\haspatch \pq
+ \pendsof{L}{\pqy} = \{ \}
 }\]
 
 \subsection{No Replay}
@@ -529,12 +558,13 @@ Not applicable.
 \subsection{Base Acyclic}
 
 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
-If $D \neq B$, $D \isin L$, and by Create Acyclic
+If $D \neq B$, $D \isin L$, so by No Replay $D \le L$
+and by Create Acyclic
 $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$.
 
@@ -553,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
@@ -583,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$
 
@@ -608,7 +640,7 @@ $$
 \subsubsection{For $\p = \pq$:}
 
 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
-By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
+By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$.  Thus $C \haspatch \pq$.
 
 \subsubsection{For $\p \neq \pq$:}
 
@@ -625,10 +657,11 @@ Simple Foreign Inclusion applies.  $\qed$
 
 Not applicable.
 
-\section{Anticommit}
+\section{Dependency Removal}
 
-Given $L$ and $\pr$ as represented by $R^+, R^-$.
-Construct $C$ which has $\pr$ removed.
+Given $L$ which contains $\pr$ as represented by $R^+, R^-$.
+Construct $C$ which has $\pr$ removed by applying a single
+commit which is the anticommit of $\pr$.
 Used for removing a branch dependency.
 \gathbegin
  C \hasparents \{ L \}
@@ -644,7 +677,7 @@ Used for removing a branch dependency.
 R^+ \in \pry \land R^- = \baseof{R^+}
 }\]
 \[ \eqn{ Into Base }{
- L \in \pn
+ L \in \pqn
 }\]
 \[ \eqn{ Unique Tip }{
  \pendsof{L}{\pry} = \{ R^+ \}
@@ -664,7 +697,7 @@ is a descendant, not an ancestor, of the 2nd parent.)
 
 \subsection{No Replay}
 
-By definition of $\merge$,
+By $\merge$,
 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
 So, by Ordering of Ingredients,
 Ingredients Prevent Replay applies.  $\qed$
@@ -680,18 +713,19 @@ Trivially $D \isin C$.  OK.
 
 \subsubsection{For $D \neq C, D \not\le L$:}
 
-By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
+By No Replay for $L$, $D \not\isin L$.
+Also, by Ordering of Ingredients, $D \not\le R^-$ hence
 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 
 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 
 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^+$.
 
-By Base Acyclic, $D \not\isin R^-$.
+By Base Acyclic for $R^-$, $D \not\isin R^-$.
 
 Apply $\merge$: $D \not\isin C$.  OK.
 
@@ -705,7 +739,7 @@ $\qed$
 
 \subsection{Unique Base}
 
-Into Base means that $C \in \pn$, so Unique Base is not
+Into Base means that $C \in \pqn$, so Unique Base is not
 applicable. $\qed$
 
 \subsection{Tip Contents}
@@ -714,11 +748,11 @@ Again, not applicable. $\qed$
 
 \subsection{Base Acyclic}
 
-By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
-And by Into Base $C \not\in \py$.
+By Into Base and Base Acyclic for $L$, $D \isin L \implies D \not\in \pqy$.
+And by Into Base $C \not\in \pqy$.
 Now from Desired Contents, above, $D \isin C
 \implies D \isin L \lor D = C$, which thus
-$\implies D \not\in \py$.  $\qed$.
+$\implies D \not\in \pqy$.  $\qed$.
 
 \subsection{Coherence and Patch Inclusion}
 
@@ -755,6 +789,37 @@ $\qed$
 
 Not applicable.
 
+\section{Dependency Insertion}
+
+Given $L$ construct $C$ which additionally
+contains $\pr$ as represented by $R^+$ and $R^-$.
+This may even be used for reintroducing a previous-removed branch
+dependency.
+\gathbegin
+ C \hasparents \{ L, R^+ \}
+\gathnext
+ \patchof{C} = \patchof{L}
+\gathnext
+ \mergeof{C}{L}{R^-}{R^+}
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Ingredients }{
+ R^- = \baseof{R^+}
+}\]
+\[ \eqn{ Into Base }{
+ L \in \pqn
+}\]
+\[ \eqn{ Currently Excluded }{
+ L \nothaspatch \pry
+}\]
+\[ \eqn{ Insertion Acyclic }{
+ R^+ \nothaspatch \pqy
+}\]
+
+xxx up to here
+
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$:
@@ -817,7 +882,7 @@ And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 Merge Ends condition applies.
 
 So a plain git merge of non-Topbloke branches meets the conditions and
-is therefore consistent with our scheme.
+is therefore consistent with our model.
 
 \subsection{No Replay}
 
@@ -867,7 +932,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$:}
@@ -911,7 +976,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.