[Gnu-arch-users] Re: formal foundations for the semantics of restricted mkpatch

[Tom Lord]

    > From: Tom Lord <address@hidden>
    > The most important thing to prove is:

    > ----------------------------------------------------------------
    > * Prime Conjecture: selected mkpatch produces a sane changeset
    > 
    >   Given trees, ORIG and MOD, and limits, LIMITS:
    > 
    >   With:
    > 
    >           C := mkpatch_selected (ORIG, MOD, LIMITS)
    > 
    >   T := apply_changeset (C, ORIG)
    > 
    >   C2 := mkpatch (ORIG, T)
    > 
    >   Then:
    > 
    >         C = C2
    > ----------------------------------------------------------------


By the way, that's part of the difference in how we started to
implement mkpatch_selected.

Your idea is to compute a bunch of the intermediate sets used in
mkpatch, then prune those according to the LIMITS.   I suspect that
thinking of the problem in those terms makes it very hard to figure
out what T, in the conjecture, will be.

Conversely, if you _know_, trivially, what T will be, the conjecture
is hopefully a bit easier to show.

So my original idea for mkpatch_selected was to evaluate limits in
terms of the inventories.

mkpatch starts by computing two tree inventories, each of which is a
pair of bijective mappings between relative paths and inventory tags.

My thought was to evaluate limits against the MOD inventory, perhaps
looking at the ORIG inventory to figure out about deleted files.

The output of that evaluation would be a _third_ inventory for a
fictional tree T.   In subsequent computation, this third inventory
would take the place of the mod inventory.

In the code, given an inventory, mkpatch computes the real path to
that file by prepending the tree-root to the relative path.   I
thought we would change that so that the inventories were stored
(internally to mkpatch) as a triple:

        relative_path   id_tag  real_path


with the understanding that if the LIMITS mean a certain file should
not be regarded as changed in MOD (even though it might be changed on
disk) that the real_path for that file in the fictional T inventory
would point to the ORIG copy of the file.

Whenever mkpatch needs to operate on a file, it uses the real_path.
For example, comparison of an ORIG file to a MOD file that we are
pretending is not modified could be very fast: simply notice that the
same real_path is used for both.

This approach does require some proof that the fictional inventory for
a tree T is, in fact, a valid inventory for a valid tree.   However,
beyond that, the prime conjecture "falls out" for free -- since
we essentially have a case of `mkpatch_selected == mkpatch' (other
than the fictional inventory).

-t