improvements to prover, better theorem tracking, added docs

htquach · Aug 7, 2010 · 1e05931 · 1e05931
1 parent c2c4aa3
commit 1e05931
Show file tree

Hide file tree

Showing 22 changed files with 670 additions and 38 deletions.
diff --git a/.gitignore b/.gitignore
@@ -9,4 +9,5 @@ lib64
 parsetab.py
 parser.out
 *.v.d
-*.egg-info
+*.egg-info
+docs/_build
diff --git a/MANIFEST.in b/MANIFEST.in
@@ -1,2 +1,12 @@
+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
+prune docs/_build
+prune docs/_themes/.git
 recursive-include cockerel/webapp/templates *
 recursive-include cockerel/webapp/static *
diff --git a/cockerel/models/schema.py b/cockerel/models/schema.py
@@ -15,11 +15,30 @@
                                      db.ForeignKey('classes.id')))
 
 
+class Theorem(db.Model):
+    __tablename__ = 'theorems'
+    id = db.Column(db.Integer, primary_key=True)
+    text = db.Column(db.String)
+    hash_value = db.Column(db.String)
+
+    def __init__(self, text, hash_value):
+        self.text = text
+        self.hash_value = hash_value
+
+    def __repr__(self):
+        return '<Proof %r>' % self.text
+
+
 class Proof(db.Model):
     __tablename__ = 'proofs'
     id = db.Column(db.Integer, primary_key=True)
     proofscript = db.Column(db.String)
     user_id = db.Column(db.Integer, db.ForeignKey('users.id'))
+    theorem_id = db.Column(db.Integer, db.ForeignKey('theorems.id'))
+
+    theorem = db.relationship('Theorem',
+                              order_by=Theorem.id,
+                              backref='theorems')
 
     def __init__(self, proofscript):
         self.proofscript = proofscript

diff --git a/cockerel/webapp/__init__.py b/cockerel/webapp/__init__.py
@@ -1,3 +1,9 @@
+"""
+cockerel.webapp
+---------------
+Main instance of the webapp. All modules will be loaded from this file. To
+add a new module you must import it here and register it.
+"""
 import logging
 import os
 
@@ -36,6 +42,7 @@
 
 
 def update_config():
+    """syncronizes the config with the g global request object"""
     g.config = app.config
 
 app.before_request(update_config)
diff --git a/cockerel/webapp/templates/base.html b/cockerel/webapp/templates/base.html
@@ -9,8 +9,7 @@
     <script>
       google.load('jquery', '1.4.2');
     </script>
-    <script type="text/javascript" language="javascript"
-            src="http://wtfbacon.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>

