- Haskell-Cafe - Haskell.org

ANN: theoremquest-0.0.0
by Tom Hawkins 08 Mar '11

08 Mar '11

I have been wanting to gain a better understanding of interactive theorem proving for some time. And I've often wondered: Can theorem proving be made into a user-friendly game that could attract mass appeal? And if so, could a population of gamers collectively solve interesting and relevant mathematical problems? To try to answer these questions -- and to gain some experience myself with theorem proving -- I started a project called TheoremQuest [1]. TheoremQuest intends to be a multi-player game system, where the game server receives requests by clients, such as theorem queries and inference rule applications. The TheoremQuest server validates deductions, compares them with existing theorems in the database, then returns results. TheoremQuest's deductive system borrows that of John Harrison's HOL Light [2]. There are 2 Hackage packages: theoremquest [3] is a library that declares types for terms, inference rules, and client-server transactions, used by both server and clients; and theoremquest-client [4] is an example client (tq). All the code, including the server-side, is hosted at github [5]. Currently the client-server interface is working, but little else. The library has defined most of the core inference rules, but has none of the basic types or axioms. And the "tq" client is nothing at all like a game; at this point it is just a command line tool to test the server. Currently "tq" can ping the server, create a new user, apply inference rules, and print out theorems. Here's how "tq" can prove "x |- x": $ tq newuser tomahawkins tomahawkins(a)gmail.com Ack $ export THEOREMQUEST_USER=tomahawkins $ tq infer 'ASSUME (Var (Variable "x" Bool))' Id 1 $ tq theorem 1 assumptions: Var (Variable "x" Bool) conclusion: Var (Variable "x" Bool) I'd love to have help with this project, if anyone's interested. I'm still grappling with the logical core, but I think the real challenge will be creating game clients that are both capable and yet intuitive enough to appeal to the general population. If the masses can play Sudoku, shouldn't they be capable of interactive theorem proving? -Tom [1] http://theoremquest.org [2] http://www.cl.cam.ac.uk/~jrh13/hol-light/ [3] http://hackage.haskell.org/package/theoremquest [4] http://hackage.haskell.org/package/theoremquest-client [5] http://github.com/tomahawkins/theoremquest

9 12

makeTokenParser + LanguageDef
by Hauschild, Klaus (EXT) 08 Mar '11

08 Mar '11

Hi Haskellers, is there a fine tutorial for building a parser with parsecs (3.*) makeTokenParser and LanguageDef stuff? Klaus

3 2

I think I've found a regression in Haskell Platform, but what do I do next?
by Nick Frolov 08 Mar '11

08 Mar '11

Hi, Recently I had to switch from ghc 6.12.3 to ghc 7.0.1 because of the bug #4235. This switch has introduced a problem with one of third-party libraries I use ('satchmo', an interface for SAT solvers). The problem is that writing to stdin of a process started by System.Process.runInteractiveCommand silently fails provided it's stderr is not read. If stderr of the spawned process is redirected to /dev/null or fully read by the parent process, then problem does not come up. The troubled code is available at http://bit.ly/dNwrIV (lines 43-45). Changes between versions of the 'process' library (1.0.1.3 -> 1.0.1.4) bundled with ghc 6.12.3 and 7.0.1 only include one bug fix, which is not the source of the problem described, as far as I can understand. The problem is not present with ghc 6.12.* at all. Something has definitely changed between these two ghc versions. Since I've spent considerable amount of time on finding a workaround for the problem, I'd like to file a real bug report, but I'm not completely sure where to do it because there are several pieces of software involved (ghc itself, 'process', 'satchmo' and 'minisat2' SAT solver). Could somebody guide me please?

2 2

Questions on list administration
by Karthick Gururaj 08 Mar '11

08 Mar '11

Hello, I recently joined Haskell group and wanted to share a few points. First, I came to Haskell cafe from google groups (groups.google.com -> search for Haskell). Two groups are listed: fa.haskell and haskell-cafe. I became a "member" of Haskell Cafe via the google groups interface (the operation was successful according to google). When I posted a message, I got an automated email (within a few seconds, so I think there was no human moderation): You are not allowed to post to this mailing list, and your message has been automatically rejected. If you think that your messages are being rejected in error, contact the mailing list owner at haskell-cafe-owner(a)haskell.org. I wrote to the email address mentioned and didn't get any response. Funny thing is, google reports that my post was successful, and my post was "visible" on google groups even after I signed out from my google account. I next wrote to the group owner, again from the google groups interface (there is an option to "send email to the owner"). No response here as well. I then went to Haskell.org -> Mailing lists and saw there are atleast three lists of immediate relevance, including one for beginners. The website also describes the posting guidelines and other information. Very useful. I would have stuck to asking questions on the beginner's group if I had known earlier.. Can I ask a couple of changes be done to help others like me? a. In google groups -> https://groups.google.com/group/haskell-cafe/about -> add a link to the haskell.org -> Mailing lists for more info. b. Let users join from google groups interface, or if this is not possible, mention that in the "about" page c. Change the contents of the reject email (reproduced above) to include the following: "If you want to subscribe to the Haskell Cafe mailing list, please visit http://www.haskell.org/mailman/listinfo/haskell-cafe" Aside: the Haskell Cafe mailing list page (at http://www.haskell.org/mailman/listinfo/haskell-cafe) has a dead link at the bottom of the page. The "Overview of all haskell.org mailing lists" points to http://www.haskell.org/cgi-bin/mailman/listinfo (404 error) instead of http://haskell.org/mailman/listinfo. Thanks! Warm regards, Karthick

