1 \section{Traversal phase}
3 In general, unless stated otherwise below, when we generate a new
4 commit $C$ using one of the commit kind recipies, we update
5 $W \assign C$. In any such case where we say we're going to Merge
6 with $L = W$, if $R \ge W$ we do not Merge but instead simply set
9 For each commit generation operation called for by the traversal
10 algorithms, we prove that the commit generation preconditions are met.
12 \subsection{Algorithm}
14 For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
19 \item Optionally, attempt
20 $\alg{Merge-Base}(\pc)$. This may or may not succeed.
22 \item If this didn't succeed, or was not attempted, execute
23 $\alg{Recreate-Base}(\pc)$.
25 \item Then in any case, execute
26 $\alg{Merge-Tip}(\pc)$.
32 After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
34 \statement{Correct Base}{
35 \baseof{\tipcy} = \tipcn
37 \statement{Base Correct Contents}{
38 \tipcn \haspatch \pa E
42 \statement{Tip Covers Reachable}{
43 \tipcy \ge \pendsof{\allreachof{\pcy}}{\pcy}
45 \statement{Base Covers Inputs' Bases}{
46 \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
48 \statement{Base Covers Base Inputs}{
49 \bigforall_{H \in \set H^{\pn}} \tipcn \ge H
52 \subsection{Reachability and coverage}
54 We ensure Tip Covers Reachable as follows:
57 \item We do not generate any commits $\in \py$ other than
58 during $\alg{Merge-Tip}(\py)$;
59 \item So at the start of $\alg{Merge-Tip}(\py)$,
60 $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $
61 \item $\alg{Merge-tip}$ arranges that when it is done
62 $\tippy \ge \pendsof{\allreach}{\py}$ --- see below.
65 A corrolary is as follows:
66 \statement{Tip Covers Superior Reachable} {
67 \bigforall_{\pd \isdep \pc}
68 \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy}
71 No commits $\in \pdy$ are created other than during
72 $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed)
73 before $\alg{Merge-Tip}(\pcy)$
74 So $\pendsof{\allreachof{\pcy}}{\pdy} =
75 \pendsof{\allreachof{\pdy}}{\pdy}$.
78 \subsection{Traversal Lemmas}
80 \statement{Tip Correct Contents}{
81 \tipcy \haspatch \pa E
83 \pa E = \pc \lor \pa E \isdep \pc
86 For $\pc = \pa E$, Tip Own Contents suffices.
87 For $\pc \neq \pa E$, Exclusive Tip Contents
88 gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
89 which by Correct Base $\equiv D \isin \tipcn$.
92 \subsection{$\alg{Merge-Base}(\pc)$}
94 This algorithm attempts to construct a suitably updated version of the
95 base branch $\pcn$ using some existing version of $\pcn$ as a starting
98 It should be executed noninteractively. Specifically, if any step
99 fails with a merge conflict, the whole thing should be abandoned.
100 This avoids asking the user to resolve confusing conflicts. It also
101 avoids asking the user to pointlessly resolve conflicts in situations
102 where we will later discover that $\alg{Merge-Base}$ wasn't feasible
105 If $\pc$ has only one direct dependency, this algorithm should not be
106 used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
107 to generate a perfect answer, whereas this algorithm might involve
108 merges and therefore might not produce a perfect answer if the
109 situation is complicated.
111 For \alg{Merge-Base} we do not prove that the preconditions are met.
112 Instead, we check them at runtime. If they turn out not to be met, we
113 abandon \alg{Merge-Base} and resort to \alg{Recreate-Base}.
115 Initially, set $W \iassign W^{\pcn}$.
117 \subsubsection{Bases and sources}
119 In some order, perhaps interleaving the two kinds of merge:
123 \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base
124 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
125 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
127 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
128 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
129 (Base Sibling Merge.)
133 \subsubsection{Fixup}
135 Execute $\alg{Fixup-Base}(W,\pc)$.
137 TODO define Fixup-Base
139 \subsubsection{Result}
141 If all of that was successful, let $\tipcn = W$.
143 \subsection{$\alg{Recreate-Base}(\pc)$}
149 Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
153 Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$
154 and set $W \iassign C$.
157 \condproof{Create Acyclic}{
158 by Tip Correct Contents of $L$,
159 $L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
160 Now $\pd \isdirdep \pc$,
161 so by Coherence, and setting $\pa E = \pc$,
162 $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK.
164 That's everything for Create Base.
169 Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
173 Declare that we contain all of the relevant information from the
174 sources. That is, use $\alg{Pseudo-Merge}$ with $L = W, \;
175 \set R = \{ W \} \cup \set S^{\pcn}$.
178 \condproof{Base Only}{ $\patchof{W} = \patchof{L} = \pn$. OK. }
180 \condproof{Unique Tips}{
181 Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
190 \subsubsection{$\alg{Recreate-Recurse}(\pd)$}
194 \item Is $W \haspatch \pd$ ? If so, there is nothing to do: return.
196 \item TODO what about non-Topbloke base branches
198 \item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
199 execute $\alg{Recreate-Recurse}(\pd')$.
201 \item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
202 (Recreate Base Dependency Base Declaration.)
204 \item Use $\alg{Merge}$ to apply $\pd$ to $W$. That is,
205 $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
211 \subsection{$\alg{Merge-Tip}(\pc)$}
215 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
217 \item $\alg{Merge}$ from $\tipcn$. That is, $L = W, \;
218 R = \tipcn$ and $M = \baseof{W}$.
221 \condproof{Ingredients}{
222 $M \le L$ is trivial. For $M \le R$ we want
223 $\tipcn \ge \baseof{W}$.
224 Well $W \in \set S^{\pcy}$ so $W \in \allreachof{\pcn}$
225 and $W \in \pcy$. So $W \in \pendsof{\allreachof{\pcn}}{\pcy}$
226 so Base Covers Reachable indeed
227 $\tipcn \ge \baseof{W}$.
229 \condproof{Tip Merge}{ Trivial. }
230 \condproof{Merge Acyclic}{
231 By Base Acyclic, $\tipcn \nothaspatch \p$.
233 \condproof{Foreign Merges}{ Not applicable. }
237 Afterwards, $\baseof{W} = \tipcn$.
240 \item For each source $S \in \set S^{\pcy}$,
241 $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
244 In fact, we do this backwards: $L = S$, $R = W$.
246 the resulting $C \in \pcy$ and the remaining properties of the Merge
247 commit construction are symmetrical in $L$ and $R$ so this is fine.
249 By the results of Tip Base Merge, $\baseof{W} = \tipcn$.
251 By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e.
252 $\baseof{R} \ge \baseof{L}$.
254 Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in
255 which case $M = \baseof{S}$ will suffice.