[darcs-devel] [patch1810] revert partitionRL to its former state, remove partiti...

Ben Franksen bugs at darcs.net
Fri Jun 14 17:40:30 UTC 2019


Ben Franksen <ben.franksen at online.de> added the comment:

> Fair enough. I guess ideally we'd have tests for the properties
> we actually want from this function so we can refactor with
> confidence.

These functions are underspecified but only with respect to (structural)
patch equality. Since we regard sequences that differ only in the order
of patches (via commutation) as equal, they are not /semantically/
underspecified (I think). We could add tests that the functions respect
the specification but that would be of no use in this particular case as
the two versions of partitionRL are (I think) semantically equivalent.

The problem is that some of our theories (V1 and V2) are incorrect in
that the order in which patches in a sequence are commuted may influence
whether later commutations in the same sequence succeed or fail, which
means commutation can distinguish between semantically equal sequences.

The properties we "want" (rather: are enforced to require due to bugs in
our previous theories) are, I think, pretty hard to specify abstractly.
It's basically "this version works (mostly)" vs. "this one more often
leads to failures". Sad but true.

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/patch1810>
__________________________________


More information about the darcs-devel mailing list