chiark / gitweb /
annotation calculation
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)
article.tex

index b4f7beb..70d6d88 100644 (file)
@@ -95,8 +95,6 @@
 
 \section{Notation}
 
-xxx make all conditions be in conditions, not in (or also in) intro
-
 \begin{basedescript}{
 \desclabelwidth{5em}
 \desclabelstyle{\nextlinelabel}
@@ -324,8 +322,6 @@ $\qed$
 
 \section{Commit annotation}
 
-xxx need to compute annotation for every commit type
-
 We annotate each Topbloke commit $C$ with:
 \gathbegin
  \patchof{C}
@@ -338,10 +334,25 @@ We annotate each Topbloke commit $C$ with:
  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 \end{gather}
 
+$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
+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 \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
+set $\{ \pa{Q} | C \haspatch \pa{Q} \}$.  Whether $C \haspatch \pa{Q}$
+is in stated
+(in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
+for the ingredients $I$),
+in the proof of Coherence for each kind of commit.
+
+$\pendsof{C}{\pa{Q}^+}$ 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
 make it wrong to make plain commits with git because the recorded $\pends$
-would have to be updated.  The annotation is not needed because
-$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
+would have to be updated.  The annotation is not needed in that case
+because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 
 \section{Simple commit}