Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

final stuff before submission

  • Loading branch information...
commit 5b4936d17bda65a98a85c631315d85f708db588a 1 parent 9d40e6d
@dcolish authored
View
2  cockerel/webapp/templates/admin/login.html
@@ -13,5 +13,5 @@
{% endfor %}
</ul>
</dl>
- <p>{{ html.input(type='submit', value='add') }}</p>
+ <p>{{ html.input(type='submit', value='login') }}</p>
</form>
View
2  cockerel/webapp/templates/prover/prover.html
@@ -17,7 +17,7 @@
});
});
</script>
-<form id="f_prover" action="{{ prover_url }}" method="POST">
+<form id="prover" action="{{ prover_url }}" method="POST">
<p>
<textarea id="f_prover_proofscript" name="proofscript" rows="20" cols="60">
</textarea>
View
123 cockerel/webapp/views/prover/prover.py
@@ -7,27 +7,55 @@
from flask import (
g,
Module,
- url_for,
render_template,
request,
session,
+ url_for,
)
from cockerel.models.schema import Proof, Theorem
+from cockerel.webapp.views.util import login_required
prover = Module(__name__)
+class ProofException(Exception):
+ """Identifier for proof exceptions"""
+ pass
+
+
def readscript(script):
- '''Chew up blank lines'''
- return [x for x in script.splitlines() if not x == '']
+ """Chew up blank lines, and be a little lame about it"""
+ return [x.strip() + '.' for x in script.strip().rsplit(r'.')
+ if not x == u'']
+
+
+def exec_cmd(command, session):
+ host = g.config.get('COQD_HOST')
+ port = g.config.get('COQD_PORT')
+
+ try:
+ tn = telnetlib.Telnet(host, port)
+ tn.write(JSONEncoder().encode(dict(userid=str(session['id']),
+ command=command)))
+ proofst = JSONDecoder().decode(tn.read_all())
+ return proofst.get('response', None)
+
+ except Exception:
+ logging.error("Connection to coqd failed")
+ raise ProofException()
+
+
+def get_proofscript(request):
+ proofscript = request.form.get('proofscript')
+ return formatscript(proofscript)
-def formatscript(script, slice):
+def formatscript(script):
commandlist = readscript(script)
- processed = '\\n'.join(commandlist[:slice])
- unprocessed = '\\n'.join(commandlist[slice:])
- return processed, unprocessed, commandlist
+ theorem = commandlist[0]
+ proof = '\\n'.join(commandlist[1:])
+ return theorem, proof, commandlist
def hash_theorem(theorem):
@@ -35,75 +63,64 @@ def hash_theorem(theorem):
def ping_coqd():
+ """check the coqd server is alive"""
pass
-@prover.route('/prover', methods=['GET', 'POST'])
-def editor():
- proofst = None
- host = g.config.get('COQD_HOST')
- port = g.config.get('COQD_PORT')
+@prover.route('/prover/', methods=['GET'])
+@prover.route('/prover/<int:theorem_id>', methods=['GET', 'POST'])
+@login_required
+def editor(theorem_id=0):
+ proofst = processed = None
lineno = 0
+ theorem = Theorem.query.filter_by(id=theorem_id).first()
+
+ if theorem:
+ theorem_text = theorem.text.rstrip()
+ proof = Proof.query.filter_by(theorem=theorem).filter_by(
+ user_id=g.user.id).first()
+
+ if not proof:
+ proof = ""
+
+ else:
+ theorem_text = proof = ""
+
+ unprocessed = ''.join([theorem_text, proof])
if request.method == 'POST':
if not session.get('id'):
session['id'] = uuid4()
if request.form.get('clear'):
+ processed, unprocessed, commandlist = get_proofscript(request)
command = 'quit'
- proofscript = request.form.get('proofscript')
- processed, unprocessed, commandlist = formatscript(proofscript, 0)
processed = None
+ unprocessed = '\\n'.join([theorem_text, unprocessed])
elif request.form.get('undo'):
lineno = 0 if lineno == 0 else int(request.form.get('line')) - 1
- proofscript = request.form.get('proofscript')
- processed, unprocessed, commandlist = formatscript(proofscript,
- lineno)
+ processed, unprocessed, commandlist = get_proofscript(request)
command = 'Undo.'
else:
lineno = int(request.form.get('line'))
- proofscript = request.form.get('proofscript')
- processed, unprocessed, commandlist = formatscript(proofscript,
- lineno)
+ processed, unprocessed, commandlist = get_proofscript(request)
command = commandlist[lineno]
logging.debug('Sending %d : %s', lineno, command)
lineno += 1
+
# here is where we'll pass it to coqd
if command:
try:
- tn = telnetlib.Telnet(host, port)
- tn.write(JSONEncoder().encode(dict(userid=str(session['id']),
- command=command)))
-
- proofst = JSONDecoder().decode(tn.read_all())
- proofst = proofst.get('response', None)
-
- except Exception:
+ proofst = exec_cmd(command, session)
+ except ProofException:
lineno = lineno - 1 if lineno != 0 else 0
- logging.error("Connection to coqd failed")
-
- return render_template('prover/prover.html',
- prover_url=url_for('editor'),
- processed=processed,
- unprocessed=unprocessed,
- proofst=proofst,
- lineno=lineno)
- else:
- # new proof session so set it up
- unprocessed = request.args.get('theorem', "")
- theorem = Theorem.query.filter_by(id=unprocessed).one()
- if theorem:
- text = theorem.text.rstrip()
- proof = Proof.query.filter_by(theorem=theorem).first()
- if not proof:
- proof = ""
- else:
- theorem = proof = ""
- return render_template('prover/prover.html',
- prover_url=url_for('editor'),
- proofst=proofst,
- processed=None,
- unprocessed=''.join([text,proof]),
- lineno=lineno)
+
+ return render_template('prover/prover.html',
+ prover_url=url_for('editor',
+ theorem_id=theorem_id),
+ proofst=proofst,
+ processed=processed,
+ unprocessed=unprocessed,
+ lineno=lineno)
View
7 manager.py
@@ -1,5 +1,6 @@
from flaskext.script import Manager, Server, Shell
+from coqd.runner import main as coqd_main
from cockerel.webapp import app, db
from cockerel.models import schema
@@ -18,5 +19,11 @@ def initdb():
db.drop_all()
db.create_all()
+
+@manager.command
+def runcoqd():
+ coqd_main()
+
+
if __name__ == "__main__":
manager.run()
View
2  tests/functional/test_login.py
@@ -14,3 +14,5 @@ def test_login():
login = page.login_form
login.fill(dict(username='test',
password='user'))
+ page.click_submit()
+ assert not page.offers_login_form
View
16 tests/functional/test_prover.py
@@ -0,0 +1,16 @@
+from tests.pages.admin import Login
+from tests.pages.prover import ProverPage
+from tests.functional import browser, testcase
+
+
+@testcase()
+def test_prover_requires_login():
+ browser.open('/prover')
+ page = Login()
+ assert page.offers_login_form
+ login = page.login_form
+ login.fill(dict(username='test',
+ password='user'))
+ page.click_submit()
+ page = ProverPage()
+ assert page.offers_prover
View
4 tests/functional/test_signup.py
@@ -1,6 +1,6 @@
from tests.functional import browser, testcase
from tests.pages.base import Page
-from tests.pages.admin import Login, Signup
+from tests.pages.admin import Signup
@testcase()
@@ -17,5 +17,3 @@ def test_signup():
foo.fill(dict(username='yermom', password='foobar'))
foo.submit()
assert not page.offers_signup_link
-
-
View
4 tests/pages/base.py
@@ -22,3 +22,7 @@ def click_login_link(self):
def click_signup_link(self):
button = browser.document['#signup']
button.click('page')
+
+ def click_submit(self):
+ button = browser.document["input[type='submit'][value='login']"][0]
+ button.click('page')
View
9 tests/pages/prover.py
@@ -0,0 +1,9 @@
+from tests.functional import browser
+from .base import Page
+
+
+class ProverPage(Page):
+
+ @property
+ def offers_prover(self):
+ return browser.document['#prover']
Please sign in to comment.
Something went wrong with that request. Please try again.