From f5c0ce1c1ebca23fac2638994160aee5fdc76d8e Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 18 Mar 2012 10:44:03 +0000 Subject: [PATCH] rationalise patch notation names - annotations --- annotations.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/annotations.tex b/annotations.tex index 1bf2fcd..72b00e8 100644 --- a/annotations.tex +++ b/annotations.tex @@ -4,12 +4,12 @@ We annotate each Topbloke commit $C$ with: \gathbegin \patchof{C} \gathnext - \baseof{C}, \text{ if } C \in \py + \baseof{C}, \text{ if } C \in \pay{C} \gathnext - \bigforall_{\pq} - \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq + \bigforall_{\p} + \text{ either } C \haspatch \p \text{ or } C \nothaspatch \p \gathnext - \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy} + \bigforall_{\py \not\ni C} \pendsof{C}{\py} \end{gather} $\patchof{C}$, for each kind of Topbloke-generated commit, is stated @@ -18,19 +18,19 @@ in the summary in the section for that kind of commit. 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 \pq$ or $\nothaspatch \pq$ is represented as a -list of $\pq$ for which it is known that $C \haspatch \pq$; -for any $\pq$ not listed, $C \nothaspatch \pq$. -Whether to record $C \haspatch \pq$ in a new commit +$C \haspatch \p$ or $\nothaspatch \p$ is represented as a +list of $\p$ for which it is known that $C \haspatch \p$; +for any $\p$ not listed, $C \nothaspatch \p$. +Whether to record $C \haspatch \p$ in a new commit is in stated -(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$ +(in terms of $I \haspatch \p$ or $I \nothaspatch \p$ for the ingredients $I$) in the proof of Coherence for each kind of commit. -$\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits, +$\pendsof{C}{\py}$ is computed, for all Topbloke-generated commits, using the lemma Calculation of Ends, above. -We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would +We do not annotate $\pendsof{C}{\pay{C}}$ for $C \in \pay{C}$. 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_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. +because $\forall_{\pay{C} \ni C} \; \pendsof{C}{\pay{C}} = \{C\}$. -- 2.30.2