improve "no replay for merge results" (correct conditions, remove some duplicate...

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index fde6e2f5cccd274528791679a0be616000352cca..1f7a59bd4018b2ed9aba33b8a46989dd24cb33c4 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -49,14 +49,18 @@
 
 \newcommand{\pancs}{{\mathcal A}}
 \newcommand{\pends}{{\mathcal E}}
-\newcommand{\merge}{{\mathcal M}}
 
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
-\newcommand{\mergeof}[3]{\merge ( #1 , #2, #3 ) }
 
-\newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
-\newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
+\newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
+%\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
+
+\newcommand{\patch}{{\mathcal P}}
+\newcommand{\base}{{\mathcal B}}
+
+\newcommand{\patchof}[1]{\patch ( #1 ) }
+\newcommand{\baseof}[1]{\base ( #1 ) }
 
 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
@@ -148,14 +152,16 @@ patch is applied to a non-Topbloke branch and then bubbles back to
 the Topbloke patch itself, we hope that git's merge algorithm will
 DTRT or that the user will no longer care about the Topbloke patch.
 
-\item[ $ \mergeof{L}{M}{R} $ ]
-$\displaystyle \left\{ C \middle|
+\item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
+The contents of a git merge result:
+
+$\displaystyle D \isin C \equiv
   \begin{cases}
     (D \isin L \land D \isin R) \lor D = C : & \true \\
     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
     \text{otherwise} : & D \not\isin M
   \end{cases}
- \right\} $
+$ 
 
 \end{basedescript}
 \newpage
@@ -251,6 +257,37 @@ by the LHS.  And $A \le A''$.
 }\]
 XXX proof TBD.
 
+\subsection{No Replay for Merge Results}
+
+If we are constructing $C$, given
+\gathbegin
+  \merge{C}{L}{M}{R}
+\gathnext
+  L \le C
+\gathnext
+  R \le C
+\end{gather}
+No Replay is preserved.  {\it Proof:}
+
+\subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
+
+\subsubsection{For $D \isin L \land D \isin R$:}
+$D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
+
+\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
+$D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \not\isin M$:}
+$D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
+R$ so $D \le C$.  OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \isin M$:}
+$D \not\isin C$.  OK.
+
+$\qed$
+
 \section{Commit annotation}
 
 We annotate each Topbloke commit $C$ with:
@@ -360,17 +397,24 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-   \begin{cases}
-      R \in \py : & \baseof{R} \ge \baseof{L}
-              \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
-      R \in \pn : & R \ge \baseof{L}
-              \land M = \baseof{L} \\
-      \text{otherwise} : & \false
-   \end{cases}
+ \merge{C}{L}{R^+}{R^-}
 \end{gather}
 
-xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
+\subsection{Conditions}
+
+\[ \eqn{ Unique Tip }{
+ \pendsof{L}{\pry} = \{ R^+ \}
+}\]
+\[ \eqn{ Correct Base }{
+ \baseof{R^+} = R^-
+}\]
+\[ \eqn{ Currently Included }{
+ L \haspatch \pry
+}\]
+
+
+
+xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
 
 \section{Merge}
 
@@ -380,12 +424,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-  \begin{cases}
-    (D \isin L \land D \isin R) \lor D = C : & \true \\
-    (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
-    \text{otherwise} : & D \not\isin M
-  \end{cases}
+ \merge{C}{L}{M}{R}
 \end{gather}
 
 \subsection{Conditions}
@@ -401,30 +440,9 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
    \end{cases}
 }\]
 
-\subsection{No Replay}
+\subsection{Merge Results}
 
-\subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
-
-\subsubsection{For $D \isin L \land D \isin R$:}
-$D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$.  OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$.  OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \not\isin M$:}
-$D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \isin M$:}
-$D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
-
-$\qed$
+As above.
 
 \subsection{Unique Base}