Camelia, the Perl 6 bug

IRC log for #darcs, 2013-03-01

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

All times shown according to UTC.

Time Nick Message
00:47 mizu_no_oto joined #darcs
00:48 intripoon joined #darcs
01:57 mizu_no_oto joined #darcs
02:28 intripoon_ joined #darcs
02:54 carter_ joined #darcs
04:35 preflex_ joined #darcs
05:10 favonia joined #darcs
06:47 lelit joined #darcs
07:35 GrayGnome joined #darcs
08:23 amgarchIn9 joined #darcs
08:30 raichoo joined #darcs
09:13 favonia joined #darcs
09:41 owst joined #darcs
11:09 owst If a patch removing a file is rolledback, would you expect darcs to implicitly `darcs add` the file, such that it shows up in whatsnew, without -l?
11:43 owst Well I decided it was a bug :-)
11:45 lelit owst, right decision, IMHO
11:45 lelit :)
13:14 mizu_no_oto joined #darcs
13:18 GrayGnome I need to go to bed because it's really early/late here but
13:18 GrayGnome How's the progress on the camp proving thing going?
13:22 owst GrayGnome: I would say "stalled"
13:23 GrayGnome Is there any way for me to look at what happned in some semi-organized fashion?
13:23 owst Do you know coq?
13:23 GrayGnome Some
13:23 GrayGnome I'm a bit more familiar with PVS but I'm trying to move to Coq
13:23 GrayGnome And am new to theorem proving in general heh.
13:24 owst let me see if I can find Igloo's latest link to his WIP copy of the coq script/documentation
13:24 GrayGnome I skimmed the theory pdf while procrastinating but it's just a hodgepodge.
13:24 GrayGnome Also the makefile looks really scary.
13:24 owst GrayGnome: which pdf was that?
13:24 owst It may be the one I'm thinking of
13:24 GrayGnome http://projects.haskell.org/camp/files/theory.pdf <-- This one
13:24 owst Oh yeah, that's the one I was thinking of
13:24 Igloo What's scary about the Makefile, OOI?
13:26 GrayGnome Just lots of .v and .vo files everywhere
13:26 GrayGnome But they have sane names so maybe I'm overreacting.
13:27 GrayGnome Just curious, what is still left to be proven? (I hope I don't come under fire here for not closely reading the theory doc.)
13:27 Igloo Oh, do you mean Makefile.coq? That's an automatically generated dependencies file
13:28 Igloo The main thing left to prove is all the cases for catch commute, IIRC
13:29 owst Which is presumably a big chunk of work? :-)
13:29 GrayGnome Okay.
13:29 Igloo Yup  :-)
13:30 GrayGnome I'll bother you guys more later probably. I need to sleep and wake up and continue doing boring work.
13:30 GrayGnome Thanks~
13:31 mizu_no_oto joined #darcs
14:38 mizu_no_oto joined #darcs
14:45 lambdabot joined #darcs
15:45 lispy joined #darcs
15:48 mizu_no_oto joined #darcs
15:50 donri joined #darcs
17:16 stepkut joined #darcs
17:52 raichoo joined #darcs
18:01 gh_ joined #darcs
18:22 amgarchIn9 joined #darcs
18:24 mizu_no_oto joined #darcs
18:30 mizu_no_oto joined #darcs
18:35 gh_ joined #darcs
19:57 favonia joined #darcs
20:12 stulli joined #darcs
20:14 carter_ joined #darcs
20:20 `nand` joined #darcs
20:31 iago joined #darcs
20:48 mizu_no_oto joined #darcs
20:51 favonia joined #darcs
21:11 gh_ joined #darcs
22:18 favonia joined #darcs

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