X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=notation.tex;h=b6b4a8cc814c01ffdb9076320796fbadfbc4bfbd;hp=b5e0e9d5549c85d32514ae3e2756e56c33f7b0b2;hb=35d8920c70badf3ea6556ad6cf53ea96ef6aec0c;hpb=6256831867d9cb3c135bbc73dad80db2a8677754 diff --git a/notation.tex b/notation.tex index b5e0e9d..b6b4a8c 100644 --- a/notation.tex +++ b/notation.tex @@ -7,6 +7,9 @@ at the outermost level. \desclabelwidth{5em} \desclabelstyle{\nextlinelabel} } +\item[ $ C \hasparent D $ ] +Commit $C$ has commit $D$ as (one of) its parents. + \item[ $ C \hasparents \set X $ ] The parents of commit $C$ are exactly the set $\set X$. @@ -14,7 +17,7 @@ $\set X$. \item[ $ C \ge D $ ] $C$ is a descendant of $D$ in the git commit graph. This is a partial order, namely the transitive closure of -$ D \in \set X $ where $ C \hasparents \set X $. +$ \hasparent $. \item[ $ C \has D $ ] Informally, the tree at commit $C$ contains the change @@ -31,20 +34,20 @@ are respectively the base and tip git branches. $\p$ may be used where the context requires a set, in which case the statement is to be taken as applying to both $\py$ and $\pn$. All of these sets will be disjoint by construction -(see Invariants, below). Hence: +(see Invariants, below). \item[ $\foreign$ ] The set of all commits which are not part of a Topbloke branch. We -call these foreign commits. - -\item[ $\set A$, $\set P$, $\ldots$ ] -Arbitrary sets of commits. Maybe $\set P = \p$ i.e.\ some $\py$ or $\pn$, but -maybe not. +call these foreign commits. Hence: \item[ $ \patchof{ C } $ ] Either $\p$ s.t. $ C \in \p $, or $\foreign$. A function from commits to patches' sets $\p$. +\item[ $\set A$, $\set P$, $\ldots$ ] +Arbitrary sets of commits. Maybe $\set P = \p$ i.e.\ some $\py$ or $\pn$, but +maybe not. + \item[ $ \pancsof{C}{\set P} $ ] $ \{ A \; | \; A \le C \land A \in \set P \} $ i.e. all the ancestors of $C$ @@ -86,41 +89,42 @@ the relevant Topbloke branches, we hope that if the user still cares about the Topbloke patch, git's merge algorithm will DTRT when trying to re-apply the changes. -\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ] +\item[ $\displaystyle \stmtmergeof{\stmt L}{\stmt M}{\stmt R} $ ] The proper results of a merge. Formally, -where $L$, $M$ and $R$ are statements: - +where $\stmt L$, $\stmt M$ and $\stmt R$ are statements: $$ - \stmtmergeof{L}{M}{R} + \stmtmergeof{\stmt L}{\stmt M}{\stmt R} \equiv \begin{cases} - (L \land R) : & \true \\ - (\neg L \land \neg R) : & \false \\ - \text{otherwise} : & \neg M + (\stmt L \land \stmt R) : & \true \\ + (\neg \stmt L \land \neg \stmt R) : & \false \\ + \text{otherwise} : & \neg \stmt M \end{cases} $$ -May also be used where $L$, $M$ and $R$ are sets, in which case +May also be used with sets: $$ - \setmergeof{L}{M}{R} + \setmergeof{\set L}{\set M}{\set R} = \left\{ \; D \; \middle| \; - \setmergeof{ D \in L }{ D \in M }{ D \in R } + \setmergeof{ D \in \set L }{ D \in \set M }{ D \in \set R } \; \right\} $$ \item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ] -The contents of a git merge result: +With $C$, $L$, $M$ and $R$ being commits, a convenience notation. +$C$ has exactly the contents of a git merge result: $\displaystyle D \isin C \equiv \begin{cases} - (D \isin L \land D \isin R) \lor D = C : & \true \\ - (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\ - \text{otherwise} : & D \not\isin M + D = C : & \true \\ + D \neq C : & \stmtmergeof{ D \isin L }{ D \isin M }{ D \isin R } \end{cases} $ +We will refer to this as \bf\commitmergename. + \end{basedescript}