From d1a680abdf1985a08c1a88157588ef881df7fb29 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 28 May 2012 00:16:52 +0100 Subject: [PATCH] annotate foreign ends too --- annotations.tex | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/annotations.tex b/annotations.tex index 3401475..b4e86da 100644 --- 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} +\gathnext + \pendsof{C}{\foreign} \end{gather} $\patchof{C}$, for each kind of Topbloke-generated commit, is stated @@ -27,10 +29,11 @@ is in stated 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. -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 -because $\forall_{\pay{C} \ni C} \; \pendsof{C}{\pay{C}} = \{C\}$. +because $\forall_{\set S \ni C} \; \pendsof{C}{\set S} = \{C\}$. -- 2.30.2