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{\pr}{\pa{R}}
36 \newcommand{\pry}{\pay{R}}
37 \newcommand{\prn}{\pan{R}}
39 %\newcommand{\hasparents}{\underaccent{1}{>}}
40 %\newcommand{\hasparents}{{%
41 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
42 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
43 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
45 \renewcommand{\implies}{\Rightarrow}
46 \renewcommand{\equiv}{\Leftrightarrow}
47 \renewcommand{\land}{\wedge}
48 \renewcommand{\lor}{\vee}
50 \newcommand{\pancs}{{\mathcal A}}
51 \newcommand{\pends}{{\mathcal E}}
53 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
54 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
56 \newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
57 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
59 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
60 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
62 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
63 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
65 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
66 \newcommand{\bigforall}{%
68 {\hbox{\huge$\forall$}}%
69 {\hbox{\Large$\forall$}}%
70 {\hbox{\normalsize$\forall$}}%
71 {\hbox{\scriptsize$\forall$}}}%
74 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
75 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
77 \newcommand{\qed}{\square}
78 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
80 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
81 \newcommand{\gathnext}{\\ \tag*{}}
84 \newcommand{\false}{f}
92 \desclabelstyle{\nextlinelabel}
94 \item[ $ C \hasparents \set X $ ]
95 The parents of commit $C$ are exactly the set
99 $C$ is a descendant of $D$ in the git commit
100 graph. This is a partial order, namely the transitive closure of
101 $ D \in \set X $ where $ C \hasparents \set X $.
103 \item[ $ C \has D $ ]
104 Informally, the tree at commit $C$ contains the change
105 made in commit $D$. Does not take account of deliberate reversions by
106 the user or reversion, rebasing or rewinding in
107 non-Topbloke-controlled branches. For merges and Topbloke-generated
108 anticommits or re-commits, the ``change made'' is only to be thought
109 of as any conflict resolution. This is not a partial order because it
112 \item[ $ \p, \py, \pn $ ]
113 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
114 are respectively the base and tip git branches. $\p$ may be used
115 where the context requires a set, in which case the statement
116 is to be taken as applying to both $\py$ and $\pn$.
117 All these sets are distinct. Hence:
119 \item[ $ \patchof{ C } $ ]
120 Either $\p$ s.t. $ C \in \p $, or $\bot$.
121 A function from commits to patches' sets $\p$.
123 \item[ $ \pancsof{C}{\set P} $ ]
124 $ \{ A \; | \; A \le C \land A \in \set P \} $
125 i.e. all the ancestors of $C$
126 which are in $\set P$.
128 \item[ $ \pendsof{C}{\set P} $ ]
129 $ \{ E \; | \; E \in \pancsof{C}{\set P}
130 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
131 E \neq A \land E \le A \} $
132 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
134 \item[ $ \baseof{C} $ ]
135 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
136 A partial function from commits to commits.
137 See Unique Base, below.
139 \item[ $ C \haspatch \p $ ]
140 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
141 ~ Informally, $C$ has the contents of $\p$.
143 \item[ $ C \nothaspatch \p $ ]
144 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
145 ~ Informally, $C$ has none of the contents of $\p$.
147 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
148 patch is applied to a non-Topbloke branch and then bubbles back to
149 the Topbloke patch itself, we hope that git's merge algorithm will
150 DTRT or that the user will no longer care about the Topbloke patch.
152 \item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
153 The contents of a git merge result:
155 $\displaystyle D \isin C \equiv
157 (D \isin L \land D \isin R) \lor D = C : & \true \\
158 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
159 \text{otherwise} : & D \not\isin M
167 We maintain these each time we construct a new commit. \\
169 C \has D \implies C \ge D
171 \[\eqn{Unique Base:}{
172 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
174 \[\eqn{Tip Contents:}{
175 \bigforall_{C \in \py} D \isin C \equiv
176 { D \isin \baseof{C} \lor \atop
177 (D \in \py \land D \le C) }
179 \[\eqn{Base Acyclic:}{
180 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
183 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
185 \[\eqn{Foreign Inclusion:}{
186 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
189 \section{Some lemmas}
191 \[ \eqn{Exclusive Tip Contents:}{
192 \bigforall_{C \in \py}
193 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
196 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
199 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
200 So by Base Acyclic $D \isin B \implies D \notin \py$.
203 \bigforall_{C \in \py} D \isin C \equiv
205 D \in \py : & D \le C \\
206 D \not\in \py : & D \isin \baseof{C}
210 \[ \eqn{Tip Self Inpatch:}{
211 \bigforall_{C \in \py} C \haspatch \p
213 Ie, tip commits contain their own patch.
216 Apply Exclusive Tip Contents to some $D \in \py$:
217 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
218 D \isin C \equiv D \le C $
221 \[ \eqn{Exact Ancestors:}{
222 \bigforall_{ C \hasparents \set{R} }
224 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
228 \[ \eqn{Transitive Ancestors:}{
229 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
230 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
234 The implication from right to left is trivial because
235 $ \pends() \subset \pancs() $.
236 For the implication from left to right:
237 by the definition of $\mathcal E$,
238 for every such $A$, either $A \in \pends()$ which implies
239 $A \le M$ by the LHS directly,
240 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
241 in which case we repeat for $A'$. Since there are finitely many
242 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
243 by the LHS. And $A \le A''$.
245 \[ \eqn{Calculation Of Ends:}{
246 \bigforall_{C \hasparents \set A}
247 \pendsof{C}{\set P} =
249 \Bigl[ \Largeexists_{A \in \set A}
250 E \in \pendsof{A}{\set P} \Bigr] \land
251 \Bigl[ \Largenexists_{B \in \set A}
252 E \neq B \land E \le B \Bigr]
257 \subsection{No Replay for Merge Results}
259 If we are constructing $C$ such that $\merge{C}{L}{M}{R}$, No Replay
260 is preserved. {\it Proof:}
262 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
264 \subsubsection{For $D \isin L \land D \isin R$:}
265 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
267 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
270 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
273 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
274 \land D \not\isin M$:}
275 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
278 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
280 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
285 \section{Commit annotation}
287 We annotate each Topbloke commit $C$ with:
291 \baseof{C}, \text{ if } C \in \py
294 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
296 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
299 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
300 make it wrong to make plain commits with git because the recorded $\pends$
301 would have to be updated. The annotation is not needed because
302 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
304 \section{Simple commit}
306 A simple single-parent forward commit $C$ as made by git-commit.
308 \tag*{} C \hasparents \{ A \} \\
309 \tag*{} \patchof{C} = \patchof{A} \\
310 \tag*{} D \isin C \equiv D \isin A \lor D = C
313 \subsection{No Replay}
316 \subsection{Unique Base}
317 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
319 \subsection{Tip Contents}
320 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
321 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
322 Substitute into the contents of $C$:
323 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
325 Since $D = C \implies D \in \py$,
326 and substituting in $\baseof{C}$, this gives:
327 \[ D \isin C \equiv D \isin \baseof{C} \lor
328 (D \in \py \land D \le A) \lor
329 (D = C \land D \in \py) \]
330 \[ \equiv D \isin \baseof{C} \lor
331 [ D \in \py \land ( D \le A \lor D = C ) ] \]
332 So by Exact Ancestors:
333 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
337 \subsection{Base Acyclic}
339 Need to consider only $A, C \in \pn$.
341 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
343 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
344 $A$, $D \isin C \implies D \not\in \py$. $\qed$
346 \subsection{Coherence and patch inclusion}
348 Need to consider $D \in \py$
350 \subsubsection{For $A \haspatch P, D = C$:}
356 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
358 \subsubsection{For $A \haspatch P, D \neq C$:}
359 Ancestors: $ D \le C \equiv D \le A $.
361 Contents: $ D \isin C \equiv D \isin A \lor f $
362 so $ D \isin C \equiv D \isin A $.
365 \[ A \haspatch P \implies C \haspatch P \]
367 \subsubsection{For $A \nothaspatch P$:}
369 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
372 Now by contents of $A$, $D \notin A$, so $D \notin C$.
375 \[ A \nothaspatch P \implies C \nothaspatch P \]
378 \subsection{Foreign inclusion:}
380 If $D = C$, trivial. For $D \neq C$:
381 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
385 Given $L, R^+, R^-$ where
386 $\patchof{R^+} = \pry, \patchof{R^-} = \prn$.
387 Construct $C$ which has $\pr$ removed.
388 Used for removing a branch dependency.
390 C \hasparents \{ L \}
392 \patchof{C} = \patchof{L}
394 \merge{C}{L}{R^+}{R^-}
397 \subsection{Conditions}
399 \[ \eqn{ Unique Tip }{
400 \pendsof{L}{\pry} = \{ R^+ \}
402 \[ \eqn{ Correct Base }{
405 \[ \eqn{ Currently Included }{
411 xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
415 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
417 C \hasparents \{ L, R \}
419 \patchof{C} = \patchof{L}
424 \subsection{Conditions}
426 \[ \eqn{ Tip Merge }{
429 R \in \py : & \baseof{R} \ge \baseof{L}
430 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
431 R \in \pn : & R \ge \baseof{L}
432 \land M = \baseof{L} \\
433 \text{otherwise} : & \false
437 \subsection{Merge Results}
441 \subsection{Unique Base}
443 Need to consider only $C \in \py$, ie $L \in \py$,
444 and calculate $\pendsof{C}{\pn}$. So we will consider some
445 putative ancestor $A \in \pn$ and see whether $A \le C$.
447 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
448 But $C \in py$ and $A \in \pn$ so $A \neq C$.
449 Thus $A \le C \equiv A \le L \lor A \le R$.
451 By Unique Base of L and Transitive Ancestors,
452 $A \le L \equiv A \le \baseof{L}$.
454 \subsubsection{For $R \in \py$:}
456 By Unique Base of $R$ and Transitive Ancestors,
457 $A \le R \equiv A \le \baseof{R}$.
459 But by Tip Merge condition on $\baseof{R}$,
460 $A \le \baseof{L} \implies A \le \baseof{R}$, so
461 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
462 Thus $A \le C \equiv A \le \baseof{R}$.
463 That is, $\baseof{C} = \baseof{R}$.
465 \subsubsection{For $R \in \pn$:}
467 By Tip Merge condition on $R$,
468 $A \le \baseof{L} \implies A \le R$, so
469 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
470 Thus $A \le C \equiv A \le R$.
471 That is, $\baseof{C} = R$.