chiark / gitweb /
notation: remove notation test file
[topbloke-formulae.git] / strategy.tex
index 62998371becf379d9aea154b32663e7d034c0ae2..bfd392224d6e5c854573b4988f4314fd66d40530 100644 (file)
@@ -50,6 +50,10 @@ the $\le$-maximal elements of $\bigcup_{J \in \set J} \pendsof{J}{\p}$
 Convenience notation for
 $\bigforall_{E \in \pendsof{\set X}{\p}} E \le T$
 
 Convenience notation for
 $\bigforall_{E \in \pendsof{\set X}{\p}} E \le T$
 
+\item[ $\allsrcs$ ]
+$\bigcup_{\p \in \allpatches} \set H^{\pn} \cup \set H^{\py}$.
+All the input commits to the update algorithm.  (See below.)
+
 %\item[ $\set E_{\pc}$ ]
 %$ \bigcup_i \pendsof{S_{\pc,i}}{\pc} $.
 %All the ends of $\pc$ in the sources.
 %\item[ $\set E_{\pc}$ ]
 %$ \bigcup_i \pendsof{S_{\pc,i}}{\pc} $.
 %All the ends of $\pc$ in the sources.
@@ -70,7 +74,7 @@ $\bigforall_{E \in \pendsof{\set X}{\p}} E \le T$
 The topmost patch which we are trying to update.  This and
 all of its dependencies will be updated.
 
 The topmost patch which we are trying to update.  This and
 all of its dependencies will be updated.
 
-\item[ $h : \pc^{+/-} \mapsto \set H_{\pc^{+/-}}$ ]
+\item[ $h : \pc^{+/-} \mapsto \set H^{\pc^{+/-}}$ ]
 Function for getting the existing heads $\set H$ of the branch $\pc^{+/-}$.
 These are the heads which will be merged and used in this update.
 This will include the current local and remote git refs, as desired.
 Function for getting the existing heads $\set H$ of the branch $\pc^{+/-}$.
 These are the heads which will be merged and used in this update.
 This will include the current local and remote git refs, as desired.
@@ -98,181 +102,10 @@ The desired direct dependencies of $\pc$, a set of patches.
 The set of all the patches we are dealing with (constructed
 during the update algorithm).
 
 The set of all the patches we are dealing with (constructed
 during 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}
-
-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 tip
-
-\end{itemize}
-
-\subsection{$\alg{Merge-Base}(\pc)$}
-
-This algorithm attempts to construct a suitably updated version of the
-base branch $\pcn$.
-
-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.
-
-\subsubsection{Bases and sources}
-
-In some order, perhaps interleaving the two kinds of merge:
-
-\begin{enumerate}
-
-\item For each $\pd \isdirdep \pc$, merge $\pd$
-
-\item
-
-\end{enumerate}
-
+\item[ $\tipcn, \tipcy$ ]
+The new tips of the git branches $\pcn$ and $\pcy$, containing
+all the appropriate commits (and the appropriate other patches),
+as generated by the Traversal phase of the update algorithm.
 
 
+\end{basedescript}