chiark
/
gitweb
/
~ian
/
topbloke.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
8acb4ab
)
wip theory
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 8 Feb 2012 21:36:30 +0000
(21:36 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 8 Feb 2012 21:36:30 +0000
(21:36 +0000)
THEORY
patch
|
blob
|
history
diff --git
a/THEORY
b/THEORY
index e908c6838a22c471af7d2a794739ea3a4de7254f..f5518b0e848d64b4eb95a948bed7fb83bb8498be 100644
(file)
--- a/
THEORY
+++ b/
THEORY
@@
-3,54
+3,85
@@
relations
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 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
patches
- patch P is two s
ubset
of commits, Ptip and Pbase
+ patch P is two s
ets Px
of commits, Ptip and Pbase
each subset has a single ur-ancestor C0_Ptip resp C0_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
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
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
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
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
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)
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
where
- A+ < A- < D
+ P(C) = Qbase
+ P(A-) = Ptip
+ inpatch(P,C) = included
E(D,Ptip) = { A- }
E(D,Ptip) = { A- }
+ then let
+ A+ = B(A-)
+ hence
+ A+ < A- < D
E(D,Pbase) = { A+ }
result
E(D,Pbase) = { A+ }
result
- C
<
{ D }
+ C
>1
{ D }
P(C) = P(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
+