X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=4c5f6751682c83a13e478fdb11d64496abd1bd22;hp=f8acb2260ffcf7898dd228718269b1efe9f40447;hb=1059b2343f8b2979915db881a067cd3307cdead2;hpb=0b6086688e6de7212b4e21c46b3dcaf39e4cf063 diff --git a/article.tex b/article.tex index f8acb22..4c5f675 100644 --- a/article.tex +++ b/article.tex @@ -32,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{>}}} @@ -49,8 +53,14 @@ \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) } \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) } -\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.}} } @@ -142,6 +152,17 @@ 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[ $\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} +$ + \end{basedescript} \newpage \section{Invariants} @@ -227,15 +248,46 @@ by the LHS. And $A \le A''$. \[ \eqn{Calculation Of Ends:}{ \bigforall_{C \hasparents \set A} \pendsof{C}{\set P} = - \Bigl\{ E \Big| + \left\{ E \Big| \Bigl[ \Largeexists_{A \in \set A} E \in \pendsof{A}{\set P} \Bigr] \land \Bigl[ \Largenexists_{B \in \set A} E \neq B \land E \le B \Bigr] - \Bigr\} + \right\} }\] 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: @@ -334,6 +386,45 @@ $\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 +$R^+ \in \pry, R^- = \baseof{R^+}$. +Construct $C$ which has $\pr$ removed. +Used for removing a branch dependency. +\gathbegin + C \hasparents \{ L \} +\gathnext + \patchof{C} = \patchof{L} +\gathnext + \merge{C}{L}{R^+}{R^-} +\end{gather} + +\subsection{Conditions} + +\[ \eqn{ Unique Tip }{ + \pendsof{L}{\pry} = \{ R^+ \} +}\] +\[ \eqn{ Currently Included }{ + L \haspatch \pry +}\] + +\subsection{Desired Contents} + +xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$. + +\subsection{No Replay} + +By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$ +so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for +Merge Results applies. $\qed$ + +\subsection{Unique Base} + +Need to consider only $C \in \py$, ie $L \in \py$. + +xxx tbd + \section{Merge} Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): @@ -342,12 +433,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} @@ -365,28 +451,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): \subsection{No Replay} -\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$ +See No Replay for Merge Results. \subsection{Unique Base} @@ -409,34 +474,17 @@ $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{L} \equiv A \le \baseof{R}$. -Thus $A \le C \equiv A \le \baseof{R}$. Ie, $\baseof{C} = -\baseof{R}$. +Thus $A \le C \equiv A \le \baseof{R}$. +That is, $\baseof{C} = \baseof{R}$. \subsubsection{For $R \in \pn$:} By Tip Merge condition on $R$, -$A \le \baseof{L} \implies A \le R$ - -UP TO HERE - -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{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$. -Let $A \in \pends{C}{\pn}$. -Then by Calculation Of Ends $A \in \pendsof{L,\pn} \lor A \in -\pendsof{R,\pn}$. - - - -%$\pends{C, - -%%\subsubsection{For $R \in \py$:} +$\qed$ \end{document}