strategy: traversal wip

[topbloke-formulae.git] / strategy.tex

diff --git a/strategy.tex b/strategy.tex
index 48d93d77954256085eb3d44c0dcf0eb52272d065..35049b56424cca0746781e9743eda0909a921005 100644 (file)
--- a/strategy.tex
+++ b/strategy.tex
@@ -155,16 +155,19 @@ if available.
 \item For each $i \ldots 1..n$, update our putative direct
 dependencies:
 $$
-\Gamma \assign \alg{set-merge}\left[\Gamma,
- \left( \begin{cases} 
-  M_i \in \pcn :     & \depsreqof{M_i} \\
-  M_i \not\in \pcn : & \{ \}
- \end{cases} \right),
- \depsreqof{S_i}
- \right]
+\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 $\alg{set-merge}$
+TODO define $\setmerge$
 
 \item Finalise our putative direct dependencies
 $
@@ -178,8 +181,8 @@ $
 as necessary).
 If this results in a cycle, abort entirely (as the function $g$ is
 inappropriate; a different $g$ could work).
-\end{enumerate}
 \item Run $\alg{Rank-Recurse}(\pd)$.
+\end{enumerate}
 
 \end{enumerate}
 
@@ -209,17 +212,64 @@ 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 $C \in \allpatches$ in topological order by $\hasdep$,
+For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
 lowest first:
 
 \begin{enumerate}
 
-\item Optionally, attempt $\alg{Merge-Base}(\pc)$.
+\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$
+
+\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$
+
+\item
+
+\end{enumerate}
+
+
+
 
 \section{Planning phase}