\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}
-
~ian / topbloke-formulae.git / blobdiff