1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
24 \newif\ifhidehack\hidehackfalse
25 \DeclareRobustCommand\hidefromedef[2]{%
26 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\land}{\wedge}
50 \renewcommand{\lor}{\vee}
52 \newcommand{\pancs}{{\mathcal A}}
53 \newcommand{\pends}{{\mathcal E}}
55 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
56 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58 \newcommand{\merge}{{\mathcal M}}
59 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
60 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62 \newcommand{\patch}{{\mathcal P}}
63 \newcommand{\base}{{\mathcal B}}
65 \newcommand{\patchof}[1]{\patch ( #1 ) }
66 \newcommand{\baseof}[1]{\base ( #1 ) }
68 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
69 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
71 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
72 \newcommand{\bigforall}{%
74 {\hbox{\huge$\forall$}}%
75 {\hbox{\Large$\forall$}}%
76 {\hbox{\normalsize$\forall$}}%
77 {\hbox{\scriptsize$\forall$}}}%
80 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
81 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83 \newcommand{\qed}{\square}
84 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
86 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
87 \newcommand{\gathnext}{\\ \tag*{}}
90 \newcommand{\false}{f}
98 \desclabelstyle{\nextlinelabel}
100 \item[ $ C \hasparents \set X $ ]
101 The parents of commit $C$ are exactly the set
105 $C$ is a descendant of $D$ in the git commit
106 graph. This is a partial order, namely the transitive closure of
107 $ D \in \set X $ where $ C \hasparents \set X $.
109 \item[ $ C \has D $ ]
110 Informally, the tree at commit $C$ contains the change
111 made in commit $D$. Does not take account of deliberate reversions by
112 the user or reversion, rebasing or rewinding in
113 non-Topbloke-controlled branches. For merges and Topbloke-generated
114 anticommits or re-commits, the ``change made'' is only to be thought
115 of as any conflict resolution. This is not a partial order because it
118 \item[ $ \p, \py, \pn $ ]
119 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
120 are respectively the base and tip git branches. $\p$ may be used
121 where the context requires a set, in which case the statement
122 is to be taken as applying to both $\py$ and $\pn$.
123 All these sets are distinct. Hence:
125 \item[ $ \patchof{ C } $ ]
126 Either $\p$ s.t. $ C \in \p $, or $\bot$.
127 A function from commits to patches' sets $\p$.
129 \item[ $ \pancsof{C}{\set P} $ ]
130 $ \{ A \; | \; A \le C \land A \in \set P \} $
131 i.e. all the ancestors of $C$
132 which are in $\set P$.
134 \item[ $ \pendsof{C}{\set P} $ ]
135 $ \{ E \; | \; E \in \pancsof{C}{\set P}
136 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
137 E \neq A \land E \le A \} $
138 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
140 \item[ $ \baseof{C} $ ]
141 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
142 A partial function from commits to commits.
143 See Unique Base, below.
145 \item[ $ C \haspatch \p $ ]
146 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
147 ~ Informally, $C$ has the contents of $\p$.
149 \item[ $ C \nothaspatch \p $ ]
150 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
151 ~ Informally, $C$ has none of the contents of $\p$.
153 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
154 patch is applied to a non-Topbloke branch and then bubbles back to
155 the Topbloke patch itself, we hope that git's merge algorithm will
156 DTRT or that the user will no longer care about the Topbloke patch.
158 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
159 The contents of a git merge result:
161 $\displaystyle D \isin C \equiv
163 (D \isin L \land D \isin R) \lor D = C : & \true \\
164 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
165 \text{otherwise} : & D \not\isin M
173 We maintain these each time we construct a new commit. \\
175 C \has D \implies C \ge D
177 \[\eqn{Unique Base:}{
178 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
180 \[\eqn{Tip Contents:}{
181 \bigforall_{C \in \py} D \isin C \equiv
182 { D \isin \baseof{C} \lor \atop
183 (D \in \py \land D \le C) }
185 \[\eqn{Base Acyclic:}{
186 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
189 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
191 \[\eqn{Foreign Inclusion:}{
192 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
195 \section{Some lemmas}
197 \[ \eqn{Exclusive Tip Contents:}{
198 \bigforall_{C \in \py}
199 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
202 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
205 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
206 So by Base Acyclic $D \isin B \implies D \notin \py$.
209 \bigforall_{C \in \py} D \isin C \equiv
211 D \in \py : & D \le C \\
212 D \not\in \py : & D \isin \baseof{C}
216 \[ \eqn{Tip Self Inpatch:}{
217 \bigforall_{C \in \py} C \haspatch \p
219 Ie, tip commits contain their own patch.
222 Apply Exclusive Tip Contents to some $D \in \py$:
223 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
224 D \isin C \equiv D \le C $
227 \[ \eqn{Exact Ancestors:}{
228 \bigforall_{ C \hasparents \set{R} }
230 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
234 \[ \eqn{Transitive Ancestors:}{
235 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
236 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
240 The implication from right to left is trivial because
241 $ \pends() \subset \pancs() $.
242 For the implication from left to right:
243 by the definition of $\mathcal E$,
244 for every such $A$, either $A \in \pends()$ which implies
245 $A \le M$ by the LHS directly,
246 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
247 in which case we repeat for $A'$. Since there are finitely many
248 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
249 by the LHS. And $A \le A''$.
251 \[ \eqn{Calculation Of Ends:}{
252 \bigforall_{C \hasparents \set A}
253 \pendsof{C}{\set P} =
255 \Bigl[ \Largeexists_{A \in \set A}
256 E \in \pendsof{A}{\set P} \Bigr] \land
257 \Bigl[ \Largenexists_{B \in \set A}
258 E \neq B \land E \le B \Bigr]
263 \subsection{No Replay for Merge Results}
265 If we are constructing $C$, given
273 No Replay is preserved. {\it Proof:}
275 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
277 \subsubsection{For $D \isin L \land D \isin R$:}
278 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
280 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
283 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
284 \land D \not\isin M$:}
285 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
288 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
294 \section{Commit annotation}
296 We annotate each Topbloke commit $C$ with:
300 \baseof{C}, \text{ if } C \in \py
303 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
305 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
308 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
309 make it wrong to make plain commits with git because the recorded $\pends$
310 would have to be updated. The annotation is not needed because
311 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
313 \section{Simple commit}
315 A simple single-parent forward commit $C$ as made by git-commit.
317 \tag*{} C \hasparents \{ A \} \\
318 \tag*{} \patchof{C} = \patchof{A} \\
319 \tag*{} D \isin C \equiv D \isin A \lor D = C
322 \subsection{No Replay}
325 \subsection{Unique Base}
326 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
328 \subsection{Tip Contents}
329 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
330 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
331 Substitute into the contents of $C$:
332 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
334 Since $D = C \implies D \in \py$,
335 and substituting in $\baseof{C}$, this gives:
336 \[ D \isin C \equiv D \isin \baseof{C} \lor
337 (D \in \py \land D \le A) \lor
338 (D = C \land D \in \py) \]
339 \[ \equiv D \isin \baseof{C} \lor
340 [ D \in \py \land ( D \le A \lor D = C ) ] \]
341 So by Exact Ancestors:
342 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
346 \subsection{Base Acyclic}
348 Need to consider only $A, C \in \pn$.
350 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
352 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
353 $A$, $D \isin C \implies D \not\in \py$. $\qed$
355 \subsection{Coherence and patch inclusion}
357 Need to consider $D \in \py$
359 \subsubsection{For $A \haspatch P, D = C$:}
365 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
367 \subsubsection{For $A \haspatch P, D \neq C$:}
368 Ancestors: $ D \le C \equiv D \le A $.
370 Contents: $ D \isin C \equiv D \isin A \lor f $
371 so $ D \isin C \equiv D \isin A $.
374 \[ A \haspatch P \implies C \haspatch P \]
376 \subsubsection{For $A \nothaspatch P$:}
378 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
381 Now by contents of $A$, $D \notin A$, so $D \notin C$.
384 \[ A \nothaspatch P \implies C \nothaspatch P \]
387 \subsection{Foreign inclusion:}
389 If $D = C$, trivial. For $D \neq C$:
390 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
394 Given $L, R^+, R^-$ where
395 $R^+ \in \pry, R^- = \baseof{R^+}$.
396 Construct $C$ which has $\pr$ removed.
397 Used for removing a branch dependency.
399 C \hasparents \{ L \}
401 \patchof{C} = \patchof{L}
403 \mergeof{C}{L}{R^+}{R^-}
406 \subsection{Conditions}
408 \[ \eqn{ Unique Tip }{
409 \pendsof{L}{\pry} = \{ R^+ \}
411 \[ \eqn{ Currently Included }{
418 \subsection{No Replay}
420 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
421 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
422 Merge Results applies. $\qed$
424 \subsection{Desired Contents}
426 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
429 \subsubsection{For $D = C$:}
431 Trivially $D \isin C$. OK.
433 \subsubsection{For $D \neq C, D \not\le L$:}
435 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
436 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
438 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
440 By Currently Included, $D \isin L$.
442 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
443 by Unique Tip, $D \le R^+ \equiv D \le L$.
446 By Base Acyclic, $D \not\isin R^-$.
448 Apply $\merge$: $D \not\isin C$. OK.
450 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
452 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
454 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
458 \subsection{Unique Base}
460 Need to consider only $C \in \py$, ie $L \in \py$.
466 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
468 C \hasparents \{ L, R \}
470 \patchof{C} = \patchof{L}
475 \subsection{Conditions}
477 \[ \eqn{ Tip Merge }{
480 R \in \py : & \baseof{R} \ge \baseof{L}
481 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
482 R \in \pn : & R \ge \baseof{L}
483 \land M = \baseof{L} \\
484 \text{otherwise} : & \false
488 \subsection{No Replay}
490 See No Replay for Merge Results.
492 \subsection{Unique Base}
494 Need to consider only $C \in \py$, ie $L \in \py$,
495 and calculate $\pendsof{C}{\pn}$. So we will consider some
496 putative ancestor $A \in \pn$ and see whether $A \le C$.
498 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
499 But $C \in py$ and $A \in \pn$ so $A \neq C$.
500 Thus $A \le C \equiv A \le L \lor A \le R$.
502 By Unique Base of L and Transitive Ancestors,
503 $A \le L \equiv A \le \baseof{L}$.
505 \subsubsection{For $R \in \py$:}
507 By Unique Base of $R$ and Transitive Ancestors,
508 $A \le R \equiv A \le \baseof{R}$.
510 But by Tip Merge condition on $\baseof{R}$,
511 $A \le \baseof{L} \implies A \le \baseof{R}$, so
512 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
513 Thus $A \le C \equiv A \le \baseof{R}$.
514 That is, $\baseof{C} = \baseof{R}$.
516 \subsubsection{For $R \in \pn$:}
518 By Tip Merge condition on $R$,
519 $A \le \baseof{L} \implies A \le R$, so
520 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
521 Thus $A \le C \equiv A \le R$.
522 That is, $\baseof{C} = R$.