chiark / gitweb /
strategy: wip proofs
[topbloke-formulae.git] / trav-alg.tex
1 \section{Traversal phase --- algorithm}
2
3 (In general, unless stated otherwise below, when we generate a new
4 commit $C$ using one of the commit kind algorith, 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
7 $W \assign R$.)
8
9
10 For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
11 lowest first:
12
13 \begin{enumerate}
14
15 \item Optionally, attempt
16  $\alg{Merge-Base}(\pc)$.  This may or may not succeed.
17
18 \item If this didn't succeed, or was not attempted, execute
19  $\alg{Recreate-Base}(\pc)$.
20
21 \item Then in any case, execute
22  $\alg{Merge-Tip}(\pc)$.
23
24 \end{enumerate}
25
26 After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
27 such that:
28
29 \statement{Correct Base}{
30   \baseof{\tipcy} = \tipcn
31 }
32 \statement{Base Ends Supreme}{
33   \tipcn \ge \pendsof{\allsrcs}{\pcn}
34 }
35 \statement{Tip Ends Supreme}{
36   \tipcy \ge \pendsof{\allsrcs}{\pcy}
37 }
38
39 \subsection{$\alg{Merge-Base}(\pc)$}
40
41 This algorithm attempts to construct a suitably updated version of the
42 base branch $\pcn$ using some existing version of $\pcn$ as a starting
43 point.
44
45 It should be executed noninteractively.  Specifically, if any step
46 fails with a merge conflict, the whole thing should be abandoned.
47 This avoids asking the user to resolve confusing conflicts.  It also
48 avoids asking the user to pointlessly resolve conflicts in situations
49 where we will later discover that $\alg{Merge-Base}$ wasn't feasible
50 after all.
51
52 If $\pc$ has only one direct dependency, this algorithm should not be
53 used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
54 to generate a perfect answer, whereas this algorithm might involve
55 merges and therefore might not produce a perfect answer if the
56 situation is complicated.
57
58 Initially, set $W \iassign W^{\pcn}$.
59
60 \subsubsection{Bases and sources}
61
62 In some order, perhaps interleaving the two kinds of merge:
63
64 \begin{enumerate}
65
66 \item For each $\pd \isdirdep \pc$, find a merge base
67 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
68 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
69 (Dependency Merge.)
70
71 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
72 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
73 (Base Sibling Merge.)
74
75 \end{enumerate}
76
77 \subsubsection{Fixup}
78
79 Execute $\alg{Fixup-Base}(W,\pc)$.
80
81
82 \subsection{$\alg{Recreate-Base}(\pc)$}
83
84 \begin{enumerate}
85
86 \item
87
88 Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
89
90 \item
91
92 Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$
93 and set $W \iassign C$.  (Recreate Base Beginning.)
94
95 \item
96
97 Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
98
99 \item
100
101 Declare that we contain all of the relevant information from the
102 sources.  That is, use $\alg{Pseudo-merge}$ with $L = W, \;
103 \set R = \{ W \} \cup \set S^{\pcn}$.
104 (Recreate Base Final Declaration.)
105
106 \end{enumerate}
107
108 \subsubsection{$\alg{Recreate-Recurse}(\pd)$}
109
110 \begin{enumerate}
111
112 \item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.
113
114 \item TODO what about non-Topbloke base branches
115
116 \item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
117 (Recreate Base Dependency Base Declaration.)
118
119 \item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
120 execute $\alg{Recreate-Recurse}(\pd')$.
121
122 \item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
123 $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
124 (Recreate Reapply.)
125
126 \end{enumerate}
127
128
129 \subsection{$\alg{Merge-Tip}(\pc)$}
130
131 \begin{enumerate}
132
133 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
134
135 \item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
136 R = \tipcn$ and choose any suitable $M$.  (Tip Base Merge.)
137
138 \item For each source $S \in \set S^{\pcy}$,
139 $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
140 (Tip Source Merge.)
141
142 \end{enumerate}
143
144