Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-04-17

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

All times shown according to UTC.

Time Nick Message
06:11 gal_bolle joined #darcs-theory
10:05 tux_rocker joined #darcs-theory
11:55 gal_bolle joined #darcs-theory
12:00 gal_bolle hi igloo
12:13 gal_bolle can you make me a sign when you're back
12:39 Igloo gal_bolle: Yo yo!
12:39 gal_bolle hi
12:39 gal_bolle saw you on #darcs
12:39 gal_bolle did you read my messages on darcs-users?
12:39 gal_bolle you're in utrecht?
12:43 Igloo In Utrecht, yes
12:43 Igloo I saw your mail but haven't read it properly yet
12:44 gal_bolle ok, are the city and hackaton nice?
12:44 Igloo Haven't seen the city, but the Hackathon is good  :-)
12:44 Igloo 49 people signed up!
12:44 gal_bolle good
12:46 gal_bolle is ee???? with you?
12:46 gal_bolle eelis
12:46 gal_bolle or is he participating through irc too?
12:47 Igloo No, he turned out to be busy
12:47 Igloo But swiert has fixed a couple of my silly problems for me
12:48 gal_bolle ok
12:49 * Igloo has just managed to fix my mail client so I can reply to your recent mail  :-)
12:49 Igloo something on my girlfriend's laptop doesn't like utf8
12:49 gal_bolle what's it running?
12:50 Igloo Windows/putty
12:52 gal_bolle that explains
12:53 Igloo :-)
13:19 mornfall You should be able to set encoding in putty config dialog to UTF-8. (It tends to be latin1 by default...)
13:19 mornfall Igloo: ^
13:23 Igloo Ah, ta
14:29 gal_bolle igloo: do you have a means of doing voip and whiteboarding and some time to do so somewhere between 17:00 and 23:00 ?
14:39 Igloo I highly doubt it
14:39 Igloo In fact, I'm sure not, as the uni people will have one home
14:39 gal_bolle ok, i'll be back online at around 17:00 i'll try to have a convincing point then
14:39 Igloo heh, OK
14:40 gal_bolle i don't get your reasoning about the uni people but anyway
15:32 gal_bolle joined #darcs-theory
15:37 Igloo gal_bolle: I have problems with modules
15:38 gal_bolle what kind of problems?
15:38 Igloo The term "up1" has type "UnnamedPatch" while it is expected to have type "patch_sequences.patch_sequences​.unnamed_patches.UnnamedPatch".
15:39 gal_bolle i think you need to add constraints somewhere
15:40 gal_bolle it's hard to tell, as i don't have your code in head, though
15:40 Igloo AIUI, the problem is that Load is making another copy of the datatype, that is distinct from the original
15:40 Igloo I could push my current state if that's useful
15:40 gal_bolle i think is advice is not to use load
15:41 gal_bolle why don't you import the other module?
15:41 gal_bolle (or make a functor with an import argument)?
15:41 Igloo Module Import gave me    Error: The reference NameSet.t was not found in the current environment.
15:41 Igloo and also means I need to build all the files IIRC
15:42 gal_bolle i don't know really
15:43 Igloo I think I'll make a tarball and mail the list
15:43 gal_bolle ok
15:43 gal_bolle which list?
15:44 Igloo coq-whateveritis
15:44 Igloo club
15:44 gal_bolle ok
15:45 gal_bolle that's the right thing to do
15:45 gal_bolle i think module import requires the module to be compiled
15:45 gal_bolle i don't think that coqide does that for you
15:46 Igloo I'd compiled it
15:47 gal_bolle then i'm not sure without looking at the code
16:13 gal_bolle igloo: do you have a little time?
16:15 gal_bolle after looking at both of our coqs, i think i see how to reconciliate them
16:22 Igloo gal_bolle: Yup
16:24 gal_bolle ok so the good news is that overlap between our respective works is minimal
16:24 gal_bolle so i'll try to describe my plan
16:25 gal_bolle first a question: if i wasn't there being a pain, what would you plan to do this week-end?
16:25 gal_bolle not in you personal life of course ;-)
16:25 Igloo I'd be working on the proofs regardless
16:25 Igloo Until I get stuck on all fronts, anyway
16:26 gal_bolle ok
16:26 gal_bolle i'd prefered if you had tell me you were going to hack on the implementation…
16:26 gal_bolle but it's a good thing that we're both motivated with this
16:27 gal_bolle do you plan to do paper-proofs or coq-proofs?
16:28 Igloo I'm only doing coq proofs now
16:28 gal_bolle ok
16:29 gal_bolle so first point of methodology: coq proofs are more akin to programs than to paper-proofs
16:29 gal_bolle hence we want fine-grained modules
16:30 gal_bolle and axioms are the interfaces between these modules
16:30 gal_bolle would you agree with that principle?
16:30 Igloo Why aren't lemmas the interfaces
16:31 gal_bolle what the producer module sees as a lemma, the consumer module sees as an axiom
16:32 gal_bolle axioms are the input of the module, and lemmas the output
16:32 Igloo But why doesn't the consumer import the producer to get the lemma?
16:33 Igloo Are you in Berline long-term, BTW?
16:33 gal_bolle isolation: you want to import the _type_ of the producer, not its guts
16:33 gal_bolle i'm in berlin until september/october
16:33 gal_bolle depending on where i go next year
16:34 Igloo I don't see why we don't just do an import, instead of rewriting lemmas as axioms
16:34 gal_bolle if you want to think of it in terms of type-classes, axioms are the class Toto = …
16:34 gal_bolle and lemmas are instance Titi Toto where
16:35 Igloo OK, I think that using axiom for that is very confusing, because it's not what axiom means to me
16:35 gal_bolle yes, it's a source of confusion
16:35 gal_bolle t
16:36 gal_bolle which i should have spotted sooner
16:36 gal_bolle so let's just say module parameter instead
16:37 Igloo OK
16:38 gal_bolle even if it doesn't exactly please the tongue
16:38 gal_bolle one minute
16:39 gal_bolle i'm back
16:40 gal_bolle my experience with coq is that it's especially useful to isolate modules as most tactics tend to break abstractions otherwise
16:40 gal_bolle and having an abstract parameter blocks them
16:41 gal_bolle that's what i think we'd gain by adding intermediary layers of axioms
16:41 Igloo parameters
16:41 gal_bolle yes parameters
16:42 Igloo OK
16:42 gal_bolle so we need some abstract module-types that define these sets of parameters
16:42 * Igloo cries at the mention of modules
16:42 gal_bolle ok, then let's just say interfaces
16:43 gal_bolle i'm going to try making it into a module hierarchy
16:43 Igloo I don't mean I don't like the term, I mean I don't like coq's module system  :-)
16:43 gal_bolle if it's impossible, it's not a tragedy
16:43 Igloo (or maybe I just don't understand it)
16:43 gal_bolle do you have experience with ocaml's
16:43 Igloo No
16:43 gal_bolle coq is a refined version of that
16:44 gal_bolle so the reasonable course of action is for you to continue your proof happily
16:44 gal_bolle for me to unite our codes into a nice set of modules
16:44 gal_bolle then let my united set of modules sync back with your (hopefully many :-) ) proofs
16:44 Igloo OK
16:45 Igloo My plan is to finish this proof if at all possible, and see if names give the problems that you fear
16:45 gal_bolle great!
16:45 gal_bolle ok
16:45 Igloo sets of names, that is
16:45 gal_bolle yup
16:45 Igloo And I also need to try to work out how to use Make instead of Raw
16:45 gal_bolle so one point is that i feel it would be nice to have an abstract interface over named patches
16:46 gal_bolle so that compute and simple see an opaque name function instead of deconstructing everything
16:47 Igloo OK, that might need some rejigging so that things using it don't need to extract the name
16:47 gal_bolle in your proofs it would stay as is
16:47 Igloo Or so they have another way to extract the name
16:47 Igloo i.e. a nameOf function
16:47 gal_bolle then i would use your proofs to instantiate that abstract type
16:47 gal_bolle yup
16:48 gal_bolle and i'd have a module PatchWithNames: NamedPatchInterface.
16:48 gal_bolle where I define nameOf to be the projection
16:48 gal_bolle is that clear?
16:49 gal_bolle if it's not, then i'll first do it then show you how it looks
16:49 Igloo I think it's clear
16:50 gal_bolle then i'd likewise like to have an abstraction layer for name freshness
16:50 gal_bolle for the same separation of concern reason
16:50 gal_bolle this means making name a certified function
16:50 gal_bolle name comparison
16:51 gal_bolle that is, having name p = name q -> something
16:51 gal_bolle and name p <> name q -> something_else
16:51 gal_bolle one possibility for something and something_else is to take minimal context
16:51 * Igloo would have to see that to see exactly what you're suggesting
16:52 gal_bolle ok, i'll do a first version, and we'll see
16:52 gal_bolle i think the biggest misunderstanding came from using the word axiom
16:52 gal_bolle which really is different in coq as on paper
16:53 Igloo Heh, OK  :-)
16:53 gal_bolle retrospectively, i understand why you were so reluctant at my tendancy to add axioms everywhere
16:54 gal_bolle so plan A is you do proofs, i do a nice module hierarchy and we see where we're at when the first of us is finished
16:55 Igloo Yup. And coq-club tells me how to make my modules work  :-)
16:55 gal_bolle btw, if you have time to look at  if
16:55 gal_bolle as p q bs <->* cs p' q' ds
16:55 gal_bolle then p and q commute iff p' and q' do.
16:55 gal_bolle i think it could be one of the example where the natural proof (yours) is not the easiest to explain to coq
16:56 gal_bolle ok, so laundry time for me
16:56 gal_bolle see you
16:58 Igloo See you
19:55 gal_bolle joined #darcs-theory
21:59 gal_bolle joined #darcs-theory
22:59 gal_bolle joined #darcs-theory

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