Moar Parsing

I burned the midnight oil a bit last night working on my output serializer/parser and got it working. The grammar is nearly complete, with only 1 shift/reduce conflict. The parser will take a coqtop response, such as

1 subgoal
  A : Prop
  B : Prop
  C : Prop    
  ============================
   A -> ~ ~ A \/ B > C
"""

and turn that into a mostly correct python object, which for now is just a dict:

{   'goal': {   'expr': (   {   'expr': ('A', '~ ~ A'), 'operator': '->'},
                            {   'expr': ('B', 'C'), 'operator': '>'}),
                'operator': '\\/'},
    'hyp': [   {   'name': 'A', 'type': 'Prop'},
               [{   'name': 'B', 'type': 'Prop'}, {   'name': 'C', 'type': 'Prop'}]],
    'subgoal': '1 subgoal'}

It's pretty cool to see it work correctly on my sample strings, but the next step will be to bring it into the request/response lifecycle and see how well these objects will serialize. Still for now, progress has been made!

Cockerel and Exposing processes to webpages

A large part of this project is allowing a user to connect to a webpage containing a form and interact with a foreign process. By design, I am encouraging remote execution of code on my server. Now, this is a decently solved problem with sites like Code Pad and projects like Geordi, but that doesn't make the particulars of implementation any easier! I've found that a large number of choices need to be made when implementing a system in this way. They range from user access and sandbox environments to tracking state in a web session.

Over the last two weeks, I've completed the basic development for Cockerel to offer a web form which you can prove theorems in. In other words, the site's up! (but only figuratively). There is a server process for multiplexing coqtop sessions called coqd. This is an extension of the Twisted Protocol which spawns a new pexpect coqtop process. Just using this alone, a user can send JSON of this schema

POST
{ "userid": "id",
  "command": "cmd_str"
}

Response
{ "userid": "id",
  "response": "resp"
}

For now, the website just passess the response through as plain text, but I am working on an output parser using PLY for better styling. There is no requirement to run my webserver to use coqd.

On the front end, I'm using Flask to build out my website. At the moment there's only one page. It's a simple form to send in proofs. You can only step through them, and its not going to be too nice to bad proofs. The proofscript line counter I'm using might be a little buggy at the moment, but it works for most cases. Sooner or later I'll need to add Undo.

Well that's all I've got for now, much more to come! Since there is a page that can be used, now's a good time to pull the code and give it a try. I'll update the README for which dependencies are required for install, but a short list is

flask
twisted
pexpect

Enjoy!

Why Twisted Changed My Life

So at Open Source Bridge I ran into the folks at OSU's Open Source Lab. They were a huge help for flushing out the high level architecture of my connection server for Cockerel. Their project, pydra, was on my list of libraries for implementing a non-blocking i/o server. Had I done it that way, I would have been in for some pain. That is definitely not
what pydra was designed for; its great for large processing jobs over networks. Instead, they suggested using Twisted.

For those who don't know, Twisted is a Python library designed for building async-network servers. Internal classes include, protocols for connections, bare-bones ssh clients, irc clients/servers, and a variety of other utilities for building your async-server/client
application. The maturity of the libraries allowed me to build out a simple connection protocol in a little over 30 minutes.

Implimenting a server protocol in Twisted is very simple. You can begin with the base protocol.Protocol, for example, and then define a dataReceived() method that processes the data. That's pretty much it! Now, dealing with exceptions and other particulars is clearly going to take most of the dev time, but the basics of your server can be completed just like that. I highly recommend trying it out.

Thanks again to OSL! Y'ALL ROCK!

Cockerel: A simpler Proof Checker

I'll be working on the Cockerel web-based proof checker for Google Summer of Code. It is specifically designed to make proof writing and verification a productive process for introductory students. Portland State University is providing mentoring and an initial deployment for this system. The project gets it name from the backend logic engine, Coq. You can track my progress from the project git repo.

git://github.com/dcolish/Cockerel.git


init

Well I think at least one post is required for my blog to actually be a blog. Here it is.