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 ] D
- C ] D => C > D
+ 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 subset of commits, Ptip and Pbase
+ patch P is two sets Px of commits, Ptip and Pbase
each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
- these subsets mutually exclusive
+ 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
- how(P,C) = included
+ inpatch(P,C) = included
P included in C
- \forall D \elem Ptip, C ] D <=> C > D
- how(P,C) = absent
+ \forall D \elem Ptip, C has D <=> C > D
+ inpatch(P,C) = absent
P absent from C
- \forall D \elem Ptip, !(C ] D)
- how(P,C) = removed
+ \forall D \elem Ptip, !(C has D)
+ inpatch(P,C) = removed
P removed from C
- \exists E s.t.
- \forall D \elem Ptip,
- something
+ 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 ^ !\exists C s.t. C > Ce
+ 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 }
-cleanness of patch
- if P(C) = Ptip
- B \elem E(C,Pbase)
- then
- C ] Cx ^ B !] Cx => P
+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 [ C <=> Cx = D v Cx [ D
- how(P,C) = how(P,D)
+ Cx isin C <=> Cx = D v Cx isin D
+ inpatch(P,C) = inpatch(P,D)
-anticommit
- make C from D, P, A-, A+
+anticommit for removing a patch P from D to make C
+ make C from D, A-
where
- A+ < A- < D
+ 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 < { D }
+ C >1 { D }
P(C) = P(D)
-
+ inpatch(P,C) = removed
+
+single patch dependency application
+ make C from D, A+
+ 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
+