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
formatting: use \pagestyle{fancyplain} so "plain" (chapter heading) pages are just...
[topbloke-formulae.git]
/
annotations.tex
diff --git
a/annotations.tex
b/annotations.tex
index 72b00e8cc63055f3dbcb3db1a9e5fbd6d6b6ea0a..b4e86dab19b0648af7998e233209b520e0b7011c 100644
(file)
--- a/
annotations.tex
+++ b/
annotations.tex
@@
-10,6
+10,8
@@
We annotate each Topbloke commit $C$ with:
\text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
\gathnext
\bigforall_{\py \not\ni C} \pendsof{C}{\py}
\text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
\gathnext
\bigforall_{\py \not\ni C} \pendsof{C}{\py}
+\gathnext
+ \pendsof{C}{\foreign}
\end{gather}
$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
\end{gather}
$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
@@
-19,7
+21,7
@@
Whether $\baseof{C}$ is required, and if so what the value is, is
stated in the proof of Unique Base for each kind of commit.
$C \haspatch \p$ or $\nothaspatch \p$ is represented as a
stated in the proof of Unique Base for each kind of commit.
$C \haspatch \p$ or $\nothaspatch \p$ is represented as a
-list of $\p$ for which
it is known that
$C \haspatch \p$;
+list of $\p$ for which $C \haspatch \p$;
for any $\p$ not listed, $C \nothaspatch \p$.
Whether to record $C \haspatch \p$ in a new commit
is in stated
for any $\p$ not listed, $C \nothaspatch \p$.
Whether to record $C \haspatch \p$ in a new commit
is in stated
@@
-27,10
+29,11
@@
is in stated
for the ingredients $I$)
in the proof of Coherence for each kind of commit.
for the ingredients $I$)
in the proof of Coherence for each kind of commit.
-$\pendsof{C}{\py}$ is computed, for all Topbloke-generated commits,
+$\pendsof{C}{\py}$ and $\pendsof{C}{\foreign}$
+are computed, for all Topbloke-generated commits,
using the lemma Calculation of Ends, above.
using the lemma Calculation of Ends, above.
-We do not annotate $\pendsof{C}{\
pay{C}}$ for $C \in \pay{C}
$. Doing so would
+We do not annotate $\pendsof{C}{\
set S}$ for $C \in \set S
$. Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
would have to be updated. The annotation is not needed in that case
make it wrong to make plain commits with git because the recorded $\pends$
would have to be updated. The annotation is not needed in that case
-because $\forall_{\
pay{C} \ni C} \; \pendsof{C}{\pay{C}
} = \{C\}$.
+because $\forall_{\
set S \ni C} \; \pendsof{C}{\set S
} = \{C\}$.