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=a650f36ab9080f36c344bbb75ba27d0a6ce71837;hb=1059b2343f8b2979915db881a067cd3307cdead2;hpb=cdc4fccc58272bf57af3e04679d0cc10aaa9b09b diff --git a/article.tex b/article.tex index a650f36..4c5f675 100644 --- 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{>}}} @@ -44,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.}} } @@ -59,6 +74,8 @@ {\hbox{\scriptsize$\forall$}}}% } +\newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}} +\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}} \newcommand{\qed}{\square} \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$} @@ -114,7 +131,7 @@ which are in $\set P$. \item[ $ \pendsof{C}{\set P} $ ] $ \{ E \; | \; E \in \pancsof{C}{\set P} \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}} - A \neq E \land E \le A \} $ + E \neq A \land E \le A \} $ i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$. \item[ $ \baseof{C} $ ] @@ -135,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} @@ -217,6 +245,48 @@ in which case we repeat for $A'$. Since there are finitely many commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$ by the LHS. And $A \le A''$. } +\[ \eqn{Calculation Of Ends:}{ + \bigforall_{C \hasparents \set A} + \pendsof{C}{\set P} = + \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] + \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} @@ -316,4 +386,105 @@ $\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$): +\gathbegin + C \hasparents \{ L, R \} +\gathnext + \patchof{C} = \patchof{L} +\gathnext + \merge{C}{L}{M}{R} +\end{gather} + +\subsection{Conditions} + +\[ \eqn{ Tip Merge }{ + L \in \py \implies + \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} +}\] + +\subsection{No Replay} + +See No Replay for Merge Results. + +\subsection{Unique Base} + +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$. + +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 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 \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{L} \equiv A \le \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$, 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$. + +$\qed$ + \end{document}