From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 27 May 2012 23:22:47 +0000 (+0100)
Subject: strategy: split into more files
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=8ee16bd8a84437fc51257805eb234c4dee054889

strategy: split into more files
---

diff --git a/article.tex b/article.tex
index 6e3d515..96857aa 100644
--- a/article.tex
+++ b/article.tex
@@ -174,5 +174,8 @@
 \chapter{Update strategy}
 
 \input{strategy.tex}
+\input{ranking.tex}
+\input{trav-alg.tex}
+\input{trav-proofs.tex}
 
 \end{document}
diff --git a/ranking.tex b/ranking.tex
new file mode 100644
index 0000000..e705a56
--- /dev/null
+++ b/ranking.tex
@@ -0,0 +1,124 @@
+\section{Ranking phase}
+
+We run the following algorithm:
+\begin{enumerate}
+\item Set $\allpatches = \{ \}$.
+\item Repeatedly:
+\begin{enumerate}
+\item Clear out the graph $\hasdirdep$ so it has no edges.
+\item Execute $\alg{Rank-Recurse}(\pc_0)$
+\item Until $\allpatches$ remains unchanged.
+\end{enumerate}
+\end{enumerate}
+
+$\alg{Rank-Recurse}(\pc)$ is:
+\begin{enumerate}
+
+\item If we have already done $\alg{Rank-Recurse}(\pc)$ in this
+ranking iteration, do nothing.  Otherwise:
+
+\item Add $\pc$ to $\allpatches$ if it is not there already.
+
+\item Set
+$$
+  \set S \iassign h(\pcn)
+     \cup 
+        \bigcup_{\p \in \allpatches}
+        \bigcup_{H \in h(\pn) \lor H \in h(\py)}
+         \{ \baseof{E} \; | \; E \in \pendsof{H}{\pcy} \}
+$$
+
+and $W \iassign w(h(\pcn))$
+
+\item While $\exists_{S \in \set S} S \ge W$,
+update $W \assign S$ and $\set S \assign \set S \, \backslash \{ S \}$
+
+(This will often remove $W$ from $\set S$.  Afterwards, $\set S$
+is a collection of heads to be merged into $W$.)
+
+\item Choose an ordering of $\set S$, $S_i$ for $i=1 \ldots n$.
+
+\item For each $S_i$ in turn, choose a corresponding $M_i$
+such that $$
+   M_i \le S_i \land \left[
+   M_i \le W \lor \bigexists_{j<i} M_i \le S_j
+   \right]
+$$
+
+\item Set $\Gamma \iassign \depsreqof{W}$.
+
+If there are multiple candidates we prefer $M_i \in \pcn$
+if available.
+
+\item For each $i \ldots 1..n$, update our putative direct
+dependencies:
+$$
+\Gamma \assign \setmergeof{
+    \Gamma
+  }{
+    \begin{cases}
+     M_i \in \pcn :     & \depsreqof{M_i} \\
+     M_i \not\in \pcn : & \{ \}
+    \end{cases}
+  }{
+    \depsreqof{S_i}
+  }
+$$
+
+TODO define $\setmerge$
+
+\item Finalise our putative direct dependencies
+$
+\Gamma \assign g(\pc, \Gamma)
+$
+
+\item For each direct dependency $\pd \in \Gamma$,
+
+\begin{enumerate}
+\item Add an edge $\pc \hasdirdep \pd$ to the digraph (adding nodes
+as necessary).
+If this results in a cycle, abort entirely (as the function $g$ is
+inappropriate; a different $g$ could work).
+\item Run $\alg{Rank-Recurse}(\pd)$.
+\end{enumerate}
+
+\end{enumerate}
+
+\subsection{Results of the ranking phase}
+
+By the end of the ranking phase, we have recorded the following
+information:
+
+\begin{itemize}
+\item
+$ \allpatches, \hasdirdep $ and hence the completion of $\hasdirdep$
+into the partial order $\hasdep$.
+
+\item
+For each $\pc \in \allpatches$,
+the base branch starting point commit $W^{\pcn} = W$.
+
+\item
+For each $\pc$,
+the direct dependencies $\Gamma^{\pc} = \Gamma$.
+
+\item
+For each $\pc$,
+the ordered set of base branch sources $\set S^{\pcn} = \set S,
+S^{\pcn}_i = S_i$
+and corresponding merge bases $M^{\pcn}_i = M_i$.
+
+\end{itemize}
+
+\subsection{Proof of termination}
+
+$\alg{Rank-Recurse}(\pc)$ recurses but only downwards through the
+finite graph $\hasdirdep$, so it must terminate.  
+
+The whole ranking algorithm iterates but each iteration involves
+adding one or more patches to $\allpatches$.  Since there are
+finitely many patches and we never remove anything from $\allpatches$
+this must complete eventually.
+
+$\qed$
+
diff --git a/strategy.tex b/strategy.tex
index 0f03ddb..bf136f6 100644
--- a/strategy.tex
+++ b/strategy.tex
@@ -105,273 +105,3 @@ generated by the Traversal phase of the update algorithm.
 
 \end{basedescript}
 
