Skip to content

Commit

Permalink
cleanups, make coqd not require json by default. add code to interp
Browse files Browse the repository at this point in the history
  • Loading branch information
dcolish committed Sep 13, 2010
1 parent 66d09f2 commit 093cedf
Show file tree
Hide file tree
Showing 7 changed files with 78 additions and 33 deletions.
1 change: 0 additions & 1 deletion MANIFEST.in
Expand Up @@ -2,7 +2,6 @@ include README
include LICENSE
recursive-include tests *
recursive-exclude tests *.pyc
recursive-exclude tests *.pyc
recursive-include docs *
recursive-exclude docs *.pyc
recursive-exclude docs *.pyo
Expand Down
17 changes: 13 additions & 4 deletions cockerel/webapp/templates/base.html
Expand Up @@ -5,11 +5,14 @@
<head>
<title>Cockerel Logic Checker - {% block title %}{% endblock %}</title>
<link rel="stylesheet" type="text/css" href="/static/site.css" />
<script type="text/javascript" src="http://www.google.com/jsapi?key=ABQIAAAA8Iq3w1LF6TgIDgZx7RQ_cRT7g5bZECU_gqoByQmzcFSTeCxKshRn_ZMRy-gSPjQ8nSSldSReJClRvA"></script>
<script type="text/javascript"
src="http://www.google.com/jsapi?key=ABQIAAAA8Iq3w1LF6TgIDgZx7RQ_cRT7g5bZECU_gqoByQmzcFSTeCxKshRn_ZMRy-gSPjQ8nSSldSReJClRvA"></script>
<script>
google.load('jquery', '1.4.2');
</script>
<script type="text/javascript" language="javascript" src="http://colishcloud.appspot.com/static/codemirror/js/codemirror.js" ></script>
<script type="text/javascript"
language="javascript"
src="http://colishcloud.appspot.com/static/codemirror/js/codemirror.js" ></script>
<!-- <script type="text/javascript" language="javascript" src="/static/cockerel.js"></script> -->
</head>
<body>
Expand Down Expand Up @@ -39,8 +42,14 @@ <h1>Welcome to Cockerel</h1>
<div id="footer">
{% block footer %}
{% endblock %}
<p>Copyright 2010 by Dan Colish</p>
<a href="http://flask.pocoo.org/">
<img
src="http://flask.pocoo.org/static/badges/powered-by-flask-s.png"
border="0"
alt="powered by Flask"
title="powered by Flask" />
</a>
<p>Copyright 2010 by Dan Colish</p>
</div>

</body>
</html>
1 change: 0 additions & 1 deletion cockerel/webapp/templates/classes/view.html
Expand Up @@ -6,7 +6,6 @@
<p><a href="{{ url_for('classes.register', class_id=class_section.id) }}">Register</a></p>
{% else %}
<p>Lessons</p>

<ul>
{% for lesson in lessons %}
<li><a href="{{ url_for('lessons.view', lesson_id=lesson.id) }}">{{ lesson.lesson_name }}</a></li>
Expand Down
2 changes: 1 addition & 1 deletion cockerel/webapp/views/prover/mdx_prover.py
Expand Up @@ -10,7 +10,7 @@
Goal True -> True.
>>>
"""
from urllib import urlencode

import re
import markdown

Expand Down
13 changes: 11 additions & 2 deletions coqd/connserv.py
Expand Up @@ -66,6 +66,9 @@ def quit(self):

active_conns = {}

def connectionMade(self):
self.serialize = self.factory.serialize

def dataReceived(self, data):
"""
Parse data we've recieved and send to proof engine
Expand All @@ -76,8 +79,14 @@ def dataReceived(self, data):
command = req_data.get('command')
userid = req_data.get('userid')
resp_data = self.handle_command(userid, command)
resp_data['response'] = self.do_parse(resp_data['response'])
self.transport.write(JSONEncoder().encode(resp_data))

data = resp_data['response']

if self.serialize:
resp_data['response'] = self.do_parse(resp_data['response'])
data = JSONEncoder().encode(resp_data)

self.transport.write(data)
self.transport.loseConnection()

def do_parse(self, output):
Expand Down
44 changes: 34 additions & 10 deletions coqd/interp.py
@@ -1,24 +1,48 @@
from code import InteractiveConsole
from argparse import ArgumentParser
from json import JSONDecoder, JSONEncoder
import readline
import logging
from sys import argv
import telnetlib


def send(command):
def send(command, serialize):
try:
tn = telnetlib.Telnet('localhost', 8003)
tn.write(JSONEncoder().encode(dict(userid=0,
command=command)))
proofst = JSONDecoder().decode(tn.read_all())
proofst = proofst.get('response', None)
if serialize:
proofst = JSONDecoder().decode(tn.read_all())
proofst = proofst.get('response', None)
else:
proofst = tn.read_all()
print proofst
except Exception:
logging.error("Connection to coqd failed")

while True:
try:
prompt = raw_input(">>> ")
send(prompt)
except:
pass

def options(parser):
parser.add_argument("--serialize", action="store_true",
default=False,
help="Serialize output to JSON")
return parser


def main():
"""
Setup and run coqd
"""
parser = ArgumentParser(prog="Coqd", description="Options for Coqd",
version="Coqd 0.1")
parser = options(parser)
opts = parser.parse_args(argv[1:])

while True:
try:
prompt = raw_input(">>> ")
send(prompt, opts.serialize)
except:
pass

if __name__ == '__main__':
main()
33 changes: 19 additions & 14 deletions coqd/runner.py
Expand Up @@ -3,14 +3,14 @@
~~~~~~
Main entry points for coqd
"""
# from argparse import ArgumentParser
from optparse import OptionParser
from argparse import ArgumentParser
# from optparse import OptionParser
from ConfigParser import SafeConfigParser
import logging
from sys import argv

from twisted.internet import reactor
from twisted.internet.protocol import Factory
from twisted.internet.protocol import ServerFactory

from connserv import CoqProtocol

Expand All @@ -22,36 +22,41 @@ def __init__(self, config_files):
self.conf.read(config_files)


class CoqFactory(ServerFactory):
protocol = CoqProtocol

def __init__(self, serialize):
self.serialize = serialize


def options(parser):
parser.add_option("--module", dest="modules", action="append",
parser.add_argument("--module", dest="modules", action="append",
default=[],
help="load modules into coqd, more than one "
"can be specified",
)
parser.add_option("--serialize", action="store_true",
default=False,
help="Serialize output to JSON")
parser.add_argument("--serialize", action="store_true",
default=False,
help="Serialize output to JSON")
return parser


def main():
"""
Setup and run coqd
"""
parser = OptionParser(prog="Coqd", description="Options for Coqd",
version="Coqd 0.1")
parser = ArgumentParser(prog="Coqd", description="Options for Coqd",
version="Coqd 0.1")
parser = options(parser)
opts, args = parser.parse_args(argv[1:])
opts = parser.parse_args(argv[1:])

if opts.modules:
# XXX: actual module loading occurs here
pass

logging.info("Coq is starting... hold on")

f = Factory()
f.protocol = CoqProtocol
reactor.listenTCP(8003, f)
factory = CoqFactory(opts.serialize)
reactor.listenTCP(8003, factory)
reactor.run()

if __name__ == '__main__':
Expand Down

0 comments on commit 093cedf

Please sign in to comment.