1 \documentclass[a4paper,leqno]{strayman}
2 \let\numberwithin=\notdef
10 \renewcommand{\ge}{\geqslant}
11 \renewcommand{\le}{\leqslant}
13 \newcommand{\has}{\sqsupseteq}
14 \newcommand{\isin}{\sqsubseteq}
16 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
17 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
18 \newcommand{\haspatch}{\sqSupset}
19 \newcommand{\patchisin}{\sqSubset}
21 \newcommand{\set}[1]{\mathbb #1}
22 \newcommand{\pa}[1]{\varmathbb #1}
23 \newcommand{\pay}[1]{\pa{#1}^+}
24 \newcommand{\pan}[1]{\pa{#1}^-}
26 \newcommand{\p}{\pa{P}}
27 \newcommand{\py}{\pay{P}}
28 \newcommand{\pn}{\pan{P}}
30 %\newcommand{\hasparents}{\underaccent{1}{>}}
31 %\newcommand{\hasparents}{{%
32 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
33 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
34 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
36 \renewcommand{\implies}{\Rightarrow}
37 \renewcommand{\equiv}{\Leftrightarrow}
38 \renewcommand{\land}{\wedge}
39 \renewcommand{\lor}{\vee}
41 \newcommand{\pancs}{{\mathcal A}}
42 \newcommand{\pends}{{\mathcal E}}
44 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
45 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
47 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
48 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
50 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
51 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
53 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
54 \newcommand{\bigforall}{%
56 {\hbox{\huge$\forall$}}%
57 {\hbox{\Large$\forall$}}%
58 {\hbox{\normalsize$\forall$}}%
59 {\hbox{\scriptsize$\forall$}}}%
62 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
63 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
65 \newcommand{\qed}{\square}
66 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
68 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
69 \newcommand{\gathnext}{\\ \tag*{}}
72 \newcommand{\false}{f}
80 \desclabelstyle{\nextlinelabel}
82 \item[ $ C \hasparents \set X $ ]
83 The parents of commit $C$ are exactly the set
87 $C$ is a descendant of $D$ in the git commit
88 graph. This is a partial order, namely the transitive closure of
89 $ D \in \set X $ where $ C \hasparents \set X $.
92 Informally, the tree at commit $C$ contains the change
93 made in commit $D$. Does not take account of deliberate reversions by
94 the user or reversion, rebasing or rewinding in
95 non-Topbloke-controlled branches. For merges and Topbloke-generated
96 anticommits or re-commits, the ``change made'' is only to be thought
97 of as any conflict resolution. This is not a partial order because it
100 \item[ $ \p, \py, \pn $ ]
101 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
102 are respectively the base and tip git branches. $\p$ may be used
103 where the context requires a set, in which case the statement
104 is to be taken as applying to both $\py$ and $\pn$.
105 All these sets are distinct. Hence:
107 \item[ $ \patchof{ C } $ ]
108 Either $\p$ s.t. $ C \in \p $, or $\bot$.
109 A function from commits to patches' sets $\p$.
111 \item[ $ \pancsof{C}{\set P} $ ]
112 $ \{ A \; | \; A \le C \land A \in \set P \} $
113 i.e. all the ancestors of $C$
114 which are in $\set P$.
116 \item[ $ \pendsof{C}{\set P} $ ]
117 $ \{ E \; | \; E \in \pancsof{C}{\set P}
118 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
119 E \neq A \land E \le A \} $
120 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
122 \item[ $ \baseof{C} $ ]
123 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
124 A partial function from commits to commits.
125 See Unique Base, below.
127 \item[ $ C \haspatch \p $ ]
128 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
129 ~ Informally, $C$ has the contents of $\p$.
131 \item[ $ C \nothaspatch \p $ ]
132 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
133 ~ Informally, $C$ has none of the contents of $\p$.
135 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
136 patch is applied to a non-Topbloke branch and then bubbles back to
137 the Topbloke patch itself, we hope that git's merge algorithm will
138 DTRT or that the user will no longer care about the Topbloke patch.
144 We maintain these each time we construct a new commit. \\
146 C \has D \implies C \ge D
148 \[\eqn{Unique Base:}{
149 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
151 \[\eqn{Tip Contents:}{
152 \bigforall_{C \in \py} D \isin C \equiv
153 { D \isin \baseof{C} \lor \atop
154 (D \in \py \land D \le C) }
156 \[\eqn{Base Acyclic:}{
157 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
160 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
162 \[\eqn{Foreign Inclusion:}{
163 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
166 \section{Some lemmas}
168 \[ \eqn{Exclusive Tip Contents:}{
169 \bigforall_{C \in \py}
170 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
173 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
176 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
177 So by Base Acyclic $D \isin B \implies D \notin \py$.
180 \bigforall_{C \in \py} D \isin C \equiv
182 D \in \py : & D \le C \\
183 D \not\in \py : & D \isin \baseof{C}
187 \[ \eqn{Tip Self Inpatch:}{
188 \bigforall_{C \in \py} C \haspatch \p
190 Ie, tip commits contain their own patch.
193 Apply Exclusive Tip Contents to some $D \in \py$:
194 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
195 D \isin C \equiv D \le C $
198 \[ \eqn{Exact Ancestors:}{
199 \bigforall_{ C \hasparents \set{R} }
201 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
205 \[ \eqn{Transitive Ancestors:}{
206 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
207 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
211 The implication from right to left is trivial because
212 $ \pends() \subset \pancs() $.
213 For the implication from left to right:
214 by the definition of $\mathcal E$,
215 for every such $A$, either $A \in \pends()$ which implies
216 $A \le M$ by the LHS directly,
217 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
218 in which case we repeat for $A'$. Since there are finitely many
219 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
220 by the LHS. And $A \le A''$.
223 \section{Commit annotation}
225 We annotate each Topbloke commit $C$ with:
229 \baseof{C}, \text{ if } C \in \py
232 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
234 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
237 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
238 make it wrong to make plain commits with git because the recorded $\pends$
239 would have to be updated. The annotation is not needed because
240 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
242 \section{Simple commit}
244 A simple single-parent forward commit $C$ as made by git-commit.
246 \tag*{} C \hasparents \{ A \} \\
247 \tag*{} \patchof{C} = \patchof{A} \\
248 \tag*{} D \isin C \equiv D \isin A \lor D = C
251 \subsection{No Replay}
254 \subsection{Unique Base}
255 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
257 \subsection{Tip Contents}
258 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
259 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
260 Substitute into the contents of $C$:
261 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
263 Since $D = C \implies D \in \py$,
264 and substituting in $\baseof{C}$, this gives:
265 \[ D \isin C \equiv D \isin \baseof{C} \lor
266 (D \in \py \land D \le A) \lor
267 (D = C \land D \in \py) \]
268 \[ \equiv D \isin \baseof{C} \lor
269 [ D \in \py \land ( D \le A \lor D = C ) ] \]
270 So by Exact Ancestors:
271 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
275 \subsection{Base Acyclic}
277 Need to consider only $A, C \in \pn$.
279 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
281 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
282 $A$, $D \isin C \implies D \not\in \py$. $\qed$
284 \subsection{Coherence and patch inclusion}
286 Need to consider $D \in \py$
288 \subsubsection{For $A \haspatch P, D = C$:}
294 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
296 \subsubsection{For $A \haspatch P, D \neq C$:}
297 Ancestors: $ D \le C \equiv D \le A $.
299 Contents: $ D \isin C \equiv D \isin A \lor f $
300 so $ D \isin C \equiv D \isin A $.
303 \[ A \haspatch P \implies C \haspatch P \]
305 \subsubsection{For $A \nothaspatch P$:}
307 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
310 Now by contents of $A$, $D \notin A$, so $D \notin C$.
313 \[ A \nothaspatch P \implies C \nothaspatch P \]
316 \subsection{Foreign inclusion:}
318 If $D = C$, trivial. For $D \neq C$:
319 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
323 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
325 C \hasparents \{ L, R \}
327 \patchof{C} = \patchof{L}
331 (D \isin L \land D \isin R) \lor D = C : & \true \\
332 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
333 \text{otherwise} : & D \not\isin M
337 \subsection{Conditions}
339 \[ \eqn{ Tip Merge }{
342 R \in \py : & \baseof{R} \ge \baseof{L}
343 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
344 R \in \pn : & R \ge \baseof{L}
345 \land M = \baseof{L} \\
346 \text{otherwise} : & \false
350 \subsection{No Replay}
352 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
354 \subsubsection{For $D \isin L \land D \isin R$:}
355 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
357 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
360 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
363 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
364 \land D \not\isin M$:}
365 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
368 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
370 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le