Hi, Jean-Phillipe: I thought you might be interested in this discussion and the paper that sparked it
The paper is /A formalization of Darcs patch theory using inverse semigroups/ by Judah Jacobson http://www.math.ucla.edu/~jjacobson/patch-theory/ As for the underlying discussion, I'm adding you because I vaguely remember GUIDs being thrown around in the Henderson's cafe (Edinburgh Haskell Hackathon) If it's too hard to follow the below, please have a look at http://lists.osuosl.org/pipermail/darcs-users/2009-October/021970.html Now... Eric worried: >> So, one of things I thought was attractive about Darcs patch theory is >> that it seems to be completely independent of the patch types. >> >> You define patch types, inverse and commutation and the theory takes >> care of the rest (cherry picking, merging, conflicts). On Fri, Oct 30, 2009 at 16:20:52 +0100, Heinrich Apfelmus replied: > Well, patch theory would take care of the rest if it were as mature as > we'd like to. :-) :-) > What I'm saying is that, in my opinion, GUIDs make building a mature > theory much easier because they eliminate commutation altogether. > > (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 http://www.cse.chalmers.se/~bernardy/focal_Code_Anders_Petter.tar.gz Jean-Phillipe : perhaps it would be useful to put up a Darcs repository for that, for example, on patch-tag.com > 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. Now that you put it that way, consider me reassured! Not that I should have anything to say about what goes into a patch theory. >> Right now the kinds of primitive patch Darcs knows about: >> >> - hunks (the most obvious) >> - add A, remove A, adddir D, rmdir D (book-keeping, perhaps) >> - move A B > > The "Principled Approach to Version Control"[1] shows that GUIDs can do > these. > > [1]: http://www.cse.chalmers.se/~wouter/Publications/ > PrincipledVersionControl.pdf >> - replace tok1 tok2 (not everybody likes this) > > Not sure about this one, but I think some weaker form can be done with > GUIDs as well, for example by lexing the whole file and giving every > token a unique GUID. > >> Some things people have asked for: >> >> - char hunks > > Every char gets its own GUID... > >> - hunk movement >> - some kind of tree structure editing > > 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.) Hunk move patches are just the idea of displacing a block of text within a file or maybe even to some other file. But it sounds like this could be done in such a scheme, and perhaps made simpler? Ganesh was commenting that it's got tons of cases to consider. Tree structure editing: I don't know, but there have been people asking about using Darcs to edit XML files. So I imagine that operations like "add a child node here; move this node there; delete this node" could be interesting. I'm still hoping that someday in the future we'll see some interesting specialised Darcs-like tools for doing some notion of versioning/merging/etc on wacky data, which was why I asked about patch agnosticism. 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). Would it be straightforward to have such tracking in a commute-free patch theory? I imagine that along with conflict marking this would become a mere user interface issue more than anything else. Maybe this would even make it easy to implement the "breakable dependencies" that some people keep asking for. (then again, in a commutation-based scheme, I guess breaking dependencies would just be creating a conflict and no more difficult). 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), 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. Is that a close approximation of the truth? Is there a deeper story behind this? Thanks! Eric PS. As you can see, I don't even understand half of the discussion here, but I hope I'm at least plugging the right people together... -- Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow> PGP Key ID: 08AC04F9
signature.asc
Description: Digital signature
_______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
