X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=01297a8fb0681c79d7ffc1933fe941f02f77adb5;hp=1f3d1647d8df7544fe1eabf8e2d8b6841b6d069b;hb=e02ac317b82e521bccdbfadda3ff9c11d6a1533d;hpb=1f1f6ab8fb22b2d8199b826de823b0167accdbbe diff --git a/article.tex b/article.tex index 1f3d164..01297a8 100644 --- a/article.tex +++ b/article.tex @@ -1,4 +1,5 @@ \documentclass[a4paper,leqno]{strayman} +\errorcontextlines=50 \let\numberwithin=\notdef \usepackage{amsmath} \usepackage{mathabx} @@ -9,6 +10,8 @@ \renewcommand{\ge}{\geqslant} \renewcommand{\le}{\leqslant} +\newcommand{\nge}{\ngeqslant} +\newcommand{\nle}{\nleqslant} \newcommand{\has}{\sqsupseteq} \newcommand{\isin}{\sqsubseteq} @@ -18,8 +21,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 +34,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,11 +55,18 @@ \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}{{\mathcal M}} +\newcommand{\mergeof}[4]{\merge(#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{\eqntag}[2]{ #2 \tag*{\mbox{#1}} } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} } -\newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} } %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}} \newcommand{\bigforall}{% @@ -59,9 +77,12 @@ {\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$} +\newcommand{\proofstarts}{{\it Proof:}} +\newcommand{\proof}[1]{\proofstarts #1 $\qed$} \newcommand{\gathbegin}{\begin{gather} \tag*{}} \newcommand{\gathnext}{\\ \tag*{}} @@ -114,7 +135,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 +156,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 \mergeof{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} @@ -174,7 +206,7 @@ Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$. So by Base Acyclic $D \isin B \implies D \notin \py$. } -\[ \corrolary{ +\[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{ \bigforall_{C \in \py} D \isin C \equiv \begin{cases} D \in \py : & D \le C \\ @@ -217,6 +249,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$, with, +\gathbegin + \mergeof{C}{L}{M}{R} +\gathnext + L \le C +\gathnext + R \le C +\end{gather} +No Replay is preserved. \proofstarts + +\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,6 +390,80 @@ $\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 + \mergeof{C}{L}{R^+}{R^-} +\end{gather} + +\subsection{Conditions} + +\[ \eqn{ Unique Tip }{ + \pendsof{L}{\pry} = \{ R^+ \} +}\] +\[ \eqn{ Currently Included }{ + L \haspatch \pry +}\] +\[ \eqn{ Not Self }{ + L \not\in \{ R^+ \} +}\] + +\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{Desired Contents} + +\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \] +\proofstarts + +\subsubsection{For $D = C$:} + +Trivially $D \isin C$. OK. + +\subsubsection{For $D \neq C, D \not\le L$:} + +By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence +$D \not\isin R^-$. Thus $D \not\isin C$. OK. + +\subsubsection{For $D \neq C, D \le L, D \in \pry$:} + +By Currently Included, $D \isin L$. + +By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by +by Unique Tip, $D \le R^+ \equiv D \le L$. +So $D \isin R^+$. + +By Base Acyclic, $D \not\isin R^-$. + +Apply $\merge$: $D \not\isin C$. OK. + +\subsubsection{For $D \neq C, D \le L, D \notin \pry$:} + +By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$. + +Apply $\merge$: $D \isin C \equiv D \isin L$. OK. + +$\qed$ + +\subsection{Unique Base} + +Need to consider only $C \in \py$, ie $L \in \py$. + +xxx tbd + +xxx need to finish anticommit + \section{Merge} Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): @@ -324,13 +472,9 @@ 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} + \mergeof{C}{L}{M}{R} \end{gather} +We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$. \subsection{Conditions} @@ -344,12 +488,132 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): \text{otherwise} : & \false \end{cases} }\] +\[ \eqn{ Removal Merge Ends }{ + X \not\haspatch \p \land + Y \haspatch \p \land + M \haspatch \p + \implies + \pendsof{Y}{\py} = \pendsof{M}{\py} +}\] +\[ \eqn{ Addition Merge Ends }{ + X \not\haspatch \p \land + Y \haspatch \p \land + M \nothaspatch \p + \implies \left[ + \bigforall_{E \in \pendsof{X}{\py}} E \le Y + \right] +}\] \subsection{No Replay} -\subsubsection{For $D=C$:} $D \isin C, D \le C$, trivial. +See No Replay for Merge Results. -\subsubsection{For $D \isin L \land D \isin R$:} -$D \isin C$. And $D \isin L +\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$ + +\subsection{Coherence and patch inclusion} + +Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$. +This involves considering $D \in \py$. + +\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:} +$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L +\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$. +Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$. + +\subsubsection{For $L \haspatch \p, R \haspatch \p$:} +$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$. +(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.) + +Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$. + +For $D \neq C$: $D \le C \equiv D \le L \lor D \le R + \equiv D \isin L \lor D \isin R$. +(Likewise $D \le C \equiv D \le X \lor D \le Y$.) + +Consider $D \neq C, D \isin X \land D \isin Y$: +By $\merge$, $D \isin C$. Also $D \le X$ +so $D \le C$. OK for $C \haspatch \p$. + +Consider $D \neq C, D \not\isin X \land D \not\isin Y$: +By $\merge$, $D \not\isin C$. +And $D \not\le X \land D \not\le Y$ so $D \not\le C$. +OK for $C \haspatch \p$. + +Remaining case, wlog, is $D \not\isin X \land D \isin Y$. +$D \not\le X$ so $D \not\le M$ so $D \not\isin M$. +Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$. +OK for $C \haspatch \p$. + +So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. + +\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:} + +$C \haspatch \p \equiv M \nothaspatch \p$. + +\proofstarts + +One of the Merge Ends conditions applies. +Recall that we are considering $D \in \py$. +$D \isin Y \equiv D \le Y$. $D \not\isin X$. +We will show for each of +various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$ +(which suffices by definition of $\haspatch$ and $\nothaspatch$). + +Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip +Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge, +$M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e. +$M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK. + +Consider $D \neq C, M \nothaspatch P, D \isin Y$: +$D \le Y$ so $D \le C$. +$D \not\isin M$ so by $\merge$, $D \isin C$. OK. + +Consider $D \neq C, M \nothaspatch P, D \not\isin Y$: +$D \not\le Y$. If $D \le X$ then +$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and +Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$. +Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK. + +Consider $D \neq C, M \haspatch P, D \isin Y$: +$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends +and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$. +Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK. + +Consider $D \neq C, M \haspatch P, D \not\isin Y$: +By $\merge$, $D \not\isin C$. OK. + +$\qed$ \end{document}