-\section{Ranking phase}
-
-We run the following algorithm:
-\begin{enumerate}
-\item Set $\allpatches = \{ \}$.
-\item Repeatedly:
-\begin{enumerate}
-\item Clear out the graph $\hasdirdep$ so it has no edges.
-\item Execute $\alg{Rank-Recurse}(\pc_0)$
-\item Until $\allpatches$ remains unchanged.
-\end{enumerate}
-\end{enumerate}
-
-$\alg{Rank-Recurse}(\pc)$ is:
-\begin{enumerate}
-
-\item If we have already done $\alg{Rank-Recurse}(\pc)$ in this
-ranking iteration, do nothing.  Otherwise:
-
-\item Add $\pc$ to $\allpatches$ if it is not there already.
-
-\item Set
-$$
-  \set S \iassign h(\pcn)
-     \cup 
-        \bigcup_{\p \in \allpatches}
-        \bigcup_{H \in h(\pn) \lor H \in h(\py)}
-         \{ \baseof{E} \; | \; E \in \pendsof{H}{\pcy} \}
-$$
-
-and $W \iassign w(h(\pcn))$
-
-\item While $\exists_{S \in \set S} S \ge W$,
-update $W \assign S$ and $\set S \assign \set S \, \backslash \{ S \}$
-
-(This will often remove $W$ from $\set S$.  Afterwards, $\set S$
-is a collection of heads to be merged into $W$.)
-
-\item Choose an ordering of $\set S$, $S_i$ for $i=1 \ldots n$.
-
-\item For each $S_i$ in turn, choose a corresponding $M_i$
-such that $$
-   M_i \le S_i \land \left[
-   M_i \le W \lor \bigexists_{j<i} M_i \le S_j
-   \right]
-$$
-
-\item Set $\Gamma \iassign \depsreqof{W}$.
-
-If there are multiple candidates we prefer $M_i \in \pcn$
-if available.
-
-\item For each $i \ldots 1..n$, update our putative direct
-dependencies:
-$$
-\Gamma \assign \setmergeof{
-    \Gamma
-  }{
-    \begin{cases}
-     M_i \in \pcn :     & \depsreqof{M_i} \\
-     M_i \not\in \pcn : & \{ \}
-    \end{cases}
-  }{
-    \depsreqof{S_i}
-  }
-$$
-
-TODO define $\setmerge$
-
-\item Finalise our putative direct dependencies
-$
-\Gamma \assign g(\pc, \Gamma)
-$
-
-\item For each direct dependency $\pd \in \Gamma$,
-
-\begin{enumerate}
-\item Add an edge $\pc \hasdirdep \pd$ to the digraph (adding nodes
-as necessary).
-If this results in a cycle, abort entirely (as the function $g$ is
-inappropriate; a different $g$ could work).
-\item Run $\alg{Rank-Recurse}(\pd)$.
-\end{enumerate}
-
-\end{enumerate}
-
-\subsection{Results of the ranking phase}
-
-By the end of the ranking phase, we have recorded the following
-information:
-
-\begin{itemize}
-\item
-$ \allpatches, \hasdirdep $ and hence the completion of $\hasdirdep$
-into the partial order $\hasdep$.
-
-\item
-For each $\pc \in \allpatches$,
-the base branch starting point commit $W^{\pcn} = W$.
-
-\item
-For each $\pc$,
-the direct dependencies $\Gamma^{\pc} = \Gamma$.
-
-\item
-For each $\pc$,
-the ordered set of base branch sources $\set S^{\pcn} = \set S,
-S^{\pcn}_i = S_i$
-and corresponding merge bases $M^{\pcn}_i = M_i$.
-
-\end{itemize}
-
-\subsection{Proof of termination}
-
-$\alg{Rank-Recurse}(\pc)$ recurses but only downwards through the
-finite graph $\hasdirdep$, so it must terminate.  
-
-The whole ranking algorithm iterates but each iteration involves
-adding one or more patches to $\allpatches$.  Since there are
-finitely many patches and we never remove anything from $\allpatches$
-this must complete eventually.
-
-$\qed$
-
-\section{Traversal phase --- algorithm}
-
-(In general, unless stated otherwise below, when we generate a new
-commit $C$ using one of the commit kind algorith, we update
-$W \assign C$.  In any such case where we say we're going to Merge
-with $L = W$, if $R \ge W$ we do not Merge but instead simply set
-$W \assign R$.)
-
-
-For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
-lowest first:
-
-\begin{enumerate}
-
-\item Optionally, attempt
- $\alg{Merge-Base}(\pc)$.  This may or may not succeed.
-
-\item If this didn't succeed, or was not attempted, execute
- $\alg{Recreate-Base}(\pc)$.
-
-\item Then in any case, execute
- $\alg{Merge-Tip}(\pc)$.
-
-\end{enumerate}
-
-After processing each $\pc$ we will have created:
-
-\begin{itemize}
-
-\item $\tipcn$ and $\tipcy$ such that $\baseof{\tipcy} = \tipcn$.
-
-\end{itemize}
-
-\subsection{$\alg{Merge-Base}(\pc)$}
-
-This algorithm attempts to construct a suitably updated version of the
-base branch $\pcn$ using some existing version of $\pcn$ as a starting
-point.
-
-It should be executed noninteractively.  Specifically, if any step
-fails with a merge conflict, the whole thing should be abandoned.
-This avoids asking the user to resolve confusing conflicts.  It also
-avoids asking the user to pointlessly resolve conflicts in situations
-where we will later discover that $\alg{Merge-Base}$ wasn't feasible
-after all.
-
-If $\pc$ has only one direct dependency, this algorithm should not be
-used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
-to generate a perfect answer, whereas this algorithm might involve
-merges and therefore might not produce a perfect answer if the
-situation is complicated.
-
-Initially, set $W \iassign W^{\pcn}$.
-
-\subsubsection{Bases and sources}
-
-In some order, perhaps interleaving the two kinds of merge:
-
-\begin{enumerate}
-
-\item For each $\pd \isdirdep \pc$, find a merge base
-$M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
-That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
-(Dependency Merge.)
-
-\item For each $S \in S^{\pcn}_i$, merge it into $W$.
-That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
-(Base Sibling Merge.)
-
-\end{enumerate}
-
-\subsubsection{Fixup}
-
-Execute $\alg{Fixup-Base}(W,\pc)$.
-
-
-\subsection{$\alg{Recreate-Base}(\pc)$}
-
-\begin{enumerate}
-
-\item
-
-Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
-
-\item
-
-Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$
-and set $W \iassign C$.  (Recreate Base Beginning.)
-
-\item
-
-Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
-
-\item
-
-Declare that we contain all of the relevant information from the
-sources.  That is, use $\alg{Pseudo-merge}$ with $L = W, \;
-\set R = \{ W \} \cup \set S^{\pcn}$.
-(Recreate Base Final Declaration.)
-
-\end{enumerate}
-
-\subsubsection{$\alg{Recreate-Recurse}(\pd)$}
-
-\begin{enumerate}
-
-\item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.
-
-\item TODO what about non-Topbloke base branches
-
-\item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
-(Recreate Base Dependency Base Declaration.)
-
-\item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
-execute $\alg{Recreate-Recurse}(\pd')$.
-
-\item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
-$L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
-(Recreate Reapply.)
-
-\end{enumerate}
-
-
-\subsection{$\alg{Merge-Tip}(\pc)$}
-
-\begin{enumerate}
-
-\item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
-
-\item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
-R = \tipcn$ and choose any suitable $M$.  (Tip Base Merge.)
-
-\item For each source $S \in \set S^{\pcy}$,
-$\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
-(Tip Source Merge.)
-
-\end{enumerate}
-
-
-\section{Traversal phase --- proofs}
-
-For each operation called for by the traversal algorithms, we prove
-that the commit generation preconditions are met.
-
-\subsection{Tip Base Merge}
-
diff --git a/trav-alg.tex b/trav-alg.tex
new file mode 100644
index 0000000..37d9194
--- /dev/null
+++ b/trav-alg.tex
@@ -0,0 +1,139 @@
+\section{Traversal phase --- algorithm}
+
+(In general, unless stated otherwise below, when we generate a new
+commit $C$ using one of the commit kind algorith, we update
+$W \assign C$.  In any such case where we say we're going to Merge
+with $L = W$, if $R \ge W$ we do not Merge but instead simply set
+$W \assign R$.)
+
+
+For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
+lowest first:
+
+\begin{enumerate}
+
+\item Optionally, attempt
+ $\alg{Merge-Base}(\pc)$.  This may or may not succeed.
+
+\item If this didn't succeed, or was not attempted, execute
+ $\alg{Recreate-Base}(\pc)$.
+
+\item Then in any case, execute
+ $\alg{Merge-Tip}(\pc)$.
+
+\end{enumerate}
+
+After processing each $\pc$ we will have created:
+
+\begin{itemize}
+
+\item $\tipcn$ and $\tipcy$ such that $\baseof{\tipcy} = \tipcn$.
+
+\end{itemize}
+
+\subsection{$\alg{Merge-Base}(\pc)$}
+
+This algorithm attempts to construct a suitably updated version of the
+base branch $\pcn$ using some existing version of $\pcn$ as a starting
+point.
+
+It should be executed noninteractively.  Specifically, if any step
+fails with a merge conflict, the whole thing should be abandoned.
+This avoids asking the user to resolve confusing conflicts.  It also
+avoids asking the user to pointlessly resolve conflicts in situations
+where we will later discover that $\alg{Merge-Base}$ wasn't feasible
+after all.
+
+If $\pc$ has only one direct dependency, this algorithm should not be
+used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
+to generate a perfect answer, whereas this algorithm might involve
+merges and therefore might not produce a perfect answer if the
+situation is complicated.
+
+Initially, set $W \iassign W^{\pcn}$.
+
+\subsubsection{Bases and sources}
+
+In some order, perhaps interleaving the two kinds of merge:
+
+\begin{enumerate}
+
+\item For each $\pd \isdirdep \pc$, find a merge base
+$M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
+That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
+(Dependency Merge.)
+
+\item For each $S \in S^{\pcn}_i$, merge it into $W$.
+That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
+(Base Sibling Merge.)
+
+\end{enumerate}
+
+\subsubsection{Fixup}
+
+Execute $\alg{Fixup-Base}(W,\pc)$.
+
+
+\subsection{$\alg{Recreate-Base}(\pc)$}
+
+\begin{enumerate}
+
+\item
+
+Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
+
+\item
+
+Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$
+and set $W \iassign C$.  (Recreate Base Beginning.)
+
+\item
+
+Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
+
+\item
+
+Declare that we contain all of the relevant information from the
+sources.  That is, use $\alg{Pseudo-merge}$ with $L = W, \;
+\set R = \{ W \} \cup \set S^{\pcn}$.
+(Recreate Base Final Declaration.)
+
+\end{enumerate}
+
+\subsubsection{$\alg{Recreate-Recurse}(\pd)$}
+
+\begin{enumerate}
+
+\item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.
+
+\item TODO what about non-Topbloke base branches
+
+\item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
+(Recreate Base Dependency Base Declaration.)
+
+\item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
+execute $\alg{Recreate-Recurse}(\pd')$.
+
+\item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
+$L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
+(Recreate Reapply.)
+
+\end{enumerate}
+
+
+\subsection{$\alg{Merge-Tip}(\pc)$}
+
+\begin{enumerate}
+
+\item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
+
+\item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
+R = \tipcn$ and choose any suitable $M$.  (Tip Base Merge.)
+
+\item For each source $S \in \set S^{\pcy}$,
+$\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
+(Tip Source Merge.)
+
+\end{enumerate}
+
+
diff --git a/trav-proofs.tex b/trav-proofs.tex
new file mode 100644
index 0000000..14f6cd8
--- /dev/null
+++ b/trav-proofs.tex
@@ -0,0 +1,7 @@
+\section{Traversal phase --- proofs}
+
+For each operation called for by the traversal algorithms, we prove
+that the commit generation preconditions are met.
+
+\subsection{Tip Base Merge}
+