[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
me at worldmaker.net
Thu Oct 29 16:06:54 UTC 2009
I'm probably similarly confused as Eric, if not more so... Excuse my
ignorance here, but I am interested in the practical repercussions of
these discussions even if I can't bring much to the table on the
> On Thu, Oct 29, 2009 at 14:50:48 +0100, Heinrich Apfelmus wrote:
>> In any case, I once again would like to stress that it is my belief that
>> commutation is already too complicated to be a suitable foundation for
>> understanding the semantics of merges.
>> In other words, thinking about the intricacies of commutation is a waste
>> of our precious brain cycles. :) They are better spent on a simpler
>> formalization where each line has its own GUID.
A GUID for each line? Is this primarily to make the proofs of darcs
theory better sync with OT (and/or other similar theories), or is this
also a practical concern?
That is, is the assertion here that darcs itself should use a GUID for
every single line? Wouldn't that be woefully inefficient?
From a purely layman's standpoint it seems to me that as intricate as
darcs commutation can get it appears to get the job done and that GUID's
are rarely the answer to anything (other than how do we embroil this
existing system with lots of rarely used cryptic strings).
I do see the practical use of Hashes/GUIDs for file naming as an
abstraction from file systems, but I can't see a GUID for every line of
source text requirement as a useful practical need for darcs. (I can
understand if it is a useful formalization to create a specific test
case, but largely if it is generally applicable to an understanding of
Eric Kow wrote:
> Some things people have asked for:
> - char hunks
> - hunk movement
> - some kind of tree structure editing
I'm still interested in playing more with token-stream based diffs
driving char hunks:
More information about the darcs-users