[darcs-users] How conflictors work
Ian Lynagh
igloo at earth.li
Sat May 17 13:45:19 UTC 2008
Hi David,
Thanks for your comments!
On Sat, May 17, 2008 at 04:18:21AM -0700, David Roundy wrote:
>
> First, as you know, I disagree with several of the statements in your "aside".
It could be that some of them turn out to be wrong, but I decided to
start with the simpler (IMO, at least) definition and see if anything
goes wrong when trying to prove things.
> In particular, it is necessary to define a distinct inverse-catch
> type. Your approach of just inverting and throwing in a bunch of
> context will fail. Most likely you made this mistake through failing
> to consider that the context in a "contexted patch" is not a sequence
> of patches, but rather a sequence of catches, and inverses when added
> to a context do not cancel one another out.
Oh, I'm not sure that I realised they were catches. I suspect I've been
inconsistent about what I consider them as.
Them being catches sounds bad, as conflictors can end up arbitrarily big
(deep).
But can it really not be a sequence of patches? If we want to add the
catch [Es, Z, P] to the context then does it not work to just add Es to
the context instead?
> i.e. the contexted patch pp^ : p is different from the contexted
> patch :p.
I don't see why that can't be simplified, even using a sequence of
catches. And you don't need to simplify it if you are using a sequence
of patches.
> It's highly inconvenient, but it's true. If you made them
> the same, you'd be unable to distinguish between distinct patches,
> i.e. the rule that two patches which have the same contexted value in
> the same context are the same patch would be violated.
What does it break? In the code, you only delete one of them if there
are two, so I think it would be fine.
(this is what I meant when I said Z should be a bag in section 5,
"Errors in this document").
> In definition 4.7 (merge), I don't see why you restrict yourself to
> the merging of conflicts where Esp and Esq are disjoint. It's trivial
> to construct an example where this isn't the case. e.g. consider the
> merge of three patches A, B and C that each modify the same line.
> First you construct AB' and AC', and then you merge B' and C', both of
> which have the same patch in their effect.
In that case that patch would be in Es_b (b for "both").
I should remove that line of English, actually, as it might be confusing
given it's also in the side condition of the equation.
(and "disjoint" is wrong; I actually mean that you can't commute them
such that Es_p = r Es_p', Es_q = r Es_q'. This is the "Es may have a
similar problem" bit in section 5)
> I think most of your conjectures 4.8 an4.9 are theorems if you define
> the merge to be such that
>
> p + q = <q', p'> implies that pq' <-> qp'
>
> so that then the properties of the commute define the properties of
> the merge.
But I have written down what the merge algorithm is, so I still need to
prove that the algorithm satisfies your property.
(the proofs are trivial for these, of course).
> However, your XXX comment in the merge definition should be all right:
> when the two effects are disjoint, they do not conflict.
Hmm, I'm not sure I follow. These are disjoint, but conflict:
[Line 3 -Foo +Bar] + [Line 3 -Foo + Wibble]
What we need to prove is that this can't happen (because these patches
would either be in Es_b, or only in the Z's, not the Es's.
> Regarding your concern whether Z should be a bag, not a set, that's
> why we treat identical patches as identical. This is what makes Z a
> set, since there can't be two distinct identical elements. The whole
> formalism is far more challenging if you allow distinct identical
> patches.
Hmm, OK. I don't think I agree at this stage, but perhaps I will once I
get deeper into it!
> I should also admit that when your paper got into dense mathematical
> notation (e.g. section 2), I tuned out, since I don't know this
> notation, and am insufficiently motivated to learn it at this
> juncture. I know that English is more verbose, but I prefer it.
Ah, sorry; can you clarify which bits you consider dense mathematical
notation, please? Is it me using
P \times P
to mean all values
<p, q>
where p and q are members of the set P? Or is it more than that?
Thanks
Ian
More information about the darcs-users
mailing list