pseudomerge.tex

   1 \section{Pseudo-merge}
   2
   3 Given $L$ and some other commits $\set R$, generate a
   4 `fake merge': i.e., a commit which is a descendant of $L$ and $\set R$
   5 but whose contents are exactly those of $L$.
   6
   7 \gathbegin
   8  C \hasparents \{ L \} \cup \set R
   9 \gathnext
  10  \patchof{C} = \patchof{L}
  11 \gathnext
  12  D \isin C \equiv D \isin L \lor D = C
  13 \end{gather}
  14
  15 \subsection{Conditions}
  16
  17 \[ \eqn{ Base Only }{
  18  \patchof{L} \neq \py
  19 }\]
  20
  21 \[ \eqn{ Unique Tips }{
  22  C \haspatch \p \implies
  23   \bigexists_T
  24     \pendsof{C}{\py} = \{ T \}
  25 }\]
  26
  27 \[ \eqn{ Foreign Unaffected }{
  28  \bigforall_{ D \text{ s.t. } \isforeign{D} }
  29   \left[ \bigexists_{A \in \set A} D \le A \right]
  30    \implies
  31   D \le L
  32 }\]
  33  TODO THAT IS IMPOSSIBLE TO CALCULATE
  34
  35 \subsection{Lemma: Foreign Identical}
  36
  37 $\isforeign{D} \implies \big[ D \le C \equiv D \le L \big]$.
  38
  39 \proof{
  40 If $D \le L$, trivially $D \le C$; so conversely
  41 $D \not\le C \implies D \not\le L$.
  42 Whereas if $D \le C$, either $D \le L$ or
  43 $\exists{A \in \set A} D \le A$ (since $D \neq C$),
  44 in which case by Foreign Unaffected $D \le L$.
  45 }
  46
  47 \subsection{No Replay}
  48
  49 Ingredients Prevent Replay applies:
  50 $A = L$ always satisfies the $\exists$.  $\qed$
  51
  52 \subsection{Unique Base}
  53
  54 Not applicable, by Base Only.
  55
  56 \subsection{Tip Contents}
  57
  58 Not applicable, by Base Only.
  59
  60 \subsection{Base Acyclic}
  61
  62 Relevant only if $L \in \pn$.  For $D = C$, $D \in \pn$; OK.
  63 For $D \neq C$, OK by Base Acyclic for $L$. $\qed$
  64
  65 \subsection{Coherence and Patch Inclusion}
  66
  67 $$
  68 \begin{cases}
  69   L \haspatch    \p : & C \haspatch    \p \\
  70   L \nothaspatch \p : & C \nothaspatch \p
  71 \end{cases}
  72 $$
  73
  74 \proof{
  75 Consider some $D \in \py$.  $D \neq C$ by Base Only.
  76 So $C \has \p \equiv L \has \p$.
  77 }
  78
  79 \subsection{Unique Tips}
  80
  81 Explicitly dealt with by our Unique Tips condition.
  82
  83 \subsection{Foreign Inclusion}
  84
  85 True by Foreign Identical, and Foreign Inclusion of $L$.
  86
  87 \subsection{Foreign Contents}
  88
  89 Not applicable.