[darcs-users] If AB and B' are repos, does that imply A and B commute?

James Cook falsifian at falsifian.org
Sat Nov 21 19:45:06 UTC 2020


> Property:
> 
> (Summary: any sequence of patch names can be realized as a sequence of
> patches unless there's a specific conflict or violated dependency
> preventing it.)
> 
> Let N be the set of (positive) patch names and C(N) the set of finite
> subsets of N.
> 
> There exist:
> - a function "minimal_context" : N -> C(N);
> - a relation "conflict" on N x N; and
> - a universal starting context "empty_repo"
> such that the following properties hold. (Note that the above three
> objects are independent of any particular repository, so I'm asserting
> for example that minimal contexts are universal.)
> 
> 1. conflict is symmetric (conflict(a,b) implies conflict(b, a)).
> 
> 2. Consistency of minimal_context and conflict:
> 
>    For any names n1 and n2, at most one of the following is true:
> 
>    - n1 is in minimal_context(n2)
>    - n2 is in minimal_context(n1)
>    - conflict(n1, n2)
> 
> 3. Let n_1, n_2, ..., n_k be a sequence of distinct patch names
>    satisfying the following:
> 
>    - No patches in the sequence conflict: for all 1 <= i < j <= k,
>      conflict(n_i, n_j) is false.
>    - Dependencies are satisfied: for all 1 <= i <= k, every element of
>      minimal_context(n_i) appears somewhere before n_i in the sequence.
> 
>    Then there exists a (unique) patch sequence P_1 ... P_k with names
>    n_1 ... n_k which can be applied starting at empty_repo.

I should say two more things here:

- P1 ... Pk does not include any conflictors. This property is intended to be
  about a primitive patch theory where we haven't added in conflictors.

- The converse should also be asserted: if there are any conflicts or
  violated dependencies, then there is no sequence P1 ... Pk. Without
  this assertion, the property is trivially satisfied by saying all
  pairs of names conflict, i.e. "conflict" is the full product N x N.

-- 
James


More information about the darcs-users mailing list