X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;ds=sidebyside;f=article.tex;h=6be7a681549b3164b2a56e3d511dc8cac9c8b719;hb=c759fdf5965e18b0fc6f713b22526ec9464ed7f7;hp=65ef0246e5c5d6f21c38aa31511f1841d0d837f1;hpb=cd9af43c46f44d374540720e9ed4b0339be65199;p=topbloke-formulae.git diff --git a/article.tex b/article.tex index 65ef024..6be7a68 100644 --- a/article.tex +++ b/article.tex @@ -133,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$. @@ -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$ @@ -632,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$:} @@ -649,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 \} @@ -668,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^+ \} @@ -688,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$ @@ -704,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. @@ -729,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} @@ -738,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} @@ -779,6 +789,59 @@ $\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 +}\] + +\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$. + +xxx up to here + \section{Merge} Merge commits $L$ and $R$ using merge base $M$: @@ -841,7 +904,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} @@ -891,7 +954,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 +998,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.