--- Log opened Wed Sep 24 16:18:53 2008
-!- Irssi: #agda: Total of 5 nicks [0 ops, 0 halfops, 0 voices, 5 normal]24/09 16:18
-!- Irssi: Join to #agda was synced in 0 secs24/09 16:18
LaneyWow, this exists!24/09 16:19
LaneyQuick question - how do I get a goal from a ? in agda/emacs? I can't figure out the key combination...24/09 16:20
LaneyA manual for agda-mode would be useful if such a thing exists24/09 16:20
LaneyAlso any good introductions to doing curry-howard style proofs in Agda ;) I'm trying to prove associativity of addition and it's not going to well :(24/09 16:34
--- Day changed Thu Sep 25 2008
--- Day changed Fri Sep 26 2008
--- Day changed Sat Sep 27 2008
--- Day changed Sun Sep 28 2008
--- Day changed Mon Sep 29 2008
--- Day changed Tue Sep 30 2008
_andrehello30/09 19:33
_andrei'm having some trouble building agda 2.1.230/09 19:34
_andrealso from darcs, although it goes a bit further30/09 19:41
kosmikus_andre: forget about agda 2.1.230/09 20:06
kosmikuswhat's the problem with the darcs version?30/09 20:07
_andreNot in scope: `quickCheck''30/09 20:07
_andrei have installed QuickCheck with cabal though30/09 20:07
kosmikusagda needs quickcheck-2.0 or higher30/09 20:08
_andrei have installed30/09 20:08
kosmikusok30/09 20:09
kosmikusI have 2.030/09 20:09
kosmikuslet me see if it works with 2.1, too30/09 20:09
kosmikuswhere do you get the error message?30/09 20:11
_andreAgda.Utils.List30/09 20:11
kosmikusnot when doing "Setup configure", but sometime later?30/09 20:11
kosmikusah30/09 20:11
kosmikusstrange30/09 20:11
_andrein the build step30/09 20:11
kosmikusthe 2.1 quickcheck release it very recent30/09 20:11
kosmikusprobably the interface did change30/09 20:12
_andredo you know if cabal lets me choose a different version of a library?30/09 20:14
kosmikusok, I can reproduce30/09 20:14
kosmikusI have a quick patch as a workaround30/09 20:21
_andredo you have a link?30/09 20:23
kosmikusone minute, I get another error30/09 20:24
kosmikuslooks good now, compilation more than halfway through30/09 20:26
kosmikussorry, taking a long time, but I'm still hopeful :)30/09 20:31
_andreno problem :)30/09 20:31
vixeyso has anybody got any programs in Agda? Something that does something, not just compute factorial30/09 20:32
_andrenot me, i've found agda today :)30/09 20:34
kosmikusdepends on what you call a program :)30/09 20:34
kosmikusactually, the standard library already contains quite some stuff30/09 20:34
kosmikusthere's an AVL tree implementation now, for instance30/09 20:34
_andrehow does agda compare to ATS?30/09 20:35
_andreis it the same kind of type system?30/09 20:35
vixeyApparently ATS has linear types (yet no section in the user manual about them), but I don't think Agda does30/09 20:36
kosmikuswell, interestingly, I've only heard about ATS last week30/09 20:36
kosmikusI want to look at it, but haven't yet30/09 20:36
vixeythen again, does ATS have coinductives? Agda does now, but I don't think ATS does30/09 20:36
vixeyit's weird, there's been a (mini) surge in intrest in ATS recently30/09 20:37
_andrei guess it's because of the benchmark game thing30/09 20:37
_andrei don't know it either, i just know about it because Hongwei Xi was my boss' advisor in his masters :p30/09 20:38
kosmikus_andre: ok, try 20:39
vixey:o30/09 20:39
kosmikus_andre: so who's your boss? :)30/09 20:40
_andrecan i apply this with "patch" ?30/09 20:40
kosmikus_andre: no, with darcs apply30/09 20:40
_andreok, building30/09 20:41
_andrehe's called Michel Machado30/09 20:42
_andrei don't know exactly what kind of work he did in ATS though30/09 20:43
_andrehmm30/09 20:43
_andrekosmikus: i guess i may have a bytestring version which is too new30/09 20:43
_andrealthough this error is really weird30/09 20:44
_andresrc/full/Agda/TypeChecking/Serialise.hs:102:25:30/09 20:44
_andre    Couldn't match expected type `bytestring-'30/09 20:44
_andre           against inferred type `ByteString'30/09 20:44
_andrei don't know how cabal works, is it normal for it to include the package and version in the type like that?30/09 20:45
kosmikusno, this is unfortunately a rather common problem with Cabal/Haskell30/09 20:46
kosmikusyou have two libraries that both depend on bytestring30/09 20:46
kosmikusbut they're both built with different versions of bytestring30/09 20:46
kosmikusso they can't be used together30/09 20:46
_andreoh30/09 20:47
_andrei guess i shouldn't have ignored those configure warnings then :p30/09 20:47
kosmikusah, you got warnings?30/09 20:47
_andrezlib is using an older version30/09 20:47
_andreyeah30/09 20:47
_andreWarning: This package indirectly depends on multiple versions of the same30/09 20:47
_andrepackage. This is highly likely to cause a compile failure.30/09 20:47
kosmikusthat's good, because then you can find out which libraries are affected30/09 20:47
kosmikusjust reinstall the one that depends on the older bytestring30/09 20:48
_andreseems to have worked30/09 20:49
_andrei still get "Warning: defaultUserHooks in Setup script is deprecated." but i guess that's ok30/09 20:49
kosmikusthat's ok30/09 20:50
_andreit built and installed :)30/09 20:53
kosmikusgreat30/09 20:54
kosmikusif you try ats too, let me know how it is :)30/09 20:54
_andrei can tell it's ugly :P30/09 20:54
kosmikusyeah30/09 20:54
kosmikusit seems much more low-level30/09 20:55
kosmikusbut otoh, it seems to be fast30/09 20:55
_andrethose benchmark programs were half embedded C30/09 20:55
kosmikusfor now, I'm more interested in what DTP can do than in the actual speed of the implementation30/09 20:55
vixeyDo you know of any automatic implementations of Bove-Capretta method?30/09 20:56
vixeyIn Agda or anything else30/09 20:56
kosmikushmm, I have to look up what that is :)30/09 20:57
_andrestupid question... it doesn't install a binary?30/09 20:57
* vixey is going to have a go at implementing it probably ..30/09 20:57
kosmikusoh, seems to be a technique I know, but not under that name30/09 20:57
kosmikusno, I don't know of any automatic implementations, I think30/09 20:57
vixey_andre, oh I think that GHC just runs the agda toplevel, doesn't it?30/09 20:58
kosmikus_andre: the recommended way is to use the emacs mode30/09 20:58
kosmikus_andre: and that just needs ghc(i) and the library30/09 20:58
kosmikus_andre: you can install a binary, too.30/09 20:58
kosmikus_andre: cd src/main30/09 20:58
_andreyou also need to know emacs :P30/09 20:58
vixeyoh emacs is really easy30/09 20:58
kosmikus_andre: runghc Setup configure / build / install in there again30/09 20:58
* _andre is a vim person30/09 20:58
vixeyyou just type text and hit key commands30/09 20:58
kosmikus_andre: I'm a vim user too30/09 20:58
kosmikus_andre: otoh, the emacs mode is really great30/09 20:59
kosmikus_andre: I wish they'd implement the same for vim ...30/09 20:59
vixeyI think the only important key command is save (C-x C-s and type check, C-c C-x l (maybe that's wrong?))30/09 20:59
kosmikusvixey: are you doing research on dependent types?30/09 21:00
vixeyI'm not sure30/09 21:02
vixeyI'm not with any institution or anything, but I am interested in using them ..30/09 21:02
kosmikusheh30/09 21:03
kosmikusso you're working in a company?30/09 21:03
vixeyno30/09 21:03
_andrei gotta go..30/09 23:03
_andrekosmikus: thanks for the help, i'll keep reading on agda :)30/09 23:03
--- Log closed Wed Oct 01 00:00:23 2008

Generated by 2.7 by Marius Gedminas - find it at!