strategy: wip traversal.

[topbloke-formulae.git] / strategy.tex

diff --git a/strategy.tex b/strategy.tex
index 62998371becf379d9aea154b32663e7d034c0ae2..a4716b313dd577c5e74c6e1a7afe4f39ba8be082 100644 (file)
--- a/strategy.tex
+++ b/strategy.tex
@@ -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,25 @@ 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[ $\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.

 
 

-\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$.
+\item[ $\allreach$ ]
+The set of all reachable commits.

 
 

-\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}
+A reachable commit is one we might refer to explicitly in any of these
+algorithms, and any ancestor of such a commit.  We explicitly
+enumerate all of the input commits ($\allsrcs$), so the reachable
+commits are originally the input commits and their ancestors.

 
 

+$\allreach$ varies over time as we generate more commits.  Each
+commit we generate will have only reachable commits as ancestors, so
+generating a new commit (only) adds that new commit to $\allreach$.

 
 

+\item[ $\allreachof{\py}$ ]
+The set of reachable commits at the point where we have just generated
+$\tippy$, i.e. just after $\alg{Merge-Tip}(\p)$.

 
 

+\end{basedescript}