From 889eb403a5fec0d4a2d22bd72dcb3c4789811fd2 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 29 Apr 2012 23:25:08 +0100 Subject: [PATCH] strategy: wip --- strategy.tex | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/strategy.tex b/strategy.tex index a3acc81..cec6388 100644 --- a/strategy.tex +++ b/strategy.tex @@ -130,16 +130,16 @@ it is, are we fast forward to $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 XXX FIXME IS THIS THE BEST THING? +commit set. We maintain $$ \bigforall_{\p \isdep \pc} - \pancsof{\tipcc}{\p} \subset \left[ - \tipfa \p \cup - \bigcup_{E \in \set E_{\pc}} \pancsof{E}{\p} - \right] + \pancsof{\tipcc}{\p} \subset + \pancsof{\tipfa \p}{\p} $$ +\proof{ + For $\tipcc = \tipzc$, $T$ ...WRONG WE NEED $\tipfa \p$ TO BE IN $\set E$ SOMEHOW +} \subsection{Merge Contributors for $\pcy$} @@ -147,16 +147,18 @@ 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. +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$. -For $p \neq \pc$, by Tip Contents, +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$. $\qed$ +By Tip Contents for $L$, $D \le L \equiv D \le M$. OK.~~$\qed$ WIP UP TO HERE @@ -167,6 +169,10 @@ $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$ -- 2.30.2