annotations.tex

   1 \section{Commit annotation}
   2
   3 We annotate each Topbloke commit $C$ with:
   4 \gathbegin
   5  \patchof{C}
   6 \gathnext
   7  \baseof{C}, \text{ if } C \in \py
   8 \gathnext
   9  \bigforall_{\pq}
  10    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
  11 \gathnext
  12  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
  13 \end{gather}
  14
  15 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
  16 in the summary in the section for that kind of commit.
  17
  18 Whether $\baseof{C}$ is required, and if so what the value is, is
  19 stated in the proof of Unique Base for each kind of commit.
  20
  21 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
  22 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
  23 is in stated
  24 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
  25 for the ingredients $I$)
  26 in the proof of Coherence for each kind of commit.
  27
  28 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
  29 using the lemma Calculation of Ends, above.
  30 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
  31 make it wrong to make plain commits with git because the recorded $\pends$
  32 would have to be updated.  The annotation is not needed in that case
  33 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
  34