Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-03-29

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
11:10 arjanb joined #darcs-theory
11:38 gal_bolle joined #darcs-theory
16:52 gal_bolle joined #darcs-theory
16:53 gal_bolle joined #darcs-theory
17:27 gal_bolle igloo: i can't get your coq to compile
17:30 Igloo gal_bolle: Hmm, with an up-to-date copy of my repo?
17:35 gal_bolle yes I think so
17:35 gal_bolle yes
17:35 Igloo gal_bolle: What error do you get, and with which file?
17:35 gal_bolle it's my fau
17:35 gal_bolle my fault sorry
17:36 gal_bolle i did not respect the order of the loads
17:36 Igloo Doesn't it do that itself?
17:37 gal_bolle hmm
17:37 Igloo I just load the file I'm interested in in coqide, and it takes care of it, anyway. Maybe proof general is different
17:37 gal_bolle unnamed_patches gets duplicated with the Load patch_sequences.v on top of foo.v
17:37 gal_bolle i don't really know
17:37 gal_bolle i don't use load
17:37 gal_bolle Require is cleaner in my understanding
17:38 Igloo I think require was loading .vo files rather than .v files
17:38 gal_bolle it's ok
17:38 gal_bolle but i think Load is Require Export
17:39 gal_bolle whereas Require Import is more often what you want
17:39 gal_bolle but my experience with such things is low
17:39 gal_bolle ok, so your commute_relate is my shuffle
17:39 gal_bolle stated differently
17:40 Igloo Require Import "patch_sequences.v".  says "Error: Can't find file patch_sequences.v.vo on loadpath"
17:40 gal_bolle Require Import patch_sequences.
17:40 gal_bolle and yes, you need to have a .vo
17:41 gal_bolle so that means changing your Makefile
17:41 Igloo OK. Well, it also means changing how I work
17:41 gal_bolle yes, so not worth the bother
17:41 gal_bolle I was just surprised
17:41 Igloo I'd need to run "make" before opening something in coqide to be sure I'm using the code I think I am
17:41 Igloo It's already a pain having to restart coqide when I change a dep
17:42 Igloo Anyway, commute_relates == shuffle, yes
17:42 gal_bolle ok
17:42 gal_bolle and commuteOutLeft q r s says "I can take some patch with the same name as r at the head of q, and I get r:>s"
17:43 Igloo commute_relates + swap, actually, I think
17:43 gal_bolle yes, of course, commute_relates alone does not make sense
17:43 Igloo r is the actual patch that you get out, not just one with the same name, but yes
17:44 gal_bolle yes, that's what I tried to formulate
17:44 gal_bolle i think it would be good style in coq to make a distinction between variables which are sequences and those which are patches
17:45 Igloo Do you mean "ps" vs "p"?
17:45 * Igloo is also hideously inconsistent with capitals
18:08 gal_bolle joined #darcs-theory
18:15 gal_bolle left #darcs-theory
18:15 gal_bolle joined #darcs-theory
18:15 gal_bolle Igloo: back
18:16 gal_bolle i think you need marked sequences in order to prove your lemma
18:16 gal_bolle s/need/probably want/
18:16 Igloo gal_bolle: Marked in what way? Have a list of names with them?
18:17 gal_bolle as in either that or more or less my shuffle_marked1
18:17 gal_bolle your commuteOutLeft is a subcase of my shuffle_marked1
18:18 gal_bolle commuteOutLeft r s1 s2 is equivalent to:
18:18 gal_bolle commuteOutLeft r (s1+>r':>s2) s3 is equivalent to:
18:18 Igloo I'll look at your code in more detail later
18:19 gal_bolle s1#>r'>#s2 =~~= NilFL#>r>#s3
18:19 Igloo But yeah, I'm not sure about details like exposing the names in sequences differently, or giving sequences a nat containing their length, etc, will be helpful or a hinderance
18:19 gal_bolle you're constraining one of the arguments to be NilFL
18:20 gal_bolle (ie, you only consider the case where you pull to the end)
18:20 gal_bolle but i think you need an induction on all the places you can pull to in order to conclude
18:20 gal_bolle if you go to the Admitted. in foo.v, there you need to do something with n
18:21 gal_bolle if it's 0 it's ok, you can conclude by commuteOutLeftSwap
18:22 gal_bolle but in the other case, there's a step of commute which you need to do, but which I don't know how to express with the NilFL constraint
18:23 gal_bolle maybe I'm confused and induction n with a suitably generalized goal works
18:24 Igloo *nod*, thanks for the ideas. I'll see what I can make of it
18:45 gal_bolle i think you have a problem in commuteOutLeft[Swap]
18:46 gal_bolle in the commuteOutLeftSwap constructor
18:46 gal_bolle s' is not constrained
18:46 gal_bolle there's probably not enough information in that predicate
18:49 Igloo Oh, yes. I think   s' = Cons p' s   or something
18:50 gal_bolle k
18:50 Igloo thanks!
18:51 gal_bolle i caught that by adding Implicit Arguments commuteOutLeftSwap.
18:51 gal_bolle Then Print commuteOutLeft.
18:51 gal_bolle s' did not get implicited
18:51 gal_bolle which was not normal
18:52 Igloo Ah, cunning
18:55 gal_bolle i'm a bit lost in that proof
18:57 gal_bolle i'm not sure if you should start with induction H or H0
18:59 Igloo I think it needs a subproof that   commuteOutLeft p q r /\ commuteOutLeft p q r' -> r = r' or something
18:59 Igloo Anyway, I didn't expect you to start trying to prove it. I was just letting you know where I was  :-)
19:01 gal_bolle yes, you probably need that
19:01 gal_bolle i'm proving these kinds of lemma for shuffles myself
19:01 gal_bolle so we're at the same point
19:01 gal_bolle still, I'm worried about how you plan to tackle the axiomatisation of sensible sequences
19:02 Igloo You mean how I plan to do the contexts?
19:02 gal_bolle i'm not sure if that's it
19:02 Igloo I think I'll put an abstract context type on unnamed patches
19:02 gal_bolle ok
19:03 * Igloo isn't thinking about that ATM, though
19:03 gal_bolle it's reassuring to see your code slowly converging to a cleaner version of mine ;-)
19:05 gal_bolle btw, i think that sensibility is underspecified in the paper
19:05 gal_bolle section 12.1
19:06 gal_bolle Explanation
19:06 gal_bolle What we’re saying here is that if we have two repos that differ in only their last patch then
19:06 gal_bolle we can always merge them. The two (equal up to commutation) results of the repo merge
19:06 gal_bolle are cde
19:06 gal_bolle
19:06 gal_bolle and ced
19:06 gal_bolle
19:06 gal_bolle .
19:06 gal_bolle this is a problem: we don't prove that we do that sensibly
19:13 Igloo There might be a theorem missing, but it is true
19:14 * Igloo is mostly away, sorry
19:14 gal_bolle I don't doubt it's true
19:14 gal_bolle i just think there's also a definition missing
19:17 gal_bolle we don't have an axiom that says : if spp^q is sensible, then so is sq ?
19:19 Igloo I don't think you can make both of those sequences unless p^ and q commute
19:20 gal_bolle hmm
19:21 gal_bolle sorry, it's if sp and sq are sensible, so is spp^q
19:21 gal_bolle (assuming p and q are not equal or inverts)
19:22 gal_bolle (with unnamed abstract contexts, this says that if p: Patch a b, then p^: Patch b a)
19:22 Igloo Ah, yes, OK, I think you are right
19:23 gal_bolle you may also want if s and s' are sensible, so is ss'
19:24 Igloo That's not true
19:24 gal_bolle sp and ps'
19:24 gal_bolle so is sps'
19:24 Igloo addfile "x"; addfile "x" isn't sensible, but the two subsequences are
19:24 gal_bolle (p is a patch, s and s' are sequences)
19:24 * arjanb is wary of adding axioms containing patches and their inverses
19:25 gal_bolle why?
19:25 gal_bolle this one really is the definition of the inverse
19:25 gal_bolle if you don't have it, then the inverse is any arbitrary patch
19:26 gal_bolle (as i said, it just says that if p goes from a to b, then p^ goes from b to a)
19:27 arjanb it's very easy to get to the point of the old conflictors where arbitrarily commutation is needed
19:28 gal_bolle i'm not convinced that arbitrary commute is not the solution (JP Bernardy's solution)
19:28 Heffalump I never quite understood his representation of them
19:29 gal_bolle his patch types, or what happens when you force commutation?
19:29 Heffalump the latter
19:29 Heffalump I should read that paper again
19:29 gal_bolle you get conflict markers (poor ones at the moment, afaik)
19:30 Heffalump but how does he guarantee the same result after different orderings?
19:30 gal_bolle the markers won't be the same
19:31 Heffalump that's no good, though
19:31 gal_bolle but the internal representation will
19:31 Heffalump oh, right
19:31 gal_bolle (same as in darcs, i think)
19:32 gal_bolle although in more cases
19:32 gal_bolle in the case of failed dependencies in addition to conflicts
19:32 gal_bolle and duplicated patches too
19:33 gal_bolle but there's no reason you can't add a dependency layer on top of that
19:37 * Heffalump is re-reading their paper and can't actually find any detail of this
19:37 gal_bolle the last line is my idea
19:37 Heffalump IM of the conflict representation at all
19:37 Heffalump I think there was a bit more in the emails but not much
19:38 gal_bolle can't remember
19:38 gal_bolle more than this, that is

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary