chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
strategy: reachable is going well
[topbloke-formulae.git]
/
notation.tex
diff --git
a/notation.tex
b/notation.tex
index b5e0e9d5549c85d32514ae3e2756e56c33f7b0b2..19cf243733e1a9ba8edce18d7d7a70a8e0fb1097 100644
(file)
--- a/
notation.tex
+++ b/
notation.tex
@@
-31,20
+31,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
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
\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[ $ \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$
\item[ $ \pancsof{C}{\set P} $ ]
$ \{ A \; | \; A \le C \land A \in \set P \} $
i.e. all the ancestors of $C$
@@
-89,7
+89,6
@@
git's merge algorithm will DTRT when trying to re-apply the changes.
\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ]
The proper results of a merge. Formally,
where $L$, $M$ and $R$ are statements:
\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ]
The proper results of a merge. Formally,
where $L$, $M$ and $R$ are statements:
-
$$
\stmtmergeof{L}{M}{R}
\equiv
$$
\stmtmergeof{L}{M}{R}
\equiv
@@
-113,14
+112,15
@@
$$
$$
\item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
$$
\item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
-
T
he contents of a git merge result:
+
$C$ has exactly t
he contents of a git merge result:
$\displaystyle D \isin C \equiv
\begin{cases}
$\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}
$
\end{cases}
$
+We will refer to this as \commitmergename.
+
\end{basedescript}
\end{basedescript}