From 1a483b6d7f338927038929e6d5e71bb506cea007 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 12 Mar 2012 17:02:50 +0000 Subject: [PATCH] clarifications and fixes from reread --- article.tex | 42 +++++++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/article.tex b/article.tex index 1a1e9d1..40c6518 100644 --- a/article.tex +++ b/article.tex @@ -163,7 +163,7 @@ $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $. $\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 @@ -558,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$. @@ -577,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 @@ -607,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$ @@ -711,7 +719,7 @@ $D \not\isin R^-$. Thus $D \not\isin C$. OK. 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^+$. @@ -891,7 +899,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$:} @@ -935,7 +943,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. -- 2.30.2