wip experiment merge

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index cae101934b5275e33c485a243e359eaca8e01e0d..fde6e2f5cccd274528791679a0be616000352cca 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -1,4 +1,5 @@
 \documentclass[a4paper,leqno]{strayman}
+\errorcontextlines=50
 \let\numberwithin=\notdef
 \usepackage{amsmath}
 \usepackage{mathabx}
@@ -18,8 +19,12 @@
 \newcommand{\haspatch}{\sqSupset}
 \newcommand{\patchisin}{\sqSubset}
 
-\newcommand{\set}[1]{\mathbb #1}
-\newcommand{\pa}[1]{\varmathbb #1}
+        \newif\ifhidehack\hidehackfalse
+        \DeclareRobustCommand\hidefromedef[2]{%
+          \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
+        \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
+
+\newcommand{\set}[1]{\mathbb{#1}}
 \newcommand{\pay}[1]{\pa{#1}^+}
 \newcommand{\pan}[1]{\pa{#1}^-}
 
@@ -27,6 +32,10 @@
 \newcommand{\py}{\pay{P}}
 \newcommand{\pn}{\pan{P}}
 
+\newcommand{\pr}{\pa{R}}
+\newcommand{\pry}{\pay{R}}
+\newcommand{\prn}{\pan{R}}
+
 %\newcommand{\hasparents}{\underaccent{1}{>}}
 %\newcommand{\hasparents}{{%
 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
@@ -40,9 +49,11 @@
 
 \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 ) }
@@ -137,6 +148,15 @@ 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|
+  \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
 \section{Invariants}
@@ -329,6 +349,29 @@ $\qed$
 If $D = C$, trivial.  For $D \neq C$:
 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 
+\section{Anticommit}
+
+Given $L, R^+, R^-$ where
+$\patchof{R^+} = \pry, \patchof{R^-} = \prn$.  
+Construct $C$ which has $\pr$ removed.
+Used for removing a branch dependency.
+\gathbegin
+ C \hasparents \{ L \}
+\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}
+\end{gather}
+
+xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
+
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
@@ -389,46 +432,32 @@ Need to consider only $C \in \py$, ie $L \in \py$,
 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 putative ancestor $A \in \pn$ and see whether $A \le C$.
 
-$A \le C \equiv A \le L \lor A \le R \lor A = 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$.  
-Thus $A \le L \lor A \le R$.
+Thus $A \le C \equiv A \le L \lor A \le R$.
 
 By Unique Base of L and Transitive Ancestors,
 $A \le L \equiv A \le \baseof{L}$.
 
-\subsubsection{For $R \in FIXME py$:}
+\subsubsection{For $R \in \py$:}
 
 By Unique Base of $R$ and Transitive Ancestors,
 $A \le R \equiv A \le \baseof{R}$.
 
 But by Tip Merge condition on $\baseof{R}$,
 $A \le \baseof{L} \implies A \le \baseof{R}$, so
-$A \le \baseof{R} \lor A \le \baseof{R} \equiv A \le \baseof{R}$.
-Thus $A \le C \equiv A \le \baseof{R}$.  Ie, $\baseof{C} =
-\baseof{R}$.
-
-UP TO HERE
-
-By Tip Merge, $A \le $
-
-Let $S =
-   \begin{cases} 
-     R \in \py : & \baseof{R} \\
-     R \in \pn : & R
-   \end{cases}$.  
-Then by Tip Merge $S \ge \baseof{L}$, and $R \ge S$ so $C \ge S$.
-   
-Consider some $A \in \pn$.  If $A \le S$ then $A \le C$.
-If $A \not\le S$ then 
+$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
+Thus $A \le C \equiv A \le \baseof{R}$.  
+That is, $\baseof{C} = \baseof{R}$.
 
-Let $A \in \pends{C}{\pn}$.  
-Then by Calculation Of Ends $A \in \pendsof{L,\pn} \lor A \in
-\pendsof{R,\pn}$.
+\subsubsection{For $R \in \pn$:}
 
+By Tip Merge condition on $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$.  
+That is, $\baseof{C} = R$.
 
-
-%$\pends{C,
-
-%%\subsubsection{For $R \in \py$:}
+$\qed$
 
 \end{document}