chiark / gitweb /
index e9b5aa2..7a48a25 100644 (file)
--- a/merge.tex
+++ b/merge.tex
@@ -47,7 +47,7 @@ $L \in \pn$, $R \in \pry$, $M = \baseof{R}$.
\right]
}\]
$\eqn{ Foreign Merges }{ - \patchof{L} = \bot \equiv \patchof{R} = \bot + \patchof{L} = \bot \implies \patchof{R} = \bot }$

\subsection{Non-Topbloke merges}
@@ -59,8 +59,11 @@ branch without Topbloke's assistance, it is also forbidden to
merge any Topbloke-controlled branch into any plain git branch.

Given those conditions, Tip Merge and Merge Acyclic do not apply.
-And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
-Merge Ends condition applies.
+By Foreign Contents of $L$, $\patchof{M} = \bot$ as well.
+So by Foreign Contents for any $A \in \{L,M,R\}$,
+$\forall_{\p, D \in \py} D \not\le A$
+so $\pendsof{A}{\py} = \{ \}$ and the RHS of both Merge Ends
+conditions are satisifed.

So a plain git merge of non-Topbloke branches meets the conditions and
is therefore consistent with our model.
@@ -79,7 +82,7 @@ and calculate $\pendsof{C}{\pn}$.  So we will consider some
putative ancestor $A \in \pn$ and see whether $A \le C$.

By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
-But $C \in py$ and $A \in \pn$ so $A \neq C$.
+But $C \in \py$ and $A \in \pn$ so $A \neq C$.
Thus $A \le C \equiv A \le L \lor A \le R$.

By Unique Base of L and Transitive Ancestors,
@@ -98,7 +101,7 @@ That is, $\baseof{C} = \baseof{R}$.

\subsubsection{For $R \in \pn$:}

-By Tip Merge condition on $R$ and since $M \le R$,
+By Tip Merge condition and since $M \le R$,
$A \le \baseof{L} \implies A \le R$, so
$A \le R \lor A \le \baseof{L} \equiv A \le R$.
Thus $A \le C \equiv A \le R$.
@@ -108,19 +111,29 @@ $\qed$

\subsection{Coherence and Patch Inclusion}

-Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
-This involves considering $D \in \py$.
+$$+\begin{cases} + L \nothaspatch \p \land R \nothaspatch \p : & C \nothaspatch \p \\ + L \haspatch \p \land R \haspatch \p : & C \haspatch \p \\ + \text{otherwise} \land M \haspatch \p : & C \nothaspatch \p \\ + \text{otherwise} \land M \nothaspatch \p : & C \haspatch \p +\end{cases} +$$
+\proofstarts
+~ Consider $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 for $L$).  So $D \neq C$.
+\in \py$ie$L \haspatch \p$by Tip Own Contents for$L$). +So$D \neq C$. Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. +OK. \subsubsection{For$L \haspatch \p, R \haspatch \p$:}$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) -Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. +Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \zhaspatch \p$. For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
\equiv D \isin L \lor D \isin R$. @@ -128,55 +141,57 @@ For$D \neq C$:$D \le C \equiv D \le L \lor D \le R

Consider $D \neq C, D \isin X \land D \isin Y$:
By $\merge$, $D \isin C$.  Also $D \le X$
-so $D \le C$.  OK for $C \haspatch \p$.
+so $D \le C$.  OK for $C \zhaspatch \p$.

Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
By $\merge$, $D \not\isin C$.
And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
-OK for $C \haspatch \p$.
+OK for $C \zhaspatch \p$.

Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
-OK for $C \haspatch \p$.
+OK for $C \zhaspatch \p$.

-So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
+So, in all cases, $C \zhaspatch \p$.
+And by $L \haspatch \p$, $\exists_{F \in \py} F \le L$
+and this $F \le C$ so indeed $C \haspatch \p$.

\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}

-$M \haspatch \p \implies C \nothaspatch \p$.
-$M \nothaspatch \p \implies C \haspatch \p$.
-
-\proofstarts
-
One of the Merge Ends conditions applies.
Recall that we are considering $D \in \py$.
$D \isin Y \equiv D \le Y$.  $D \not\isin X$.
We will show for each of
-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 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.
-
-Consider $D \neq C, M \nothaspatch P, D \isin Y$:
+various cases that
+if $M \haspatch \p$, $D \not\isin C$,
+whereas if $M \nothaspatch \p$, $D \isin C \equiv D \le C$.
+And by $Y \haspatch \p$, $\exists_{F \in \py} F \le Y$ and this
+$F \le C$ so this suffices.
+
+Consider $D = C$:  Thus $C \in \py, L \in \py$.
+By Tip Own Contents, $\neg[ L \nothaspatch \p ]$ so $L \neq X$,
+therefore we must have $L=Y$, $R=X$.
+By Tip Merge $M = \baseof{L}$ so $M \in \pn$ so
+by Base Acyclic $M \nothaspatch \p$.  By $\merge$, $D \isin C$,
+and $D \le C$.  OK.
+
+Consider $D \neq C, M \nothaspatch \p, D \isin Y$:
$D \le Y$ so $D \le C$.
$D \not\isin M$ so by $\merge$, $D \isin C$.  OK.

-Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
+Consider $D \neq C, M \nothaspatch \p, D \not\isin Y$:
$D \not\le Y$.  If $D \le X$ then
$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.

-Consider $D \neq C, M \haspatch P, D \isin Y$:
+Consider $D \neq C, M \haspatch \p, D \isin Y$:
$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.

-Consider $D \neq C, M \haspatch P, D \not\isin Y$:
+Consider $D \neq C, M \haspatch \p, D \not\isin Y$:
By $\merge$, $D \not\isin C$.  OK.

$\qed$
@@ -216,8 +231,8 @@ $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D \subsubsection{For$D \not\in \py, R \not\in \py$:}$D \neq C$. By Tip Contents of$L$, -$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, -$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
+$D \isin L \equiv D \isin \baseof{L}$, so by Tip Merge condition,
+$D \isin L \equiv D \isin M$.  So by $\merge$, $D \isin C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.

@@ -229,14 +244,16 @@ By Tip Contents
$D \isin L \equiv D \isin \baseof{L}$ and
$D \isin R \equiv D \isin \baseof{R}$.

+Apply Tip Merge condition.
If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.

-So $D \isin M \equiv D \isin L$ and by $\merge$,
+So $D \isin M \equiv D \isin L$ so by $\merge$,
$D \isin C \equiv D \isin R$.  But from Unique Base,
-$\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
+$\baseof{C} = \baseof{R}$.
+Therefore $D \isin C \equiv D \isin \baseof{C}$.  OK.

$\qed$