\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 $.
$
\end{basedescript}
-\newpage
+
\section{Invariants}
We maintain these each time we construct a new commit. \\
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 \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$:
\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
}\]
\[ \eqn{ Removal Merge Ends }{
X \not\haspatch \p \land
- Y \haspatch \p \land
- M \haspatch \p
+ M \haspatch \p \land
+ Y \haspatch \p
\implies
\pendsof{Y}{\py} = \pendsof{M}{\py}
}\]
\[ \eqn{ Addition Merge Ends }{
X \not\haspatch \p \land
- Y \haspatch \p \land
- M \nothaspatch \p
+ M \nothaspatch \p \land
+ Y \haspatch \p
\implies \left[
\bigforall_{E \in \pendsof{X}{\py}} E \le Y
\right]