From 8acb4aba1948cee65c773e1d0c199e190dc4837f Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Wed, 8 Feb 2012 18:41:58 +0000 Subject: [PATCH] wip theory --- THEORY | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 THEORY diff --git a/THEORY b/THEORY new file mode 100644 index 0000000..e908c68 --- /dev/null +++ b/THEORY @@ -0,0 +1,56 @@ +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 ] D + C ] D => C > D + +patches + patch P is two subset of commits, Ptip and Pbase + each subset has a single ur-ancestor C0_Ptip resp C0_Pbase + these subsets mutually exclusive + P(C) is either Ptip, Pbase, or nil (recorded in commit) + +commits fall into three categories wrt P + how(P,C) = included + P included in C + \forall D \elem Ptip, C ] D <=> C > D + how(P,C) = absent + P absent from C + \forall D \elem Ptip, !(C ] D) + how(P,C) = removed + P removed from C + \exists E s.t. + \forall D \elem Ptip, + something + +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 + +cleanness of patch + if P(C) = Ptip + B \elem E(C,Pbase) + then + C ] Cx ^ B !] Cx => P + +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) + +anticommit + make C from D, P, A-, A+ + where + A+ < A- < D + E(D,Ptip) = { A- } + E(D,Pbase) = { A+ } + result + C < { D } + P(C) = P(D) + -- 2.1.4