X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=0ed90a67314921007898565e28874630769e8908;hb=12818e0da31738adbaecf129c1e697633d371cf8;hp=321914746537919ca730ce384393fe522d268862;hpb=01c84a4814d7ab659483e8a4cc3fb6aa7c90faa1;p=topbloke-formulae.git diff --git a/article.tex b/article.tex index 3219147..0ed90a6 100644 --- a/article.tex +++ b/article.tex @@ -657,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 \} @@ -676,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^+ \} @@ -696,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$ @@ -712,7 +713,8 @@ 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$:} @@ -723,7 +725,7 @@ 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. @@ -737,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} @@ -746,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} @@ -787,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$: