chiark / gitweb /
notation: fixes from paper markup of 389264b
[topbloke-formulae.git] / strategy.tex
index 9bed7cf..a4716b3 100644 (file)
@@ -6,7 +6,7 @@ remove dependencies from patches.
 
 Broadly speaking the update proceeds as follows: during the Ranking
 phase we construct the intended graph of dependencies between patches
 
 Broadly speaking the update proceeds as follows: during the Ranking
 phase we construct the intended graph of dependencies between patches
-(which involves select a merge order for the base branch of each
+(and incidentally select a merge order for the base branch of each
 patch).  Then during the Traversal phase we walk that graph from the
 bottom up, constructing for each patch by a series of merges and other
 operations first a new base branch head commit and then a new tip
 patch).  Then during the Traversal phase we walk that graph from the
 bottom up, constructing for each patch by a series of merges and other
 operations first a new base branch head commit and then a new tip
@@ -50,12 +50,9 @@ 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[ $\Gamma_{\pc}$ ]
-The desired direct dependencies of $\pc$, a set of patches.
-
-\item[ $\allpatches$ ]
-The set of all the patches we are dealing with (constructed
-during the update algorithm).
+\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} $.
 
 %\item[ $\set E_{\pc}$ ]
 %$ \bigcup_i \pendsof{S_{\pc,i}}{\pc} $.
@@ -77,7 +74,7 @@ during the update algorithm).
 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.
@@ -92,278 +89,38 @@ dependencies to use.  This allows the specification of any desired
 
 \end{basedescript}
 
 
 \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 {\bf Rank-Recurse}($\pc_0$)
-\item Until $\allpatches$ remains unchanged.
-\end{enumerate}
-\end{enumerate}
-
-{\bf Rank-Recurse}($\pc$) is:
-\begin{enumerate}
-
-\item If we have already done {\bf Rank-Recurse}($\pc$) in this
-ranking iteration, do nothing.  Otherwise:
-
-\item Add $\pc$ to $\allpatches$ if it is not there already.
-
-\item Let
-$$
-  \set S = 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 = 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 order 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_{S_i, j<i} M_i \le S_i
-   \right]
-$$
-
-\item Set $\Gamma = \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 \text{\bf 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]
-$$
-
-TODO define {\bf set-merge}
-
-\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.)
-\end{enumerate}
-\item Run ${\text{\bf Rank-Recurse}}(\pd)$.
-
-\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}$.
-
-\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}
-
-\section{Traversal phase}
-
-
-
-
-
-\section{Planning phase}
-
-The results of the planning phase consist of: 
-\begin{itemize*}
-\item{ The relation $\hasdirdep$ and hence the partial order $\hasdep$. }
-\item{ For each commit set $\pc$, a confirmed set of sources $\set S_{\pc}$. }
-\item{ For each commit set $\pc$, the order in which to merge the sources
-        $E_{\pc,j} \in \set E_{\pc}$. }
-\item{ For each $E_{\pc,j}$ an intended merge base $M_{\pc,j}$. }
-\end{itemize*}
-
-We use a recursive planning algorith, recursing over Topbloke commit
-sets (ie, sets $\py$ or $\pn$).  We'll call the commit set we're
-processing at each step $\pc$.
-At each recursive step 
-we make a plan to merge all $\set E_{\pc} = \{ E_{\pc,j \ldots} \}$
-and all the direct contributors of $\pc$ (as determined below)
-into $\tipzc$, to make $\tipfc$.
-
-We start with $\pc = \pl$ where $\pl = \patchof{L}$.
-
-
-\subsection{Direct contributors for $\pc = \pcn$}
+\stdsection{Important variables and values in the update algorithm}
 
 
-The direct contributors of $\pcn$ are the commit sets corresponding to
-the tip branches for the direct dependencies of the patch $\pc$.  We
-need to calculate what the direct dependencies are going to be.
-
-Choose an (arbitrary, but ideally somehow optimal in
-a way not discussed here) ordering of $\set E_{\pc}$, $E_{\pc,j}$
-($j = 1 \ldots m$).
-For brevity we will write $E_j$ for $E_{\pc,j}$.
-Remove from that set (and ordering) any $E_j$ which
-are $\le$ and $\neq$ some other $E_k$.
-
-Initially let $\set D_0 = \depsreqof{\tipzc}$.
-For each $E_j$ starting with $j=1$ choose a corresponding intended
-merge base $M_j$ such that $M_j \le E_j \land M_j \le T_{\pc,j-1}$.
-Calculate $\set D_j$ as the 3-way merge of the sets $\set D_{j-1}$ and
-$\depsreqof{E_j}$ using as a base $\depsreqof{M_j}$.  This will
-generate $D_m$ as the putative direct contributors of $\pcn$.
-
-However, the invocation may give instructions that certain direct
-dependencies are definitely to be included, or excluded.  As a result
-the set of actual direct contributors is some arbitrary set of patches
-(strictly, some arbitrary set of Topbloke tip commit sets).
-
-\subsection{Direct contributors for $\pc = \pcy$}
-
-The sole direct contributor of $\pcy$ is $\pcn$.
-
-\subsection{Recursive step}
-
-For each direct contributor $\p$, we add the edge $\pc \hasdirdep \p$
-and augment the ordering $\hasdep$ accordingly.
-
-If this would make a cycle in $\hasdep$, we abort . The operation must
-then be retried by the user, if desired, but with different or
-additional instructions for modifying the direct contributors of some
-$\pqn$ involved in the cycle.
-
-For each such $\p$, after updating $\hasdep$, we recursively make a plan
-for $\pc' = \p$.
-
-
-
-\section{Execution phase}
-
-We process commit sets from the bottom up according to the relation
-$\hasdep$.  For each commit set $\pc$ we construct $\tipfc$ from
-$\tipzc$, as planned.  By construction, $\hasdep$ has $\patchof{L}$
-as its maximum, so this operation will finish by updating
-$\tipca{\patchof{L}}$ with $\tipfa{\patchof{L}}$.
-
-After we are done with each commit set $\pc$, the
-new tip $\tipfc$ has the following properties:
-\[ \eqn{Tip Sources}{
-  \bigforall_{E_i \in \set E_{\pc}} \tipfc \ge E_i
-}\]
-\[ \eqn{Tip Dependencies}{
-  \bigforall_{\pc \hasdep \p} \tipfc \ge \tipfa \p
-}\]
-\[ \eqn{Perfect Contents}{
-  \tipfc \haspatch \p \equiv \pc \hasdep \py
-}\]
-
-For brevity we will sometimes write $\tipu$ for $\tipuc$, etc.  We will start
-out with $\tipc = \tipz$, and at each step of the way construct some
-$\tipu$ from $\tipc$.  The final $\tipu$ becomes $\tipf$.
-
-\subsection{Preparation}
-
-Firstly, we will check each $E_i$ for being $\ge \tipc$.  If
-it is, are we fast forward to $E_i$
---- formally, $\tipu = \text{max}(\tipc, E_i)$ ---
-and drop $E_i$ from the planned ordering.
-
-Then we will merge the direct contributors and the sources' ends.
-This generates more commits $\tipuc \in \pc$, but none in any other
-commit set.  We maintain
-$$
- \bigforall_{\p \isdep \pc}
- \pancsof{\tipcc}{\p} \subset
-   \pancsof{\tipfa \p}{\p}
-$$
-\proof{
- For $\tipcc = \tipzc$, $T$ ...WRONG WE NEED $\tipfa \p$ TO BE IN $\set E$ SOMEHOW
+\begin{basedescript}{
+\desclabelwidth{5em}
+\desclabelstyle{\nextlinelabel}
 }
 }
