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!