\item[ $ C \haspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
-~ Informally, $C$ has the contents of $\p$.
+~ Informally, $C$ has all the reachable contents of $\p$.
\item[ $ C \nothaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
Not applicable.
-\section{Dependency Removal}
+\section{Anticommit}
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$.
+Construct $C$ which has $\pr$ removed.
Used for removing a branch dependency.
\gathbegin
C \hasparents \{ L \}
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$
-
\section{Merge}
Merge commits $L$ and $R$ using merge base $M$:
\end{gather}
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
+This can also be used for dependency re-insertion, by setting
+$L \in \pn$, $R \in \pry$, $M = \baseof{R}$.
+
\subsection{Conditions}
\[ \eqn{ Ingredients }{
M \le L, M \le R
~ian / topbloke-formulae.git / blobdiff