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 \pay{C}
   8 \gathnext
   9  \bigforall_{\p}
  10    \text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
  11 \gathnext
  12  \bigforall_{\py \not\ni C} \pendsof{C}{\py}
  13 \gathnext
  14  \pendsof{C}{\foreign}
  15 \end{gather}
  16
  17 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
  18 in the summary in the section for that kind of commit.
  19
  20 Whether $\baseof{C}$ is required, and if so what the value is, is
  21 stated in the proof of Unique Base for each kind of commit.
  22
  23 $C \haspatch \p$ or $\nothaspatch \p$ is represented as a
  24 list of $\p$ for which $C \haspatch \p$;
  25 for any $\p$ not listed, $C \nothaspatch \p$.
  26 Whether to record $C \haspatch \p$ in a new commit
  27 is in stated
  28 (in terms of $I \haspatch \p$ or $I \nothaspatch \p$
  29 for the ingredients $I$)
  30 in the proof of Coherence for each kind of commit.
  31
  32 $\pendsof{C}{\py}$ and $\pendsof{C}{\foreign}$
  33 are computed, for all Topbloke-generated commits,
  34 using the lemma Calculation of Ends, above.
  35 We do not annotate $\pendsof{C}{\set S}$ for $C \in \set S$.  Doing so would
  36 make it wrong to make plain commits with git because the recorded $\pends$
  37 would have to be updated.  The annotation is not needed in that case
  38 because $\forall_{\set S \ni C} \; \pendsof{C}{\set S} = \{C\}$.
  39