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

[Ganesh Sittampalam]

Hi,

On 24/05/2021 11:18, Ben Franksen wrote:
> Am 23.05.21 um 22:33 schrieb Ganesh Sittampalam:
>> On 23/05/2021 13:43, Ben Franksen wrote:
>>> In the Prim.V1 world, we can associate ("recover") a unique identity for
>>> all tracked file system objects (files, directories) using the unique
>>> identity of the patch that adds them. More precisely, what uniquely
>>> identifies FS objects is the /prim patch identity/ i.e. the patch
>>> identity (hash of the meta data) plus the index of the prim patch inside
>>> the named patch at the point (i.e. in the context) where it was
>>> originally recorded.
>>
>> I think this is true, but it doesn't address the question of commute
>> behaviour. The most important thing we want to improve on from Prim.V1
>> is to not have conflicts (in the sense of things needing to be handled
>> at the RepoPatch level) between patches that cause name collisions.
> 
> I don't think this is true. What Prim.FileUUID gives us is that file
> system patches and content patches cannot conflict: you can change file
> content regardless of whether the object is manifest or not. Manifesting
> two different file objects at the same location conflicts in
> Prim.FileUUID exactly as adding two such objects does in Prim.V1.

I was being a bit vague to avoid talking about the specifics of
Prim.FileUUID as it currently is, as we are free to change that.

But regardless, my point is that you have shown above that the two patch
representations themselves are either equivalent or very closely so: you
can back out a unique ID for each filesystem object from Prim.V1. But
our current commute rules will reject commutes that FileUUID would
accept. So I'm not sure how the equivalence helps us, as once we change
commute rules we can change the types anyway.

> I agree that one doesn't depend on the other. What I mean is that if we
> have a clear separation between the file system layer and the content
> layer(s), we could re-imagine FileUUID as a replacement for (only) the
> former i.e. the file system patch layer. They'd both be parametric in
> the content layer(s) and we could mix and match the two layers just as
> we do now with RepoPatchV* and the prim patch types. This would make it
> much easier (or so I hope) to fully integrate FileUUID. It would also
> make proofs and property tests easier.

Agreed. That was definitely one of the goals of my refactoring.

> To make this work we have to abstract over File Object identifiers, so
> that we can refer to the source and target object w/o mentioning the
> concrete form they take (UUID for Prim.FileUUID, AnchoredPath for
> Prim.V1). This in turn could perhaps open the possibility of
> retro-fitting unique IDs for file objects (this is still a very rough idea).

I don't see why we need to abstract over File Object identifiers. The
content layer can be independent of those identifiers, for example as it
is in my refactoring: 'Name' only appears in FSTreePatchType and no lower.


> It idea also begs the question of whether/how we should adapt the
> ApplyState type for the sub-primitive layers or if we need a completely
> different API for "applying" such patches. Taking a clue from your
> clipboard idea, the ApplyState for file content patches of type
> "line-based text" should be just the content of a single file plus the
> clipboard content. We may also want to modularize the definition of the
> Tree type in conjunction with that of Prim.V1 patches.

Yes, one of the other TODOs for my modularisation was to see how Apply
can be decomposed.

> [BTW, and sorry for the unstructured stream of thought: if we regard the
> clipboard content as being either full with some data or empty, we could
> enforce useful invariants, like that it is always empty outside of a
> "complete" prim patch, or that some low-level operation expects it to be
> full or empty, even at the type level. I am not sure if this is what you
> wanted to do and gave up on.]

Yes, that's what I tried. I found it hard because commuting two moves
gives you two clipboards to keep track of, and in theory if you view
cut/paste patches as obeying patch theory laws independent of the moves
they are part of, then you need to support an unbounded number of
clipboards. I had a way of counting the number of clipboards but the
arithmetic proofs required got too ugly and I gave up for now. I might
come back to it later.

Ganesh