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{\proof}[1]{{\it Proof.} #1 $\square$}
70 \desclabelstyle{\nextlinelabel}
72 \item[ $ C \hasparents \set X $ ]
73 The parents of commit $C$ are exactly the set
77 $C$ is a descendant of $D$ in the git commit
78 graph. This is a partial order, namely the transitive closure of
79 $ D \in \set X $ where $ C \hasparents \set X $.
82 Informally, the tree at commit $C$ contains the change
83 made in commit $D$. Does not take account of deliberate reversions by
84 the user or reversion, rebasing or rewinding in
85 non-Topbloke-controlled branches. For merges and Topbloke-generated
86 anticommits or re-commits, the ``change made'' is only to be thought
87 of as any conflict resolution. This is not a partial order because it
90 \item[ $ \p, \py, \pn $ ]
91 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
92 are respectively the base and tip git branches. $\p$ may be used
93 where the context requires a set, in which case the statement
94 is to be taken as applying to both $\py$ and $\pn$.
95 All these sets are distinct. Hence:
97 \item[ $ \patchof{ C } $ ]
98 Either $\p$ s.t. $ C \in \p $, or $\bot$.
99 A function from commits to patches' sets $\p$.
101 \item[ $ \pancsof{C}{\set P} $ ]
102 $ \{ A \; | \; A \le C \land A \in \set P \} $
103 i.e. all the ancestors of $C$
104 which are in $\set P$.
106 \item[ $ \pendsof{C}{\set P} $ ]
107 $ \{ E \; | \; E \in \pancsof{C}{\set P}
108 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
109 A \neq E \land E \le A \} $
110 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
112 \item[ $ \baseof{C} $ ]
113 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
114 A partial function from commits to commits.
115 See ``unique base'', below.
117 \item[ $ C \haspatch \p $ ]
118 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
119 ~ Informally, $C$ has the contents of $\p$.
121 \item[ $ C \nothaspatch \p $ ]
122 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
123 ~ Informally, $C$ has none of the contents of $\p$.
125 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
126 patch is applied to a non-Topbloke branch and then bubbles back to
127 the Topbloke patch itself, we hope that git's merge algorithm will
128 DTRT or that the user will no longer care about the Topbloke patch.
134 We maintain these each time we construct a new commit. \\
136 C \has D \implies C \ge D
138 \[\eqn{Unique Base:}{
139 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
141 \[\eqn{Tip Contents:}{
142 \bigforall_{C \in \py} D \isin C \equiv
143 { D \isin \baseof{C} \lor \atop
144 (D \in \py \land D \le C) }
146 \[\eqn{Base Acyclic:}{
147 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
150 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
152 \[\eqn{Foreign Inclusion:}{
153 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
156 \section{Some lemmas}
158 \[ \eqn{Exclusive Tip Contents:}{
159 \bigforall_{C \in \py}
160 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
163 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
166 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
167 So by Base Acyclic $D \isin B \implies D \notin \py$.
170 \bigforall_{C \in \py} D \isin C \equiv
172 D \in \py : & D \le C \\
173 D \not\in \py : & D \isin \baseof{C}
177 \[ \eqn{Tip Self Inpatch:}{
178 \bigforall_{C \in \py} C \haspatch \p
180 Ie, tip commits contain their own patch.
183 Apply Exclusive Tip Contents to some $D \in \py$:
184 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
185 D \isin C \equiv D \le C $
188 \[ \eqn{Exact Ancestors:}{
189 \bigforall_{ C \hasparents \set{R} }
191 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
195 \[ \eqn{Transitive Ancestors:}{
196 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
197 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
201 The implication from right to left is trivial because
202 $ \pends() \subset \pancs() $.
203 For the implication from left to right:
204 by the definition of $\mathcal E$,
205 for every such $A$, either $A \in \pends()$ which implies
206 $A \le M$ by the LHS directly,
207 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
208 in which case we repeat for $A'$. Since there are finitely many
209 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
210 by the LHS. And $A \le A''$.
213 \section{Commit annotation}
215 We annotate each Topbloke commit $C$ with:
217 \tag*{} \patchof{C} \\
218 \tag*{} \baseof{C}, \text{ if } C \in \py \\
219 \tag*{} \bigforall_{\pa{Q}}
220 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} \\
221 \tag*{} \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
224 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
225 make it wrong to make plain commits with git because the recorded $\pends$
226 would have to be updated. The annotation is not needed because
227 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
229 \section{Test more symbols}
233 $ C \nothaspatch \p $
237 $ \p \notpatchisin C $
239 $ \{ B \} \areparents C $