X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke.git;a=blobdiff_plain;f=THEORY;h=4478fa064937a2b9a017b6526819a5a44efa50dc;hp=f5518b0e848d64b4eb95a948bed7fb83bb8498be;hb=8bbe58f296f2b26fa1457c5ed3337d66810a0fae;hpb=5ae399ddff45b6edb446ee5d9b779fb91985e439 diff --git a/THEORY b/THEORY index f5518b0..4478fa0 100644 --- a/THEORY +++ b/THEORY @@ -1,87 +1,151 @@ -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 + D \isin C 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) + Patch inclusion + C \haspatch P <=> [ \forall D \elem P+: D \isin C <=> D <= C ] + C \nothaspatch P <=> [ \forall D \elem P+: D \notisin C ] + +COMMIT ANNOTATIONS + + Commit C is annotated with: + + P(C) + Either P s.t. C \elem P + or _|_ meaning \notexists_{P} C \elem P. + + { Pi | C \haspatch Pi } + ie the set of included patches + + 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) = _|_, \forall_{Px} E(C,Px+) = { } + and this is also not annotated explicitly. + + B(C) + For C \elem P+: B s.t. E(C,P-) = { B } + P(C) = P- or _|_: _|_ + + Of these in principle all except P(C) can be recalculated from the + commit history, but that would involve a complete history scan and in + the case of \haspatch is clearly impractical. At some point we may + provide a checker/sanitiser that recalculates E(C,Px+) and B(C) from + the commit history. + +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(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+ + 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 + 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 + P(L) = Pl+ v P(L) = _|_ + 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 + 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