2 1

AusHack 2011
by Ivan Lazar Miljenovic 08 Mar '11

08 Mar '11

It is time once again to start planning for AusHac (the Hackathon Down Under)! The current proposed dates are 8-10 July. This time we're trying to organise a venue in the Sydney CBD, but if all else fails we'll be at UNSW again. So, is anyone vehemently opposed to having AusHac at this time or place? -- Ivan Lazar Miljenovic Ivan.Miljenovic(a)gmail.com IvanMiljenovic.wordpress.com

1 0

Re: [Haskell-cafe] [Haskell] ANNOUNCE: silently-0.0.1 (prevent IO actions from writing to stdout)
by trystan.s＠comcast.net 07 Mar '11

07 Mar '11

Thanks for the feedback! I'll definitely update the documentation. I agree that temp files are a weird way to go about it but they're the least surprising and dangerous way I could think of handling it. Unix has /dev/null and Windows has a NUL device that works the same way so I could use those. * I could see what OS it is and try those options and use a temp file only if it's an unexpected os. Unfortunately System.Info.os reports windows (and some other os's) as "mingw32", I think it's because of how GHC was compiled. Who knows what the real os is or what each os will be reported as in the future or how they appear to other compilers and runtimes. * I could write to /dev/null or NUL if they exist and use a temp file if neither does, but if there's a legitimate /dev/null or NUL file then having some unrelated program write to them would be very very bad and a major pain for whoever has to figure that one out. I'd rather not use temp files but both of these seem problematic. Does anyone have a better idea or think that either of those are acceptable? Trystan Spangler ----- Original Message ----- From: "Felipe Almeida Lessa" <felipe.lessa(a)gmail.com> To: "Trystan Spangler" <trystan.s(a)comcast.net> Cc: haskell-cafe(a)haskell.org Sent: Monday, March 7, 2011 3:41:07 AM Subject: Re: [Haskell] ANNOUNCE: silently-0.0.1 (prevent IO actions from writing to stdout) Hello! I wouldn't expect that a function that ignores the output directs it to a temporary file. I think that should be clearly stated on the documentation, as this may be undesirable. I don't know if there is a better way of solving this problem, though. (Note, however, that on Unix systems you could probably direct the output to /dev/null.) Cheers, -- Felipe.

2 2

ghc in debian sid
by rustom 07 Mar '11

07 Mar '11

I tried to move from debian testing to sid and got the message that a whole load of libghc**'s would be removed. Are more recent ones lined up?

1 1

groupBy huh?
by Jacek Generowicz 07 Mar '11

07 Mar '11

Hi Cafe, It seems that I don't understand what groupBy does. I expect it to group together elements as long as adjacent ones satisfy the predicate, so I would expect ALL four of the following to give one group of 3 and a group of 1. Prelude> :m + Data.List Prelude Data.List> groupBy (<) "abcb" ["abcb"] Prelude Data.List> groupBy (<) "abca" ["abc","a"] Prelude Data.List> groupBy (<) [1,2,3,2] [[1,2,3,2]] Prelude Data.List> groupBy (<) [1,2,3,1] [[1,2,3],[1]] What am I missing? Thanks.

7 9

Re: [Haskell-cafe] [Haskell] ANNOUNCE: silently-0.0.1 (prevent IO actions from writing to stdout)
by Felipe Almeida Lessa 07 Mar '11

07 Mar '11

Hello! I wouldn't expect that a function that ignores the output directs it to a temporary file. I think that should be clearly stated on the documentation, as this may be undesirable. I don't know if there is a better way of solving this problem, though. (Note, however, that on Unix systems you could probably direct the output to /dev/null.) Cheers, -- Felipe.

1 0

Idiomatic error handling in Haskell
by Rouan van Dalen 07 Mar '11

07 Mar '11

There are quite a few exception handling mechanisms provided by Haskell, as can be seen from this post: http://www.randomhacks.net/articles/2007/03/10/haskell-8-ways-to-report-err… I would like to know what is the preferred Haskell mechanism for handling exceptions in the IO monad? I am not concerned with mechanisms such as Maybe / Either, but would like to know about exception mechanisms inside the IO monad. The 2 I know of are: o) throwDyn o) ioError and catch I do need the exceptions to be extendable. So which is the preferred way to handle exceptions in Haskell for new libs?

2 2