Camelia, the Perl 6 bug

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

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

All times shown according to UTC.

Time Nick Message
11:28 gal_bolle joined #darcs-theory
11:28 gal_bolle hi all
11:30 Igloo Hey hey
13:53 ertai gal_bolle: hi, I'm trying your coq formalization of patch theory
13:53 gal_bolle viel spaß
13:55 ertai gal_bolle: hopefully I've co-worker that speaks german :)
13:55 gal_bolle amuse-toi bien disais-je donc
13:56 ertai gal_bolle: currently my coq block on eq_trans
13:56 ertai what version do you use?
13:56 gal_bolle 8.2
13:56 gal_bolle coqtop
13:56 gal_bolle Welcome to Coq 8.2 (February 2009)
13:57 gal_bolle oh it's an old version you have
13:57 gal_bolle where did you get it from
13:57 gal_bolle ?
13:57 gal_bolle it's trans_eq
13:58 gal_bolle old version of my code, not of coq
14:00 ertai 8.2 March 2009
14:00 gal_bolle yes, you have an old version of my proofs
14:00 ertai from the darcs repo with paper of camp
14:00 gal_bolle which is buggy with all known coqs
14:00 gal_bolle ok
14:00 gal_bolle one second
14:00 ertai http://code.haskell.org/camp/devel/paper
14:01 gal_bolle there's a new repo at  darcs get http://patch-tag.com/publicrepos/dic
14:01 gal_bolle without the paper
14:02 ertai hum it now stops somewhere else in the comm_patch_seq inductive
14:03 gal_bolle what does it say?
14:32 ertai gal_bolle: that's your Set Implicit Arguments on the top of the file
14:32 gal_bolle yes
14:32 gal_bolle i'm going down the file changing everything to match that
14:32 ertai it tell coq to automatically make some implicit arguments
14:33 ertai A ok
14:33 gal_bolle i was waiting to be finished with that to make an announcement of the repo on darcs-user
14:33 gal_bolle it's a draft of a draft atm
14:33 ertai :)
14:34 ertai Temporarly adding a Unset Implicit Arguments at the right place helps
14:34 gal_bolle ok
14:34 gal_bolle thanks for the tip
14:35 ertai I will wait a little more then
14:37 gal_bolle yes, i'll send the announcement when it's ready
17:46 arjanb joined #darcs-theory

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