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$}}}%
63 \newcommand{\qed}{\square}
64 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
66 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
67 \newcommand{\gathnext}{\\ \tag*{}}
75 \desclabelstyle{\nextlinelabel}
77 \item[ $ C \hasparents \set X $ ]
78 The parents of commit $C$ are exactly the set
82 $C$ is a descendant of $D$ in the git commit
83 graph. This is a partial order, namely the transitive closure of
84 $ D \in \set X $ where $ C \hasparents \set X $.
87 Informally, the tree at commit $C$ contains the change
88 made in commit $D$. Does not take account of deliberate reversions by
89 the user or reversion, rebasing or rewinding in
90 non-Topbloke-controlled branches. For merges and Topbloke-generated
91 anticommits or re-commits, the ``change made'' is only to be thought
92 of as any conflict resolution. This is not a partial order because it
95 \item[ $ \p, \py, \pn $ ]
96 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
97 are respectively the base and tip git branches. $\p$ may be used
98 where the context requires a set, in which case the statement
99 is to be taken as applying to both $\py$ and $\pn$.
100 All these sets are distinct. Hence:
102 \item[ $ \patchof{ C } $ ]
103 Either $\p$ s.t. $ C \in \p $, or $\bot$.
104 A function from commits to patches' sets $\p$.
106 \item[ $ \pancsof{C}{\set P} $ ]
107 $ \{ A \; | \; A \le C \land A \in \set P \} $
108 i.e. all the ancestors of $C$
109 which are in $\set P$.
111 \item[ $ \pendsof{C}{\set P} $ ]
112 $ \{ E \; | \; E \in \pancsof{C}{\set P}
113 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
114 A \neq E \land E \le A \} $
115 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
117 \item[ $ \baseof{C} $ ]
118 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
119 A partial function from commits to commits.
120 See Unique Base, below.
122 \item[ $ C \haspatch \p $ ]
123 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
124 ~ Informally, $C$ has the contents of $\p$.
126 \item[ $ C \nothaspatch \p $ ]
127 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
128 ~ Informally, $C$ has none of the contents of $\p$.
130 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
131 patch is applied to a non-Topbloke branch and then bubbles back to
132 the Topbloke patch itself, we hope that git's merge algorithm will
133 DTRT or that the user will no longer care about the Topbloke patch.
139 We maintain these each time we construct a new commit. \\
141 C \has D \implies C \ge D
143 \[\eqn{Unique Base:}{
144 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
146 \[\eqn{Tip Contents:}{
147 \bigforall_{C \in \py} D \isin C \equiv
148 { D \isin \baseof{C} \lor \atop
149 (D \in \py \land D \le C) }
151 \[\eqn{Base Acyclic:}{
152 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
155 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
157 \[\eqn{Foreign Inclusion:}{
158 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
161 \section{Some lemmas}
163 \[ \eqn{Exclusive Tip Contents:}{
164 \bigforall_{C \in \py}
165 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
168 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
171 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
172 So by Base Acyclic $D \isin B \implies D \notin \py$.
175 \bigforall_{C \in \py} D \isin C \equiv
177 D \in \py : & D \le C \\
178 D \not\in \py : & D \isin \baseof{C}
182 \[ \eqn{Tip Self Inpatch:}{
183 \bigforall_{C \in \py} C \haspatch \p
185 Ie, tip commits contain their own patch.
188 Apply Exclusive Tip Contents to some $D \in \py$:
189 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
190 D \isin C \equiv D \le C $
193 \[ \eqn{Exact Ancestors:}{
194 \bigforall_{ C \hasparents \set{R} }
196 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
200 \[ \eqn{Transitive Ancestors:}{
201 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
202 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
206 The implication from right to left is trivial because
207 $ \pends() \subset \pancs() $.
208 For the implication from left to right:
209 by the definition of $\mathcal E$,
210 for every such $A$, either $A \in \pends()$ which implies
211 $A \le M$ by the LHS directly,
212 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
213 in which case we repeat for $A'$. Since there are finitely many
214 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
215 by the LHS. And $A \le A''$.
218 \section{Commit annotation}
220 We annotate each Topbloke commit $C$ with:
224 \baseof{C}, \text{ if } C \in \py
227 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
229 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
232 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
233 make it wrong to make plain commits with git because the recorded $\pends$
234 would have to be updated. The annotation is not needed because
235 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
237 \section{Simple commit}
239 A simple single-parent forward commit $C$ as made by git-commit.
241 \tag*{} C \hasparents \{ A \} \\
242 \tag*{} \patchof{C} = \patchof{A} \\
243 \tag*{} D \isin C \equiv D \isin A \lor D = C
246 \subsection{No Replay}
249 \subsection{Unique Base}
250 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
252 \subsection{Tip Contents}
253 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
254 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
255 Substitute into the contents of $C$:
256 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
258 Since $D = C \implies D \in \py$,
259 and substituting in $\baseof{C}$, this gives:
260 \[ D \isin C \equiv D \isin \baseof{C} \lor
261 (D \in \py \land D \le A) \lor
262 (D = C \land D \in \py) \]
263 \[ \equiv D \isin \baseof{C} \lor
264 [ D \in \py \land ( D \le A \lor D = C ) ] \]
265 So by Exact Ancestors:
266 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
270 \subsection{Base Acyclic}
272 Need to consider only $A, C \in \pn$.
274 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
276 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
277 $A$, $D \isin C \implies D \not\in \py$. $\qed$
279 \subsection{Coherence and patch inclusion}
281 Need to consider $D \in \py$
283 \subsubsection{For $A \haspatch P, D = C$:}
289 $ D \isin C \equiv \ldots \lor t \text{ so } D \haspatch C $.
291 \subsubsection{For $A \haspatch P, D \neq C$:}
292 Ancestors: $ D \le C \equiv D \le A $.
294 Contents: $ D \isin C \equiv D \isin A \lor f $
295 so $ D \isin C \equiv D \isin A $.
298 \[ A \haspatch P \implies C \haspatch P \]
300 \subsubsection{For $A \nothaspatch P$:}
302 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
305 Now by contents of $A$, $D \notin A$, so $D \notin C$.
308 \[ A \nothaspatch P \implies C \nothaspatch P \]
311 \subsection{Foreign inclusion:}
313 If $D = C$, trivial. For $D \neq C$:
314 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
316 \section{Test more symbols}
320 $ C \nothaspatch \p $
324 $ \p \notpatchisin C $
326 $ \{ B \} \areparents C $