[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

[Jean-Philippe Bernardy]

Just to sum up my take on this:

>  http://www.math.ucla.edu/~jjacobson/patch-theory/

Disclaimer: I haven't read the paper. (yet)

>> What I'm saying is that, in my opinion, GUIDs make building a mature
>> theory much easier because they eliminate commutation altogether.

I support this statement.

An alternative that I may also support is the following: make
commutation a total operation. In other words, detection of conflicts
should be decoupled from commutation.

>> (My litmus test for maturity of a theory is that I can read it up
>> somewhere and implement my own toy darcs, just like I can implement my
>> own toy lambda calculus or my own toy type inference, for example.)
>
> Darcs-users: Speaking of toy implementations, here's a tarball for
> FoCAL, which I think you have seen but which I'm reposting because it
> seemed relevant

There is a notion of GUID in here, yes. GUIDs are relative to the
position in the tree where "stuff happens". So they are global across
all users of the repo, but not local to a "place" in the repo.

> Jean-Phillipe : perhaps it would be useful to put up a Darcs repository
> for that, for example, on patch-tag.com

Ok, I'll keep it in mind. Otherwise I wouldn't mind if anybody else would do it.

>> Being agnostic of patch types sounds great, but neither do I expect
>> GUIDs to be less agnostic, nor is Darcs patch theory as agnostic as it
>> may sound. The thing is that the commutation operation has to obey a lot
>> of rules ("patch laws"), some of which are collected in Judah's paper and
>> some of which are hitherto unknown, and if you introduce a new patch
>> type, it might just not be possible to make it obey the patch laws.

All good points.

>> Every char gets its own GUID...

As I try to point out, this is not as bad as it sounds, if you make GUID local.
To be more specific, the hunk gets a GUID. Each element in the Hunk
gets an implicit GUID: (GUID, index in the thunk). Hunks are attached
at a given
(GUID, index in the thunk).


>> What are these? But yes, there might be patch types that cannot be
>> formulated in terms of GUIDs. (Not sure whether this is a problem,
>> though.)

I would argue that if you can work out a total commutation function, then
there exists a GUID version.


> Now that you've tackled agnosticism, I have one more question for you,
> oh monorail salesman: what about dependencies?  I understand how Darcs
> figures out if one patch depends on another (they don't commute).

IMHO, this is the weakest point in darcs. (In case I wasn't clear
enough before :)


> Would
> it be straightforward to have such tracking in a commute-free patch
> theory?

Dependencies cannot be fully and automatically tracked by a VC system.
(Otherwise it could solve the halting problem...)

So, you have two possibilities:

1. Specify dependencies manually
2. Use something like delta-debugging to work out the dependencies,
(or just let users run the test suite after pulling / before applying!)

Still, I understand that VC can detect some (hints of) conflicts
early, and this is useful. A GUID-based system will just detect a
somewhat different set
of conflicts than other systems.

In "FoCAL" you can detect:

1. Hunk attached to missing parent
2. Text removed more than once
3. Other more subtle cases that I won't go into.

> Finally: are there any reasons to be GUID-skeptical?  If they really
> could give us a better way to think about patches, why do we continue
> the line of inquiry into commutation-based merging?  I imagine that one
> reason is that (a) because it's known to work (for the most part),

"For the most part": indeed. I think that most people are still wary of
of what happens in case of conflict.

> whereas the new scheme would open up whole new cans of worms
> and that
> (b) Ian really has pretty much worked it all out already and it's really
> just a matter of hammering out the proofs in Coq.

You should consider

* how many people are going to understand this enough to be able to
maintain it ?
* Will Coq proofs be a strong argument for people to regain trust in darcs?

I know that, even if they get completed, proofs won't convince me
until a number of people have gone through the theorems and understood
what
they mean. (ie. the proof might be correct, but prove useless statements)

Cheers,
JP.