[darcs-users] How conflictors work

Ian Lynagh igloo at earth.li
Thu May 29 12:09:34 UTC 2008


On Mon, May 19, 2008 at 08:11:41PM +0100, Ian Lynagh wrote:
> On Mon, May 19, 2008 at 11:48:16AM -0400, David Roundy wrote:
> 
> > Maybe it would make sense to try to implement your merge algorithm
> > before attempting to prove it correct? I would be highly surprised if
> > you were able to prove it correct, and a quick run through unit should
> > be able to prove it incorrect.  Or perhaps the typechecker would
> > succeed at that?
> 
> That sounds like a good idea.

You meant the Darcs/Patch/Unit.lhs tests, right?

Attached is a patch that changes the Conflictor constructor from
    [Non RealPatch x] -> FL Prim x y -> Non RealPatch x -> RealPatch y x
to
    [Non Prim      x] -> FL Prim x y -> Non Prim      x -> RealPatch y x
(and InvConflictor likewise), and updates the rest of the code
mechanically, with no intelligence applied. All the tests pass, except
for four where we hit an exception:

Testing real merge output consistent... exception: Commute Prim merge
Testing real merge either way... exception: Commute Prim merge
Testing real merge and commute... exception: Commute Prim merge
Testing real partial permutivity... exception: Commute Prim merge

I'm still optimistic - I haven't looked to see exactly what the code is
doing here, but I think it ought to be possible to rewrite the code in
such a way that it doesn't try to merge contexts and assume that it will
succeed (which I assume is what's going on here).

Complete output is below in case I missed something.

By the way, you might want to apply some of the accompanying patches to
the main repo.


Thanks
Ian


Testing prim join inverses... passed.
Checking prim join inverses using QuickCheck... +++ OK, passed 100 tests.
Testing prim inverse doesn't commute... passed.
Testing join commute... passed.
Checking prim join commute using QuickCheck... +++ OK, passed 100 tests.
Testing prim recommute... passed.
Testing prim patch and inverse commute... passed.
Testing prim inverses commute... passed.
Testing FL prim recommute... passed.
Testing FL prim patch and inverse commute... passed.
Testing FL prim inverses commute... passed.
Testing fails... passed.
Testing read and show work on Prim... passed.
Testing read and show work on RealPatch... passed.
Checking that readPatch and showPatch work on RealPatch... +++ OK, passed 100 te
sts.
Checking that readPatch and showPatch work on FL RealPatch... +++ OK, passed 100
 tests.
Testing example flattenings work... passed.
Checking that tree flattenings are consistent... +++ OK, passed 100 tests.
Checking with quickcheck that real patches are consistent... +++ OK, passed 100 
tests.
Testing real merge input consistent... passed.
Testing real merge input is forward... passed.
Testing real merge output is forward... passed.
Testing real merge output consistent... exception: Commute Prim merge
Testing real merge either way... exception: Commute Prim merge
Testing real merge and commute... exception: Commute Prim merge
Testing real recommute... passed.
Testing real inverses commute... passed.
Testing real permutivity... passed.
Testing real partial permutivity... exception: Commute Prim merge
Checking we can do merges using QuickCheck... +++ OK, passed 100 tests.
Checking again we can do merges using QuickCheck... +++ OK, passed 1000 tests.
Checking recommute using QuickCheck Tree generator... +++ OK, passed 100 tests.
Checking recommute using QuickCheck TWFP generator... +++ OK, passed 100 tests.
Checking nontrivial recommute... +++ OK, passed 100 tests.
Checking nontrivial recommute using TWFP... +++ OK, passed 100 tests.
Checking inverses commute using QuickCheck Tree generator... +++ OK, passed 100 
tests.
Checking inverses commute using QuickCheck TWFP generator... +++ OK, passed 100 
tests.
Checking nontrivial inverses commute... +++ OK, passed 100 tests.
Checking nontrivial inverses commute using TWFP... +++ OK, passed 100 tests.
Checking merge either way using QuickCheck TWFP generator... +++ OK, passed 100 
tests.
Checking merge either way using QuickCheck Tree generator... +++ OK, passed 100 
tests.
Checking nontrivial merge either way... +++ OK, passed 100 tests.
Checking nontrivial merge either way using TWFP... +++ OK, passed 100 tests.
Checking permutivity... +++ OK, passed 100 tests.
Checking partial permutivity... +++ OK, passed 100 tests.
Checking nontrivial permutivity... +++ OK, passed 100 tests. 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: partialPrimContexts.patch
Type: text/x-diff
Size: 34512 bytes
Desc: not available
Url : http://lists.osuosl.org/pipermail/darcs-users/attachments/20080529/f1f52aaa/attachment-0001.bin 


More information about the darcs-users mailing list