[darcs-devel] experiment: modular primitive patches and hunk move

[Ben Franksen]

Am 24.05.21 um 08:46 schrieb Ganesh Sittampalam:
> On 23/05/2021 13:01, Ben Franksen wrote:
>> Am 22.05.21 um 21:41 schrieb Ganesh Sittampalam:
>>> 1) Change path handling to work one level at a time. Either a patch is
>>> on the current filesystem object (a file/directory) or on a subdirectory
>>> of the current directory.
>>
>> What does "current" mean here? If this introduces additional state into
>> the operations then I am not sure I like the direction this goes. In any
>> case, I wonder how this is related to the next three ideas. See also
>> remarks further below regarding Prim.FileUUID.
> 
> No new state except some implicitly held in the recursive implementation
> of commute.
> 
> An actual patch exposed to the rest of the code is rooted at the
> top-level of the repository.

Ah, okay.

> If two patches operate on different filesystem entries at the current
> path, they commute trivially (bearing in mind that move is already split
> into cut/paste). If they operate on the same entry in the current
> directory, then we strip off that subdirectory and recursively try to
> commute them again, so the next commute down is implicitly "inside" that
> subdirectory.

I see. Could you explain the advantage of this scheme, compared to the
plain old check whether the two paths involved have a common prefix?

>> Making the prim patch representation and code more modular is something
>> I strongly support. The idea of splitting the prim operations into
>> smaller atomic parts sounds like a promising direction. I am not yet
>> convinced you have found the ideal way to do that. Is the copy/paste
>> idiom really the "right" abstraction?
> 
> No idea :-) But it was the only thing I could think of that would reduce
> the quadratic explosion in the number of cases when we have to consider
> interactions at both source and destination.

Fair enough. I guess /some/ sort of intermediate location is needed to
achive that.

>> I am also sceptical that types will help us improve this part, apart
>> from what we already do with witnesses. Formal proofs are certainly
>> nice, but I have serious doubts when it comes to things like permutivity
>> because of the exploding number of cases. IME testing QC properties has
>> the best balance between practicability (maintenance, flexibility) and
>> effectiveness (finding bugs).
> 
> I think we need to confront the fundamental weakness of the darcs model
> head-on here: if we make a mistake in defining commute rules it will
> live with us for a very long time. Hunk move is sufficiently complicated
> that I think it will take a lot of work to be very confident it's
> correct. I think we have various possible tools available, like testing,
> careful review, proof, more modular implementations that are easier to
> check, etc.

You make a very good point.

>> I think that a modularization effort for prim patches should take these
>> considerations into account. When I think about how this would interact
>> with hunkmove patches, it is clear that moving content from one file to
>> another can only be meaningful if both files belong to the same
>> "sub-primitive" theory. Taking another look at your repo, I see that you
>> are already doing something a long these lines (FSTreePatchType vs.
>> FsObjectPatchType). The concrete form that FSTreePatchType has doesn't
>> convince me, though, see above remark about your point (1).
> 
> Yes, I think more tweaking is needed. Part of the current structure is
> influenced by the need to be compatible with Darcs as it is now (I use
> pattern synonyms to map my types into the same structure as existing
> patches) which means treating directories a bit differently to files. I
> think ideally we'd have 'Directory', 'TextFile', 'BinaryFile' etc as
> three options for content at the same level, with the caveat that a
> 'Directory' still needs to refer to file patches so you can say things
> like "modify the text content of file x in directory y".

I think we should have a clear hierarchy instead of directory patches at
the same level as file content patches, because only then do we get
fully decoupled implemenations that we can reason about independently.

Cheers
Ben
-- 
I would rather have questions that cannot be answered, than answers that
cannot be questioned.  -- Richard Feynman