# IRC log for #darcs-theory, 2008-12-23

All times shown according to UTC.

Time Nick Message
14:06 Igloo Heffalump: It follows from   pq <-> q'p' => q'^p <-> p'q^
14:07 Igloo (I might have that wrong, but the one that says you can rotate the commute square by 90 degrees)
15:11 Heffalump oh, cos you can keep rotating?
15:28 Igloo Yup
15:29 Heffalump ta
15:29 Heffalump how is the coq-ing going?
15:32 Igloo gal_bolle's the one who's been working on it, not me. He's put what he has so far in the theory repo
15:32 Heffalump I thought you might have some idea of what it could/couldn't do since it is in the repo.
15:44 Igloo I've skimmed it. It's only for the basic properties of primitive patches ATM, I think
15:45 * Heffalump is making a reasonable amount of progress trying to semi-automatically derive commute conditions for primitive patches
15:47 Igloo Cool
15:48 Heffalump I'm more confident that you can commute touching hunk patches if one of the two has non-empty old and new bits.
15:48 Heffalump and I'm working my way towards figuring out hunk moves (which are really quite fiddly)
15:51 Igloo They don't commute in the same way as a sequence of 2 hunk changes?
15:52 Heffalump if they did they'd be no use
15:53 Heffalump since then they'd be just like a sequence of 2 hunk changes :-)
15:53 Igloo Oh, and also commute with hunks entirely inside the moving hunk
15:53 Heffalump right
15:54 Heffalump what you do when things touch is the tricky bit
15:54 Igloo Oh, I see
15:54 Igloo Because removing the end of a moving hunk, and removing the thing just aftr the moving hunk, look the same when you invert them
15:55 Heffalump yeah
15:55 Heffalump but there's an asymmetry (because hunk /= move) that means that we could choose to always pick one, rather than just banning that case
15:56 Heffalump I'm modelling things in terms of a clipboard and using "cut" and "paste" patches rather than "move" patches so I don't have to deal with both ends at once
15:56 Heffalump another tricky thing is what to do when you remove the entirety of a moving hunk
15:56 Heffalump you have to decide whether to ban empty moves or not
15:56 Igloo I don't think you can just pick one
15:57 Igloo Because then commuting one way, then back again, wouldn't be the identity for the case you didn't pick
15:57 Heffalump ah, perhaps
15:58 Heffalump I haven't got enough infrastructure to test the laws on non-symmetric patch combinations yet.
15:58 Heffalump simplifying boolean expressions is a real nightmare
15:58 thorkilnaur joined #darcs-theory
15:58 Igloo Did you find a useful library?
15:59 Heffalump I took a bit of a look at the one someone suggested but it looked too complicated to be worth the effort.
15:59 Heffalump So no, I've just been rolling my own set of rules.
15:59 Igloo *nod*
16:10 Heffalump another interesting question - should completely empty hunk patches be banned
16:14 Igloo Probably not, in the theory, unless it causes problems
16:16 Heffalump it makes verifying some of the laws a bit harder, because it's a case where ambiguity is actually ok because it produces the same result
16:17 Igloo Ah, I see
16:17 Igloo I'd ban them then
16:17 Heffalump ah, but doing that makes verifying other laws harder cos you end up with nasty piles of disjuncts :-)
16:17 Igloo Although banning empty moves is harder, because reasonable commutes can create them
16:18 Heffalump and yes, that too
16:18 * Igloo needs to AFK
16:18 Heffalump but if you don't ban empty moves you get complicated conditions
18:00 arjanb joined #darcs-theory