X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=45acbb30bf9573e9b76e72109f8a04c2cc85d126;hb=8addc4c379707bd89ab14defc11914a85ee45254;hp=f7ce2c2ad0fcbfc0f45f63b522a8c16c195e4590;hpb=a4160f5fbb014fc2a7523e962996b0a35fdcc161;p=topbloke-formulae.git diff --git a/article.tex b/article.tex index f7ce2c2..45acbb3 100644 --- a/article.tex +++ b/article.tex @@ -133,7 +133,7 @@ A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which are respectively the base and tip git branches. $\p$ may be used where the context requires a set, in which case the statement is to be taken as applying to both $\py$ and $\pn$. -None of these sets overlap. Hence: +All of these sets are disjoint. Hence: \item[ $ \patchof{ C } $ ] Either $\p$ s.t. $ C \in \p $, or $\bot$. @@ -157,13 +157,13 @@ See Unique Base, below. \item[ $ C \haspatch \p $ ] $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $. -~ Informally, $C$ has the contents of $\p$. +~ Informally, $C$ has all the reachable contents of $\p$. \item[ $ C \nothaspatch \p $ ] $\displaystyle \bigforall_{D \in \py} D \not\isin C $. ~ Informally, $C$ has none of the contents of $\p$. -Non-Topbloke commits are $\nothaspatch \p$ for all $\p$. This +Commits on Non-Topbloke branches are $\nothaspatch \p$ for all $\p$. This includes commits on plain git branches made by applying a Topbloke patch. If a Topbloke patch is applied to a non-Topbloke branch and then bubbles back to @@ -247,6 +247,7 @@ $$ } \subsection{Exclusive Tip Contents} +Given Base Acyclic for $C$, $$ \bigforall_{C \in \py} \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C ) @@ -267,6 +268,7 @@ So by Base Acyclic $D \isin B \implies D \notin \py$. }\] \subsection{Tip Self Inpatch} +Given Exclusive Tip Contents and Base Acyclic for $C$, $$ \bigforall_{C \in \py} C \haspatch \p $$ @@ -281,9 +283,11 @@ $ \bigforall_{C \in \py}\bigforall_{D \in \py} \subsection{Exact Ancestors} $$ \bigforall_{ C \hasparents \set{R} } + \left[ D \le C \equiv ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R ) \lor D = C + \right] $$ \proof{ ~ Trivial.} @@ -306,7 +310,7 @@ commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$ by the LHS. And $A \le A''$. } -\subsection{Calculation Of Ends} +\subsection{Calculation of Ends} $$ \bigforall_{C \hasparents \set A} \pendsof{C}{\set P} = @@ -338,12 +342,13 @@ $$ \left[ {C \hasparents \set A} \land \\ + \bigforall_{D} \left( - D \isin C \implies + D \isin C \implies D = C \lor \Largeexists_{A \in \set A} D \isin A \right) - \right] \implies \left[ + \right] \implies \left[ \bigforall_{D} D \isin C \implies D \le C \right] $$ @@ -377,13 +382,14 @@ So $D \isin C \equiv D \le C$. \subsection{Totally Foreign Contents} $$ - \bigforall_{C \hasparents \set A} \left[ + C \hasparents \set A \land \patchof{C} = \bot \land \bigforall_{A \in \set A} \patchof{A} = \bot \right] \implies \left[ + \bigforall_{D} D \le C \implies \patchof{D} = \bot @@ -419,7 +425,7 @@ $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$ is in stated (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$ -for the ingredients $I$), +for the ingredients $I$) in the proof of Coherence for each kind of commit. $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits, @@ -445,8 +451,7 @@ Topbloke strips the metadata when exporting. Ingredients Prevent Replay applies. $\qed$ \subsection{Unique Base} -If $L, C \in \py$ then by Calculation of Ends for -$C, \py, C \not\in \py$: +If $L, C \in \py$ then by Calculation of Ends, $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so $\baseof{C} = \baseof{L}$. $\qed$ @@ -457,7 +462,7 @@ Substitute into the contents of $C$: \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \lor D = C \] Since $D = C \implies D \in \py$, -and substituting in $\baseof{C}$, this gives: +and substituting in $\baseof{C}$, from Unique Base above, this gives: \[ D \isin C \equiv D \isin \baseof{C} \lor (D \in \py \land D \le L) \lor (D = C \land D \in \py) \] @@ -522,7 +527,8 @@ Foreign Contents applies. $\qed$ \section{Create Base} -Given $L$, create a Topbloke base branch initial commit $B$. +Given a starting point $L$ and a proposed patch $\pq$, +create a Topbloke base branch initial commit $B$. \gathbegin B \hasparents \{ L \} \gathnext @@ -533,9 +539,6 @@ Given $L$, create a Topbloke base branch initial commit $B$. \subsection{Conditions} -\[ \eqn{ Ingredients }{ - \patchof{L} = \pa{L} \lor \patchof{L} = \bot -}\] \[ \eqn{ Create Acyclic }{ \pendsof{L}{\pqy} = \{ \} }\] @@ -561,7 +564,7 @@ $D \not\in \pqy$. $\qed$ \subsection{Coherence and Patch Inclusion} -Consider some $D \in \p$. +Consider some $D \in \py$. $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$ and $D \le B \equiv D \le L$. @@ -580,7 +583,8 @@ Not applicable. \section{Create Tip} -Given a Topbloke base $B$, create a tip branch initial commit B. +Given a Topbloke base $B$ for a patch $\pq$, +create a tip branch initial commit B. \gathbegin C \hasparents \{ B \} \gathnext @@ -610,9 +614,10 @@ Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$ Consider some arbitrary commit $D$. If $D = C$, trivially satisfied. -If $D \neq C$, $D \isin C \equiv D \isin B$. +If $D \neq C$, $D \isin C \equiv D \isin B$, +which by Unique Base, above, $ \equiv D \isin \baseof{B}$. By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$. -So $D \isin C \equiv D \isin \baseof{B}$. + $\qed$ @@ -635,7 +640,7 @@ $$ \subsubsection{For $\p = \pq$:} By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$. -By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$. +By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$. Thus $C \haspatch \pq$. \subsubsection{For $\p \neq \pq$:} @@ -654,7 +659,7 @@ Not applicable. \section{Anticommit} -Given $L$ and $\pr$ as represented by $R^+, R^-$. +Given $L$ which contains $\pr$ as represented by $R^+, R^-$. Construct $C$ which has $\pr$ removed. Used for removing a branch dependency. \gathbegin @@ -671,7 +676,7 @@ Used for removing a branch dependency. R^+ \in \pry \land R^- = \baseof{R^+} }\] \[ \eqn{ Into Base }{ - L \in \pn + L \in \pqn }\] \[ \eqn{ Unique Tip }{ \pendsof{L}{\pry} = \{ R^+ \} @@ -691,7 +696,7 @@ is a descendant, not an ancestor, of the 2nd parent.) \subsection{No Replay} -By definition of $\merge$, +By $\merge$, $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$. So, by Ordering of Ingredients, Ingredients Prevent Replay applies. $\qed$ @@ -707,18 +712,19 @@ 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 +By No Replay for $L$, $D \not\isin L$. +Also, by Ordering of Ingredients, $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 Tip Self Inpatch for $R^+$, $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^-$. +By Base Acyclic for $R^-$, $D \not\isin R^-$. Apply $\merge$: $D \not\isin C$. OK. @@ -732,7 +738,7 @@ $\qed$ \subsection{Unique Base} -Into Base means that $C \in \pn$, so Unique Base is not +Into Base means that $C \in \pqn$, so Unique Base is not applicable. $\qed$ \subsection{Tip Contents} @@ -741,11 +747,11 @@ Again, not applicable. $\qed$ \subsection{Base Acyclic} -By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$. -And by Into Base $C \not\in \py$. +By Into Base and Base Acyclic for $L$, $D \isin L \implies D \not\in \pqy$. +And by Into Base $C \not\in \pqy$. Now from Desired Contents, above, $D \isin C \implies D \isin L \lor D = C$, which thus -$\implies D \not\in \py$. $\qed$. +$\implies D \not\in \pqy$. $\qed$. \subsection{Coherence and Patch Inclusion} @@ -794,6 +800,9 @@ Merge commits $L$ and $R$ using merge base $M$: \end{gather} We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$. +This can also be used for dependency re-insertion, by setting +$L \in \pn$, $R \in \pry$, $M = \baseof{R}$. + \subsection{Conditions} \[ \eqn{ Ingredients }{ M \le L, M \le R @@ -814,15 +823,15 @@ We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$. }\] \[ \eqn{ Removal Merge Ends }{ X \not\haspatch \p \land - Y \haspatch \p \land - M \haspatch \p + M \haspatch \p \land + Y \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 + M \nothaspatch \p \land + Y \haspatch \p \implies \left[ \bigforall_{E \in \pendsof{X}{\py}} E \le Y \right] @@ -844,7 +853,7 @@ And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither Merge Ends condition applies. So a plain git merge of non-Topbloke branches meets the conditions and -is therefore consistent with our scheme. +is therefore consistent with our model. \subsection{No Replay} @@ -894,7 +903,7 @@ 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$. +\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch for $L$). So $D \neq C$. Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$. \subsubsection{For $L \haspatch \p, R \haspatch \p$:} @@ -938,7 +947,7 @@ 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, +Self Inpatch for $L$, $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.