notation.tex

   1 \stdsection{Notation}
   2
   3 Throughout, any free variables are implicitly universally quantified
   4 at the outermost level.
   5
   6 \begin{basedescript}{
   7 \desclabelwidth{5em}
   8 \desclabelstyle{\nextlinelabel}
   9 }
  10 \item[ $ C \hasparent D $ ]
  11 Commit $C$ has commit $D$ as (one of) its parents.
  12
  13 \item[ $ C \hasparents \set X $ ]
  14 The parents of commit $C$ are exactly the set
  15 $\set X$.
  16
  17 \item[ $ C \ge D $ ]
  18 $C$ is a descendant of $D$ in the git commit
  19 graph.  This is a partial order, namely the transitive closure of
  20 $ \hasparent $.
  21
  22 \item[ $ C \has D $ ]
  23 Informally, the tree at commit $C$ contains the change
  24 made in commit $D$.  Does not take account of deliberate reversions by
  25 the user or reversion, rebasing or rewinding in
  26 non-Topbloke-controlled branches.  For merges and Topbloke-generated
  27 anticommits or re-commits, the ``change made'' is only to be thought
  28 of as any conflict resolution.  This is not a partial order because it
  29 is not transitive.
  30
  31 \item[ $ \p, \py, \pn $ ]
  32 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
  33 are respectively the base and tip git branches.  $\p$ may be used
  34 where the context requires a set, in which case the statement
  35 is to be taken as applying to both $\py$ and $\pn$.
  36 All of these sets will be disjoint by construction
  37 (see Invariants, below).
  38
  39 \item[ $\foreign$ ]
  40 The set of all commits which are not part of a Topbloke branch.  We
  41 call these foreign commits.  Hence:
  42
  43 \item[ $ \patchof{ C } $ ]
  44 Either $\p$ s.t. $ C \in \p $, or $\foreign$.
  45 A function from commits to patches' sets $\p$.
  46
  47 \item[ $\set A$, $\set P$, $\ldots$ ]
  48 Arbitrary sets of commits.  Maybe $\set P = \p$ i.e.\ some $\py$ or $\pn$, but
  49 maybe not.
  50
  51 \item[ $ \pancsof{C}{\set P} $ ]
  52 $ \{ A \; | \; A \le C \land A \in \set P \} $
  53 i.e. all the ancestors of $C$
  54 which are in $\set P$.
  55
  56 \item[ $ \pendsof{C}{\set P} $ ]
  57 $ \{ E \; | \; E \in \pancsof{C}{\set P}
  58   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
  59   E \neq A \land E \le A \} $
  60 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
  61
  62 \item[ $ \baseof{C} $ ]
  63 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
  64 A partial function from commits to commits.
  65 See Unique Base, below.
  66
  67 \item[ $ C \nothaspatch \p $ ]
  68 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
  69 ~ Informally, $C$ has none of the contents of $\p$.
  70
  71 \item[ $ C \zhaspatch \p $ ]
  72 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
  73 ~ Informally, $C$ has all the reachable contents of $\p$.
  74
  75 \item[ $ C \haspatch \p $ ]
  76 $\displaystyle C \zhaspatch \p \land \exists_{F \in \py} F \le C $.
  77 ~ Informally, $C$ nontrivially has all the reachable contents of $\p$.
  78
  79 Note that $\zhaspatch$ and $\nothaspatch$ are neither
  80 mutually exclusive nor exhaustive.
  81 $\haspatch$ and $\nothaspatch$ are mutually exclusive but not
  82 necessarily exhaustive.
  83
  84 Commits on Non-Topbloke branches are $\nothaspatch \p$ for all $\p$.  This
  85 includes commits on plain git branches made by applying a Topbloke
  86 patch.  If a Topbloke
  87 patch is applied to a non-Topbloke branch and then bubbles back to
  88 the relevant Topbloke branches, we hope that
  89 if the user still cares about the Topbloke patch,
  90 git's merge algorithm will DTRT when trying to re-apply the changes.
  91
  92 \item[ $\displaystyle \stmtmergeof{\stmt L}{\stmt M}{\stmt R} $ ]
  93 The proper results of a merge.  Formally,
  94 where $\stmt L$, $\stmt M$ and $\stmt R$ are statements:
  95 $$
  96   \stmtmergeof{\stmt L}{\stmt M}{\stmt R}
  97     \equiv
  98   \begin{cases}
  99          (\stmt L \land \stmt R)      : & \true \\
 100     (\neg \stmt L \land \neg \stmt R) : & \false \\
 101     \text{otherwise} : & \neg \stmt M
 102   \end{cases}
 103 $$
 104
 105 May also be used with sets:
 106 $$
 107   \setmergeof{\set L}{\set M}{\set R}
 108      =
 109   \left\{
 110     \;
 111     D \; \middle| \;
 112       \setmergeof{ D \in \set L }{ D \in \set M }{ D \in \set R }
 113     \;
 114   \right\}
 115 $$
 116
 117 \item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
 118 With $C$, $L$, $M$ and $R$ being commits, a convenience notation.
 119 $C$ has exactly the contents of a git merge result:
 120
 121 $\displaystyle D \isin C \equiv
 122   \begin{cases}
 123     D = C : & \true \\
 124     D \neq C : & \stmtmergeof{ D \isin L }{ D \isin M }{ D \isin R }
 125   \end{cases}
 126 $
 127
 128 We will refer to this as \bf\commitmergename.
 129
 130 \end{basedescript}