From 3737625f8517dbb585defcc887b9db86e2e17228 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Wed, 22 Feb 2012 10:47:45 +0000 Subject: [PATCH] new THEORY, proved --- THEORY | 232 ++++++++++++++++++++++++++++++++------------------------- 1 file changed, 132 insertions(+), 100 deletions(-) diff --git a/THEORY b/THEORY index d0fdab5..5dd24c3 100644 --- a/THEORY +++ b/THEORY @@ -1,103 +1,135 @@ -relations - ancestry: of commits, a partial order - C > D C is a descendant of D - inclusion: commit includes change made in another - a partial order, consistent with ancestry but more partial - C has D <=> D isin C - C has D => C > D - -define convenience function - cont(C) := { Cx | Cx isin C } - -patches - patch P is two sets Px of commits, Ptip and Pbase - each subset has a single ur-ancestor C0_Ptip resp C0_Pbase - all these subsets Ptip,Qbase,Rtip,Sbase mutually exclusive - P(C) is either Ptip, Pbase, or nil (recorded in commit) - -commits fall into three categories wrt P - inpatch(P,C) = included - P included in C - \forall D \elem Ptip, C has D <=> C > D - inpatch(P,C) = absent - P absent from C - \forall D \elem Ptip, !(C has D) - inpatch(P,C) = removed - P removed from C - cont(C) \intersection Ptip = { } - but maybe \exists Cx \elem Ptip s.t. Cx < C - -the ends E(C,Px) of Px = Pbase or Ptip are - every maximal Ce < C in Px - ie every Ce for which - C > Ce and !\exists C s.t. C > Ce - -existence of corresponding base B for every tip commit C - \forall C s.t. P(C) = Ptip - \exists B s.t. E(C,Pbase) = { B } - resulting function B(C) - -contents of tip commits - \forall C s.t. P(c) = Ptip - cont(C) = cont(B(C)) \union { Cp s.t. P(Cp) = Ptip and Cp < C } - -non-circularity - \forall B s.t. P(c) = Pbase - cont(B) \notintersect Ptip - -normal commits - make C from D - result - C < { D } - P(C) = P(D) - Cx isin C <=> Cx = D v Cx isin D - inpatch(P,C) = inpatch(P,D) - -anticommit for removing a patch P from D to make C - make C from D, A- +GENERAL + + C >= D C is descendant of D, partial order + C \haspatch D C contains changes from D, partial order + Patch P has two sets P+, P- + Ancestors A(C,P) = { Ca \elem C | Ca \elem P } + Ends E(C,P) = maximal elements of A(C,P) + +COMMIT ANNOTATIONS + + Commit C is annotated with: + + P(C) + Either P s.t. C \elem P + or \bottom meaning \notexists_{P} C \elem P. + + For every Px, E(C,Px+) + Implicitly for C \elem Pc+, E(C,Pc+) = { C } + and this is not annotated explicitly. + Also implicitly for P(C) = \bottom, \forall_{Px} E(C,Px+) = { } + and this is also not annotated explicitly. + +SIMPLE COMMIT + + make C >1 { A } + from A + + with contents + D \isin C <=> D \isin A v D = C + + results + P(C) = P(A) + A \haspatch P <=> C \haspatch P + For A \notelem Px+: E(C,Px+) = E(A,Px+) + A \elem Px+: E(C,Px+) = { C } -- not annotated + +ANTICOMMIT + + make C >1 { L } + from L, R+, R- + + with contents + D \isin C <=> D \notelement Pr+ ^ D \isin L + + where + P(R+) = Pr+, P(R-) = Pr- + E(L,Pr+) = { R+ } -- nontrivial, may need R+' = merge of E(L,Pr+) + B(R+) = R- + L \haspatch Pr + + results + P(C) = P(L) = Pl- + If C \elem P+, B(C) = B(L); otherwise B(C) n/a + For P = Pr: C \nothaspatch Pr + E(C,Pr+) = E(L,Pr+) = { R+ } + P != Pr: C \haspatch P <=> L \haspatch P + E(C,P+) = E(L,P+) + +MERGE + + make C >1 { L, R } + from L, R, M + + with contents + D \isin C <=> [ (D \isin L ^ D \isin R) v D = C : T ] + [ D \notisin L ^ D \notisin R ^ D != C : F ] + [ otherwise : D \notisin M ] + where - P(C) = Qbase - P(A-) = Ptip - inpatch(P,C) = included - E(D,Ptip) = { A- } - then let - A+ = B(A-) - hence - A+ < A- < D - E(D,Pbase) = { A+ } - result - C >1 { D } - P(C) = P(D) - inpatch(P,C) = removed - -single patch dependency application - make C from D, A+ + M < L, M < R + If L \elem P+: + R \elem P+ ^ B(R) = B(L) -- only merge tips with same base + v R \elem P- ^ R >= B(L) ^ M = B(L) -- base when merging into tip + If L \elem P-: + R \nothaspatch P + If L \haspatch P <=/=> R \haspatch P: + \forall Ce \elem E(R,P+): Ce <= L -- may need to merge E(R,P+) into L + + results + P(C) = P(L) + B(C) = + For C \notelem P+: n/a + C \elem P+, R \elem P+: B(L) = B(R) + C \elem P+, R \notelem P+: R >= B(L) + + C \haspatch P = + For L \nothaspatch P, R \nothaspatch P: F + L \haspatch P, R \haspatch P: T + otherwise: M \nothaspatch P + E(C,P+) = maximal elements of E(L,P+) \union E(R,P+) + = { Cl | \notexist Cr \elem E(R,P+): Cr >= Cl } \union + { Cr | \notexist Cl \elem E(L,P+): Cl >= Cr } + + -- to reintroduce a dep, set P(C)=P(L)=Pl-, P(R)=Pr+, M=B(R) + where L \notelem Pr obv. + + +CREATE BASE + + make B >1 { L } + from L, P + where - P(C) = Qbase - P(A+) = Ptip - inpatch(P,C) != included - then let - A- = B(A+) - hence - A- < A+ - result - C >1 { D, A+ } => C > D, C > A+ > A- - P(C) = P(D) - inpatch(P,C) = included - -simple merge - make C from L, R, M + P(L) = Pl+ v P(L) = \bottom + P(L) != P(B) + E(B,P+) = { } + + with contents + D \isin B <=> D \isin L v D = B + + results + P(B) = Pb- + B(C) n/a + E(B,Px+) = E(L,Px+) + B \haspatch P <=> L \haspatch P + + +CREATE TIP + + make C >1 { B} + from B + where - M < L < C - M < R < C - result - C >1 { L, R } - P(C) = P(L) - if Cx isin L = Cx isin R, - Cx isin C = Cx isin L - otherwise - Cx isin C = ! Cx isin M - - cases of inpatch(P,L) and ,R - - or Cx isin + B \elem Pb- + E(B,P+) = { } + + with contents + D \isin C <=> D \isin B v D = C + + results + P(C) = Pb+ + B(C) = B + C \haspatch P = + For P != Pb: B \haspatch P + P = Pb: T -- 2.30.2