X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=0ed90a67314921007898565e28874630769e8908;hp=ed6ce526885a0729b74c091398edf032659c8b04;hb=12818e0da31738adbaecf129c1e697633d371cf8;hpb=c517a34b73ff5df3f28591b2a2b1c0c312f13df8 diff --git a/article.tex b/article.tex index ed6ce52..0ed90a6 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 -}\] + \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} @@ -309,7 +325,7 @@ by the LHS. And $A \le A''$. E \neq F \land E \le F \Bigr] \right\} \end{cases} -}\] +$$ \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}$. @@ -321,19 +337,21 @@ 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$ @@ -341,16 +359,19 @@ Otherwise, $E$ meets all the conditions for $\pends$. $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$, @@ -359,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 @@ -402,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, @@ -428,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$ @@ -440,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) \] @@ -505,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 @@ -516,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} @@ -538,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$. @@ -562,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 @@ -592,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$ @@ -617,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$:} @@ -634,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 \} @@ -653,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^+ \} @@ -673,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$ @@ -689,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. @@ -714,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} @@ -723,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} @@ -764,6 +789,125 @@ $\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 \pr +}\] +\[ \eqn{ Inserted's Ends }{ + E \in \pendsof{L}{\pry} \implies E \le R^+ +}\] +\[ \eqn{ Others' Ends }{ + \bigforall_{\p \patchisin \L} + E \in \pendsof{R^+}{\py} \implies E \le L +}\] +\[ \eqn{ Insertion Acyclic }{ + R^+ \nothaspatch \pq +}\] + +\subsection{No Replay} + +By $\merge$, +$D \isin C \implies D \isin L \lor D \isin R^+ \lor D = C$. +So Ingredients Prevent Replay applies. $\qed$ + +\subsection{Unique Base} + +Not applicable. + +\subsection{Tip Contents} + +Not applicable. + +\subsection{Base Acyclic} + +Consider some $D \isin C$. We will show that $D \not\in \pqy$. +By $\merge$, $D \isin L \lor D \isin R^+ \lor D = C$. + +For $D \isin L$, Base Acyclic for L suffices. For $D \isin R^+$, +Insertion Acyclic suffices. For $D = C$, trivial. $\qed$. + +\subsection{Coherence and Patch Inclusion} + +$$ +\begin{cases} + \p = \pr \lor L \haspatch \p : & C \haspatch \p \\ + \p \neq \pr \land L \nothaspatch \p : & C \nothaspatch \p +\end{cases} +$$ +\proofstarts +~ Consider some $D \in \py$. +$D \neq C$ so $D \le C \equiv D \le L \lor D \le R^+$. + +\subsubsection{For $\p = \pr$:} + +$D \not\isin L$ by Currently Excluded. +$D \not\isin R^-$ by Base Acyclic. +So by $\merge$, $D \isin C \equiv D \isin R^+$, +which by Tip Self Inpatch of $R^+$, $\equiv D \le R^+$. + +And by definition of $\pancs$, +$D \le L \equiv D \in \pancsof{L}{R^+}$. +Applying Transitive Ancestors to Inserted's Ends gives +$A \in \pancsof{L}{R^+} \implies A \le R^+$. +So $D \le L \implies D \le R^+$. +Thus $D \le C \equiv D \le R^+$. + +So $D \isin C \equiv D \le C$, i.e. $C \haspatch \pr$. +OK. + +\subsubsection{For $\p \neq \pr$:} + +By Exclusive Tip Contents for $R^+$ ($D \not\in \pry$ case) +$D \isin R^+ \equiv D \isin R^-$. +So by $\merge$, $D \isin C \equiv D \isin L$. + +If $L \nothaspatch \p$, $D \not\isin L$ so $C \nothaspatch \p$. OK. + +If $L \haspatch \p$, Others' Ends applies; by Transitive +Ancestors, $A \in \pancsof{R^+}{\py} \implies A \le L$. +So $D \le R^+ \implies D \le L$, +since $D \le R^+ \equiv D \in \pancsof{R^+}{\py}$. +Thus $D \le C \equiv D \le L$. +And by $\haspatch$, $D \le L \equiv D \isin L$ so +$D \isin C \equiv D \le C$. Thus $C \haspatch \p$. +OK. + +$\qed$ + +\subsection{Foreign Inclusion} + +Consider some $D$ s.t. $\patchof{D} = \bot$. + +By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$. +So by $\merge$, $D \isin C \equiv D \isin L$. + +xxx up to here, need new condition + +$D \neq C$. + + + \section{Merge} Merge commits $L$ and $R$ using merge base $M$: @@ -826,7 +970,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} @@ -876,7 +1020,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$:} @@ -920,7 +1064,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.