X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=fde6e2f5cccd274528791679a0be616000352cca;hp=d85a022ff8fb8388f380325f4ffd4ed9e4330d5d;hb=139e1dd4dce6fcbc306dc4798f4cac017a0a4897;hpb=400772c417bd54383994df5a227df88adc769171 diff --git a/article.tex b/article.tex index d85a022..fde6e2f 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{>}}} @@ -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 ) } @@ -59,6 +70,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 +127,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 +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} @@ -217,6 +239,17 @@ 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} = + \Bigl\{ 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\} +}\] +XXX proof TBD. \section{Commit annotation} @@ -316,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$): @@ -334,15 +390,74 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): \subsection{Conditions} -\[ \eqn{ Merges Exhaustive }{ - L \in \py => \Bigl[ R \in \py \lor R \in \pn \Bigr] -}\] \[ \eqn{ Tip Merge }{ - L \in \py \land R \in \py \implies \Bigl[ \text{TBD} \Bigr] -}\] -\[ \eqn{ Base Merge }{ - L \in \py \land R \in \pn \implies \Bigl[ R \ge \baseof{L} \land M = - \baseof{L} \Bigr] + 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} + +\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$ + +\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}