+\item[ $\Gamma_{\pc}$ ]
+The desired direct dependencies of $\pc$, a set of patches.
 
 
-\subsection{Merge Contributors for $\pcy$}
-
-Merge $\pcn$ into $\tipc$.  That is, merge with
-$L = \tipc, R = \tipfa{\pcn}, M = \baseof{\tipc}$.
-to construct $\tipu$.
-
-Merge conditions:
-
-Ingredients satisfied by construction.
-Tip Merge satisfied by construction.  Merge Acyclic follows
-from Perfect Contents and $\hasdep$ being acyclic.
-
-Removal Merge Ends: For $\p = \pc$, $M \nothaspatch \p$; OK.
-For $\p \neq \pc$, by Tip Contents,
-$M \haspatch \p \equiv L \haspatch \p$, so we need only
-worry about $X = R, Y = L$; ie $L \haspatch \p$,
-$M = \baseof{L} \haspatch \p$.
-By Tip Contents for $L$, $D \le L \equiv D \le M$.  OK.~~$\qed$
-
-WIP UP TO HERE
-
-Addition Merge Ends: If $\py \isdep \pcn$, we have already
-done the execution phase for $\pcn$ and $\py$.  By
-Perfect Contents for $\pcn$, $\tipfa \pcn \haspatch \p$ i.e.
-$R \haspatch \p$.  So we only need to worry about $Y = R = \tipfa \pcn$.
-By Tip Dependencies $\tipfa \pcn \ge \tipfa \py$.
-And by Tip Sources $\tipfa \py \ge $
-
-want to prove $E \le \tipfc$ where $E \in \pendsof{\tipcc}{\py}$
-
-$\pancsof{\tipcc}{\py} = $
-
-
-computed $\tipfa \py$, and by Perfect Contents for $\py$
-
-
-with $M=M_j, L=T_{\pc,j-1}, R=E_j$,
-and calculate what the resulting desired direct dependencies file
-(ie, the set of patches $\set D_j$)
-would be.  Eventually we 
-
-So, formally, we select somehow an order of sources $S_i$.  For each 
-
+\item[ $\allpatches$ ]
+The set of all the patches we are dealing with (constructed
+during the update algorithm).
 
 
-Make use of the following recursive algorithm, Plan 
+\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[ $\allreach$ ]
+The set of all reachable commits.
 
 
+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$.
 
 
- recursively make a plan to merge all $E = \pends$
+\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)$.
 
 
-Specifically, in
+\end{basedescript}