1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
14 \newcommand{\has}{\sqsupseteq}
15 \newcommand{\isin}{\sqsubseteq}
17 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
18 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
19 \newcommand{\haspatch}{\sqSupset}
20 \newcommand{\patchisin}{\sqSubset}
22 \newif\ifhidehack\hidehackfalse
23 \DeclareRobustCommand\hidefromedef[2]{%
24 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
25 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
27 \newcommand{\set}[1]{\mathbb{#1}}
28 \newcommand{\pay}[1]{\pa{#1}^+}
29 \newcommand{\pan}[1]{\pa{#1}^-}
31 \newcommand{\p}{\pa{P}}
32 \newcommand{\py}{\pay{P}}
33 \newcommand{\pn}{\pan{P}}
35 %\newcommand{\hasparents}{\underaccent{1}{>}}
36 %\newcommand{\hasparents}{{%
37 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
38 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
39 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
41 \renewcommand{\implies}{\Rightarrow}
42 \renewcommand{\equiv}{\Leftrightarrow}
43 \renewcommand{\land}{\wedge}
44 \renewcommand{\lor}{\vee}
46 \newcommand{\pancs}{{\mathcal A}}
47 \newcommand{\pends}{{\mathcal E}}
49 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
50 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
52 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
53 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
55 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
56 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
58 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
59 \newcommand{\bigforall}{%
61 {\hbox{\huge$\forall$}}%
62 {\hbox{\Large$\forall$}}%
63 {\hbox{\normalsize$\forall$}}%
64 {\hbox{\scriptsize$\forall$}}}%
67 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
68 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
70 \newcommand{\qed}{\square}
71 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
73 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
74 \newcommand{\gathnext}{\\ \tag*{}}
77 \newcommand{\false}{f}
85 \desclabelstyle{\nextlinelabel}
87 \item[ $ C \hasparents \set X $ ]
88 The parents of commit $C$ are exactly the set
92 $C$ is a descendant of $D$ in the git commit
93 graph. This is a partial order, namely the transitive closure of
94 $ D \in \set X $ where $ C \hasparents \set X $.
97 Informally, the tree at commit $C$ contains the change
98 made in commit $D$. Does not take account of deliberate reversions by
99 the user or reversion, rebasing or rewinding in
100 non-Topbloke-controlled branches. For merges and Topbloke-generated
101 anticommits or re-commits, the ``change made'' is only to be thought
102 of as any conflict resolution. This is not a partial order because it
105 \item[ $ \p, \py, \pn $ ]
106 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
107 are respectively the base and tip git branches. $\p$ may be used
108 where the context requires a set, in which case the statement
109 is to be taken as applying to both $\py$ and $\pn$.
110 All these sets are distinct. Hence:
112 \item[ $ \patchof{ C } $ ]
113 Either $\p$ s.t. $ C \in \p $, or $\bot$.
114 A function from commits to patches' sets $\p$.
116 \item[ $ \pancsof{C}{\set P} $ ]
117 $ \{ A \; | \; A \le C \land A \in \set P \} $
118 i.e. all the ancestors of $C$
119 which are in $\set P$.
121 \item[ $ \pendsof{C}{\set P} $ ]
122 $ \{ E \; | \; E \in \pancsof{C}{\set P}
123 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
124 E \neq A \land E \le A \} $
125 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
127 \item[ $ \baseof{C} $ ]
128 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
129 A partial function from commits to commits.
130 See Unique Base, below.
132 \item[ $ C \haspatch \p $ ]
133 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
134 ~ Informally, $C$ has the contents of $\p$.
136 \item[ $ C \nothaspatch \p $ ]
137 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
138 ~ Informally, $C$ has none of the contents of $\p$.
140 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
141 patch is applied to a non-Topbloke branch and then bubbles back to
142 the Topbloke patch itself, we hope that git's merge algorithm will
143 DTRT or that the user will no longer care about the Topbloke patch.
149 We maintain these each time we construct a new commit. \\
151 C \has D \implies C \ge D
153 \[\eqn{Unique Base:}{
154 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
156 \[\eqn{Tip Contents:}{
157 \bigforall_{C \in \py} D \isin C \equiv
158 { D \isin \baseof{C} \lor \atop
159 (D \in \py \land D \le C) }
161 \[\eqn{Base Acyclic:}{
162 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
165 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
167 \[\eqn{Foreign Inclusion:}{
168 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
171 \section{Some lemmas}
173 \[ \eqn{Exclusive Tip Contents:}{
174 \bigforall_{C \in \py}
175 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
178 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
181 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
182 So by Base Acyclic $D \isin B \implies D \notin \py$.
185 \bigforall_{C \in \py} D \isin C \equiv
187 D \in \py : & D \le C \\
188 D \not\in \py : & D \isin \baseof{C}
192 \[ \eqn{Tip Self Inpatch:}{
193 \bigforall_{C \in \py} C \haspatch \p
195 Ie, tip commits contain their own patch.
198 Apply Exclusive Tip Contents to some $D \in \py$:
199 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
200 D \isin C \equiv D \le C $
203 \[ \eqn{Exact Ancestors:}{
204 \bigforall_{ C \hasparents \set{R} }
206 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
210 \[ \eqn{Transitive Ancestors:}{
211 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
212 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
216 The implication from right to left is trivial because
217 $ \pends() \subset \pancs() $.
218 For the implication from left to right:
219 by the definition of $\mathcal E$,
220 for every such $A$, either $A \in \pends()$ which implies
221 $A \le M$ by the LHS directly,
222 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
223 in which case we repeat for $A'$. Since there are finitely many
224 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
225 by the LHS. And $A \le A''$.
227 \[ \eqn{Calculation Of Ends:}{
228 \bigforall_{C \hasparents \set A}
229 \pendsof{C}{\set P} =
231 \Bigl[ \Largeexists_{A \in \set A}
232 E \in \pendsof{A}{\set P} \Bigr] \land
233 \Bigl[ \Largenexists_{B \in \set A}
234 E \neq B \land E \le B \Bigr]
239 \section{Commit annotation}
241 We annotate each Topbloke commit $C$ with:
245 \baseof{C}, \text{ if } C \in \py
248 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
250 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
253 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
254 make it wrong to make plain commits with git because the recorded $\pends$
255 would have to be updated. The annotation is not needed because
256 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
258 \section{Simple commit}
260 A simple single-parent forward commit $C$ as made by git-commit.
262 \tag*{} C \hasparents \{ A \} \\
263 \tag*{} \patchof{C} = \patchof{A} \\
264 \tag*{} D \isin C \equiv D \isin A \lor D = C
267 \subsection{No Replay}
270 \subsection{Unique Base}
271 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
273 \subsection{Tip Contents}
274 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
275 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
276 Substitute into the contents of $C$:
277 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
279 Since $D = C \implies D \in \py$,
280 and substituting in $\baseof{C}$, this gives:
281 \[ D \isin C \equiv D \isin \baseof{C} \lor
282 (D \in \py \land D \le A) \lor
283 (D = C \land D \in \py) \]
284 \[ \equiv D \isin \baseof{C} \lor
285 [ D \in \py \land ( D \le A \lor D = C ) ] \]
286 So by Exact Ancestors:
287 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
291 \subsection{Base Acyclic}
293 Need to consider only $A, C \in \pn$.
295 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
297 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
298 $A$, $D \isin C \implies D \not\in \py$. $\qed$
300 \subsection{Coherence and patch inclusion}
302 Need to consider $D \in \py$
304 \subsubsection{For $A \haspatch P, D = C$:}
310 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
312 \subsubsection{For $A \haspatch P, D \neq C$:}
313 Ancestors: $ D \le C \equiv D \le A $.
315 Contents: $ D \isin C \equiv D \isin A \lor f $
316 so $ D \isin C \equiv D \isin A $.
319 \[ A \haspatch P \implies C \haspatch P \]
321 \subsubsection{For $A \nothaspatch P$:}
323 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
326 Now by contents of $A$, $D \notin A$, so $D \notin C$.
329 \[ A \nothaspatch P \implies C \nothaspatch P \]
332 \subsection{Foreign inclusion:}
334 If $D = C$, trivial. For $D \neq C$:
335 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
339 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
341 C \hasparents \{ L, R \}
343 \patchof{C} = \patchof{L}
347 (D \isin L \land D \isin R) \lor D = C : & \true \\
348 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
349 \text{otherwise} : & D \not\isin M
353 \subsection{Conditions}
355 \[ \eqn{ Tip Merge }{
358 R \in \py : & \baseof{R} \ge \baseof{L}
359 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
360 R \in \pn : & R \ge \baseof{L}
361 \land M = \baseof{L} \\
362 \text{otherwise} : & \false
366 \subsection{No Replay}
368 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
370 \subsubsection{For $D \isin L \land D \isin R$:}
371 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
373 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
376 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
379 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
380 \land D \not\isin M$:}
381 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
384 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
386 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
391 \subsection{Unique Base}
393 Need to consider only $C \in \py$, ie $L \in \py$,
394 and calculate $\pendsof{C}{\pn}$. So we will consider some
395 putative ancestor $A \in \pn$ and see whether $A \le C$.
397 $A \le C \equiv A \le L \lor A \le R \lor A = C$.
398 But $C \in py$ and $A \in \pn$ so $A \neq C$.
399 Thus $fixme this is not really the right thing A \le L \lor A \le R$.
401 By Unique Base of L and Transitive Ancestors,
402 $A \le L \equiv A \le \baseof{L}$.
404 \subsubsection{For $R \in \py$:}
406 By Unique Base of $R$ and Transitive Ancestors,
407 $A \le R \equiv A \le \baseof{R}$.
409 But by Tip Merge condition on $\baseof{R}$,
410 $A \le \baseof{L} \implies A \le \baseof{R}$, so
411 $A \le \baseof{R} \lor A \le \baseof{R} \equiv A \le \baseof{R}$.
412 Thus $A \le C \equiv A \le \baseof{R}$. Ie, $\baseof{C} =
417 By Tip Merge, $A \le $
421 R \in \py : & \baseof{R} \\
424 Then by Tip Merge $S \ge \baseof{L}$, and $R \ge S$ so $C \ge S$.
426 Consider some $A \in \pn$. If $A \le S$ then $A \le C$.
427 If $A \not\le S$ then
429 Let $A \in \pends{C}{\pn}$.
430 Then by Calculation Of Ends $A \in \pendsof{L,\pn} \lor A \in
437 %%\subsubsection{For $R \in \py$:}