X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=strategy.tex;h=bf136f69c912d185b9531089fafc2dd2922913c6;hp=0f03ddb9883200fed514b821df14948994e78aca;hb=8ee16bd8a84437fc51257805eb234c4dee054889;hpb=e284656ebfa338be8bc3a02de60391063d9f8f3d

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}
-