diff --git a/cockerel/webapp/templates/prover/prover.html b/cockerel/webapp/templates/prover/prover.html
@@ -6,8 +6,8 @@
 $(document).ready(function () {
     var editor = CodeMirror.fromTextArea("f_prover_proofscript", {
         parserfile: "parsedummy.js",
-        path: "/static/codemirror/js/",
-        stylesheet: "/static/codemirror/css/jscolors.css",
+        path: "http://colishcloud.appspot.com/static/codemirror/js/",
+        stylesheet: "http://colishcloud.appspot.com/static/codemirror/css/jscolors.css",
         tabMode: "spaces",
         initCallback: function() { 
             editor.setCode("{%- if processed -%}{{ processed|safe }} \n {% endif %}{%- if unprocessed -%}{{ unprocessed|safe }}{% endif %}\n\n");

diff --git a/cockerel/webapp/views/classes.py b/cockerel/webapp/views/classes.py
@@ -1,3 +1,11 @@
+"""
+classes.py
+-----------------------------
+
+Controller functions for classes. A class object allows you to add associated
+lesson plans.
+"""
+
 from flask import (
     g,
     Module,
@@ -18,13 +26,15 @@
 
 @classes.route('/classes', methods=['GET'])
 def index():
+    """Shows all classes currently in the system"""
     classes = Classes.query.all()
     return render_template("/classes/index.html", classes=classes)
 
 
 @classes.route('/classes/add', methods=['GET', 'POST'])
 @login_required
 def add():
+    """Users can add classes if they are authenticated"""
     if request.method == 'POST':
 
         form = AddEditClassForm.from_flat(request.form)
@@ -47,8 +57,8 @@ def add():
 @classes.route('/classes/edit/<int:class_id>', methods=['GET', 'POST'])
 @login_required
 def edit():
+    """Make modifications to a class"""
     if request.method == 'POST':
-
         form = AddEditClassForm.from_flat(request.form)
         form.validate()
         class_section = Classes(form['classname'].value,
@@ -69,6 +79,7 @@ def edit():
 @classes.route('/classes/register/<int:class_id>', methods=['GET'])
 @login_required
 def register(class_id):
+    """As a student user, register for access to a class"""
     if class_id and request.method == 'GET':
         section = Classes.query.filter_by(id=class_id).first()
         section.users.append(g.user)
@@ -79,6 +90,8 @@ def register(class_id):
 
 @classes.route('/classes/view/<int:class_id>', methods=['GET'])
 def view(class_id):
+    """View the lesson plans offered by a specific class. The user must be
+    either the admin or registered for that class"""
     section = Classes.query.filter_by(id=class_id).first()
     lessons = section.lessons
     if g.user in section.users:

diff --git a/cockerel/webapp/views/prover/mdx_prover.py b/cockerel/webapp/views/prover/mdx_prover.py
@@ -14,6 +14,12 @@
 import re
 import markdown
 
+from sqlalchemy.orm.exc import NoResultFound
+
+from cockerel.webapp import db
+from cockerel.models.schema import Theorem
+from .prover import hash_theorem
+
 
 class ProverExtension(markdown.Extension):
     """ Add definition lists to Markdown. """
@@ -28,7 +34,7 @@ def extendMarkdown(self, md, md_globals):
 class ProverPreprocessor(markdown.preprocessors.Preprocessor):
     """ Process Theorem. """
 
-    RE = re.compile(r'(?P<begin>^<{3,})[ ]*\n(?P<proofscript>.*?)'
+    RE = re.compile(r'(?P<begin>^<{3,})[ ]*\n(?P<theorem>.*?)'
                     '(?P<end>^>{3,})[ ]*$',
                     re.MULTILINE | re.DOTALL)
     WRAP = """
@@ -42,9 +48,18 @@ def run(self, lines):
         while 1:
             m = self.RE.search(text)
             if m:
+                hash_value = hash_theorem(m.group('theorem'))
+                try:
+                    theorem = Theorem.query.filter_by(
+                        hash_value=hash_value).one()
+                except NoResultFound:
+                    theorem = Theorem(text=m.group('theorem'),
+                                      hash_value=hash_value)
+                    db.session.add(theorem)
+                    db.session.commit()
                 proof = self.WRAP.format(
-                    url=urlencode(dict(proof=m.group('proofscript').rstrip())),
-                    proof=self._escape(m.group('proofscript')))
+                    url=urlencode(dict(theorem=theorem.id)),
+                    proof=self._escape(theorem.text))
 
                 placeholder = self.markdown.htmlStash.store(proof, safe=True)
                 text = '%s\n%s\n%s' % (text[:m.start()], placeholder,

diff --git a/cockerel/webapp/views/prover/prover.py b/cockerel/webapp/views/prover/prover.py
@@ -13,6 +13,8 @@
     session,
     )
 
+from cockerel.models.schema import Proof, Theorem
+
 prover = Module(__name__)
 
 
@@ -90,10 +92,18 @@ def editor():
                                lineno=lineno)
     else:
         # new proof session so set it up
-        unprocessed = request.args.get('proof', "(* Begin Your Proof Here *)")
+        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=unprocessed,
+                               unprocessed=''.join([text,proof]),
                                lineno=lineno)
diff --git a/coqd/base.py b/coqd/base.py
@@ -1,13 +1,20 @@
+"""
+Base
+~~~~~
+Deals with Coq
+"""
 from multiprocessing import Process
 from pexpect import spawn, EOF
 
 
 class CoqProc(Process):
-
+    """Handles the shell process conncetion"""
     def start(self):
+        """Execs a new child for coqtop"""
         self.process = spawn('coqtop', ['-emacs-U'])
 
     def run(self, conn):
+        """Attempts to connect with the fork and send a command"""
         cmd = ''
         try:
             if conn.poll():
@@ -27,6 +34,7 @@ def alive(self):
         return self.process.isalive()
 
     def terminate(self, Force=False):
+        """Have the child terminate"""
         if Force:
             return self.process.terminate(True)
         else:

diff --git a/coqd/connserv.py b/coqd/connserv.py
@@ -1,4 +1,6 @@
 """
+Connserv
+~~~~~~~~
 Handle protocol for connections
 """
 from json import JSONDecoder, JSONEncoder