From 1e05931f1f20208512d85df7a4a10a9c93e5a1bf Mon Sep 17 00:00:00 2001 From: Dan Date: Sat, 7 Aug 2010 10:21:32 -0700 Subject: [PATCH] improvements to prover, better theorem tracking, added docs --- .gitignore | 3 +- MANIFEST.in | 10 + cockerel/models/schema.py | 19 ++ cockerel/webapp/__init__.py | 7 + cockerel/webapp/templates/base.html | 3 +- cockerel/webapp/templates/prover/prover.html | 4 +- cockerel/webapp/views/classes.py | 15 +- cockerel/webapp/views/prover/mdx_prover.py | 21 +- cockerel/webapp/views/prover/prover.py | 14 +- coqd/base.py | 10 +- coqd/connserv.py | 2 + coqd/parser/gram.py | 96 ++++++-- coqd/parser/lexer.py | 16 ++ coqd/runner.py | 4 +- docs/cockerel/index.rst | 38 ++++ docs/conf.py | 218 +++++++++++++++++++ docs/coqd/index.rst | 26 +++ docs/index.rst | 24 ++ docs/make.bat | 155 +++++++++++++ pavement.py | 12 +- setup.cfg | 7 + setup.py | 4 + 22 files changed, 670 insertions(+), 38 deletions(-) create mode 100644 docs/cockerel/index.rst create mode 100644 docs/conf.py create mode 100644 docs/coqd/index.rst create mode 100644 docs/index.rst create mode 100644 docs/make.bat create mode 100644 setup.cfg diff --git a/.gitignore b/.gitignore index a2711a2..4232358 100644 --- a/.gitignore +++ b/.gitignore @@ -9,4 +9,5 @@ lib64 parsetab.py parser.out *.v.d -*.egg-info \ No newline at end of file +*.egg-info +docs/_build \ No newline at end of file diff --git a/MANIFEST.in b/MANIFEST.in index 249bd33..22819bd 100644 --- 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 * \ No newline at end of file diff --git a/cockerel/models/schema.py b/cockerel/models/schema.py index 625db72..b355022 100644 --- 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 '' % 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 index 612d7b2..0c0a81f 100644 --- 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 index 8be97cf..f5102cf 100644 --- a/cockerel/webapp/templates/base.html +++ b/cockerel/webapp/templates/base.html @@ -9,8 +9,7 @@ - + diff --git a/cockerel/webapp/templates/prover/prover.html b/cockerel/webapp/templates/prover/prover.html index e5f1c02..079b554 100644 --- 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 index 4455a08..b5ebe04 100644 --- 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,6 +26,7 @@ @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) @@ -25,6 +34,7 @@ def index(): @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/', 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/', 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/', 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 index 7c9e2dd..7c7add6 100644 --- 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^<{3,})[ ]*\n(?P.*?)' + RE = re.compile(r'(?P^<{3,})[ ]*\n(?P.*?)' '(?P^>{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 index e2ec135..dfebf9e 100644 --- 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 index 8f9c715..1cebeeb 100644 --- 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 index 7518fed..642d487 100644 --- a/coqd/connserv.py +++ b/coqd/connserv.py @@ -1,4 +1,6 @@ """ +Connserv +~~~~~~~~ Handle protocol for connections """ from json import JSONDecoder, JSONEncoder diff --git a/coqd/parser/gram.py b/coqd/parser/gram.py index 1647fe6..53f9166 100644 --- a/coqd/parser/gram.py +++ b/coqd/parser/gram.py @@ -1,3 +1,51 @@ +""" +Gram +____ + +To use import the parser module object like so:: + + from coq.parser.gram import parser + +The grammar for Coqtop interpreter output. Our grammar is the following:: + + S' -> proofst + proofst -> subgoal hyp goal term_prompt + proofst -> subgoal goal term_prompt + proofst -> sysmsg term_prompt + subgoal -> NUMBER SUBGOAL + hyp -> ID COLON PROP hyp + hyp -> ID COLON expr hyp + hyp -> ID COLON PROP + hyp -> ID COLON expr + goal -> GOALINE quantified_expr + goal -> GOALINE expr + quantified_expr -> forall + quantified_expr -> exists + forall -> FORALL idlist COLON ID COMMA expr + forall -> FORALL idlist COLON PROP COMMA expr + exists -> EXISTS idlist COLON ID COMMA expr + expr -> expr IMPL expr + expr -> expr AND expr + expr -> expr OR expr + expr -> expr LARRW expr + expr -> expr RARRW expr + expr -> LPAREN expr RPAREN + expr -> LBRKT expr RBRKT + expr -> idlist + idlist -> ID idlist + idlist -> TILDE idlist + idlist -> PLING idlist + idlist -> ID + term_prompt -> PROMPT proverstate PROMPT + sysmsg -> PROOF idlist DOT + proverstate -> thmname LARRW NUMBER PIPE thmlist NUMBER LARRW + statelist -> PIPE thmlist + thmlist -> thmname PIPE thmlist + thmlist -> thmname PIPE + thmname -> ID + thmname -> ID NUMBER + +""" from ply import yacc from lexer import tokens @@ -6,9 +54,9 @@ def p_proofst(p): - '''proofst : subgoal hyp goal term_prompt + """proofst : subgoal hyp goal term_prompt | subgoal goal term_prompt - | sysmsg term_prompt''' + | sysmsg term_prompt""" if len(p) == 5: p[0] = dict(subgoal=p[1], hyp=p[2], @@ -29,16 +77,16 @@ def p_proofst(p): def p_subgoal(p): - '''subgoal : NUMBER SUBGOAL''' + """subgoal : NUMBER SUBGOAL""" p[0] = ' '.join((str(p[1]), str(p[2]))) def p_hyp(p): - '''hyp : ID COLON PROP hyp + """hyp : ID COLON PROP hyp | ID COLON expr hyp | ID COLON PROP | ID COLON expr - ''' + """ hyp = [dict(name=p[1], type=p[3])] if len(p) == 5: @@ -49,22 +97,22 @@ def p_hyp(p): def p_goal(p): - '''goal : GOALINE quantified_expr + """goal : GOALINE quantified_expr | GOALINE expr - ''' + """ p[0] = p[2] def p_quantified_expr(p): - '''quantified_expr : forall - | exists''' + """quantified_expr : forall + | exists""" p[0] = dict(quantified_expr=p[1]) def p_forall(p): - '''forall : FORALL idlist COLON ID COMMA expr + """forall : FORALL idlist COLON ID COMMA expr | FORALL idlist COLON PROP COMMA expr - ''' + """ p[0] = dict(quantifier=p[1], identifiers=p[2], type=p[4], @@ -72,8 +120,8 @@ def p_forall(p): def p_exists(p): - '''exists : EXISTS idlist COLON ID COMMA expr - ''' + """exists : EXISTS idlist COLON ID COMMA expr + """ p[0] = dict(quantifier=p[1], identifiers=p[2], type=p[4], @@ -81,7 +129,7 @@ def p_exists(p): def p_expr(p): - '''expr : expr IMPL expr + """expr : expr IMPL expr | expr AND expr | expr OR expr | expr LARRW expr @@ -89,7 +137,7 @@ def p_expr(p): | LPAREN expr RPAREN | LBRKT expr RBRKT | idlist - ''' + """ if len(p) == 2 and p[1] is not None: p[0] = str(p[1]) elif len(p) == 4: @@ -102,11 +150,11 @@ def p_expr(p): def p_idlist(p): - '''idlist : ID idlist + """idlist : ID idlist | TILDE idlist | PLING idlist | ID - ''' + """ if len(p) == 3: p[0] = ' '.join((str(p[1]), str(p[2]))) else: @@ -114,26 +162,26 @@ def p_idlist(p): def p_term_prompt(p): - '''term_prompt : PROMPT proverstate PROMPT''' + """term_prompt : PROMPT proverstate PROMPT""" p[0] = dict(thm=p[2], thmstate=p[3]) def p_sysmsg(p): - '''sysmsg : PROOF idlist DOT''' + """sysmsg : PROOF idlist DOT""" p[0] = dict(msg=p[2]) def p_proverstate(p): - '''proverstate : thmname LARRW NUMBER PIPE thmlist NUMBER LARRW''' + """proverstate : thmname LARRW NUMBER PIPE thmlist NUMBER LARRW""" p[0] = dict(proverline=p[2], thmname=p[3], thmlin=p[4]) def p_thmlist(p): - '''thmlist : thmname PIPE thmlist - | thmname PIPE''' + """thmlist : thmname PIPE thmlist + | thmname PIPE""" if len(p) == 4: p[0] = dict(names=' ,'.join((p[1], p[3]))) else: @@ -141,8 +189,8 @@ def p_thmlist(p): def p_thmname(p): - '''thmname : ID - | ID NUMBER''' + """thmname : ID + | ID NUMBER""" if len(p) == 2: p[0] = p[1] else: diff --git a/coqd/parser/lexer.py b/coqd/parser/lexer.py index 994ae63..d92d832 100644 --- a/coqd/parser/lexer.py +++ b/coqd/parser/lexer.py @@ -1,3 +1,17 @@ +""" +Lexer +----- +Token definitons for the Coqtop Output Language. + +.. warning:: It is not meant to be used on its own and will not provide a useful + language + +To use import the tokens object:: + + from coqd.parser.lexer import tokens + +""" + from ply import lex t_ignore = ' \t' @@ -47,6 +61,7 @@ def t_ID(t): + """Ensure that reserved words are not overwritten with ID's""" r'[a-zA-Z_][a-zA-Z_0-9\']*' t.type = reserved.get(t.value, 'ID') # Check for reserved words return t @@ -79,6 +94,7 @@ def t_newline(t): r'\n+' t.lexer.lineno += len(t.value) + t_OR = r'\\/' t_CARET = r'\^' t_COLON = r':' diff --git a/coqd/runner.py b/coqd/runner.py index 112466d..0847fdf 100644 --- a/coqd/runner.py +++ b/coqd/runner.py @@ -1,4 +1,6 @@ """ +Runner +~~~~~~ Main entry points for coqd """ # from argparse import ArgumentParser @@ -14,7 +16,7 @@ class Configurator(SafeConfigParser): - """Responsible or coqd configuration""" + """Responsible for coqd configuration""" def __init__(self, config_files): self.conf = SafeConfigParser() self.conf.read(config_files) diff --git a/docs/cockerel/index.rst b/docs/cockerel/index.rst new file mode 100644 index 0000000..5bb65aa --- /dev/null +++ b/docs/cockerel/index.rst @@ -0,0 +1,38 @@ +Cockerel +==================================== +The main web application + +API Reference +------------- + +.. automodule:: cockerel.webapp + :members: + +.. automodule:: cockerel.webapp.views.admin + :members: + +.. automodule:: cockerel.webapp.views.classes + :members: + +.. automodule:: cockerel.webapp.views.frontend + :members: + +.. automodule:: cockerel.webapp.views.lessons + :members: + +.. automodule:: cockerel.webapp.views.prover.mdx_prover + :members: + +.. automodule:: cockerel.webapp.views.prover.prover + :members: + +.. automodule:: cockerel.webapp.views.util + :members: + +Indices and tables +------------------ + +* :ref:`genindex` +* :ref:`modindex` +* :ref:`search` + diff --git a/docs/conf.py b/docs/conf.py new file mode 100644 index 0000000..7317c41 --- /dev/null +++ b/docs/conf.py @@ -0,0 +1,218 @@ +# -*- coding: utf-8 -*- +# +# Cockerel documentation build configuration file, created by +# sphinx-quickstart on Sat Aug 7 08:24:55 2010. +# +# This file is execfile()d with the current directory set to its containing dir. +# +# Note that not all possible configuration values are present in this +# autogenerated file. +# +# All configuration values have a default; values that are commented out +# serve to show the default. + +import sys, os + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. + +sys.path.append(os.path.abspath('_themes')) +sys.path.append(os.path.abspath('..')) + +# -- General configuration ----------------------------------------------------- + +# If your documentation needs a minimal Sphinx version, state it here. +#needs_sphinx = '1.0' + +# Add any Sphinx extension module names here, as strings. They can be extensions +# coming with Sphinx (named 'sphinx.ext.*') or your custom ones. +extensions = ['sphinx.ext.autodoc'] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ['_templates'] + +# The suffix of source filenames. +source_suffix = '.rst' + +# The encoding of source files. +#source_encoding = 'utf-8-sig' + +# The master toctree document. +master_doc = 'index' + +# General information about the project. +project = u'Cockerel' +copyright = u'2010, Dan Colish' + +# The version info for the project you're documenting, acts as replacement for +# |version| and |release|, also used in various other places throughout the +# built documents. +# +# The short X.Y version. +version = '0.1' +# The full version, including alpha/beta/rc tags. +release = '0.1' + +# The language for content autogenerated by Sphinx. Refer to documentation +# for a list of supported languages. +#language = None + +# There are two options for replacing |today|: either, you set today to some +# non-false value, then it is used: +#today = '' +# Else, today_fmt is used as the format for a strftime call. +#today_fmt = '%B %d, %Y' + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +exclude_patterns = ['_build'] + +# The reST default role (used for this markup: `text`) to use for all documents. +#default_role = None + +# If true, '()' will be appended to :func: etc. cross-reference text. +#add_function_parentheses = True + +# If true, the current module name will be prepended to all description +# unit titles (such as .. function::). +#add_module_names = True + +# If true, sectionauthor and moduleauthor directives will be shown in the +# output. They are ignored by default. +#show_authors = False + +# The name of the Pygments (syntax highlighting) style to use. +pygments_style = 'sphinx' + +# A list of ignored prefixes for module index sorting. +#modindex_common_prefix = [] + + +# -- Options for HTML output --------------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +html_theme = 'default' + +# Theme options are theme-specific and customize the look and feel of a theme +# further. For a list of options available for each theme, see the +# documentation. +#html_theme_options = {} + +# Add any paths that contain custom themes here, relative to this directory. +#html_theme_path = [] + +# The name for this set of Sphinx documents. If None, it defaults to +# " v documentation". +#html_title = None + +# A shorter title for the navigation bar. Default is the same as html_title. +#html_short_title = None + +# The name of an image file (relative to this directory) to place at the top +# of the sidebar. +#html_logo = None + +# The name of an image file (within the static path) to use as favicon of the +# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32 +# pixels large. +#html_favicon = None + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ['_static'] + +# If not '', a 'Last updated on:' timestamp is inserted at every page bottom, +# using the given strftime format. +#html_last_updated_fmt = '%b %d, %Y' + +# If true, SmartyPants will be used to convert quotes and dashes to +# typographically correct entities. +#html_use_smartypants = True + +# Custom sidebar templates, maps document names to template names. +#html_sidebars = {} + +# Additional templates that should be rendered to pages, maps page names to +# template names. +#html_additional_pages = {} + +# If false, no module index is generated. +#html_domain_indices = True + +# If false, no index is generated. +#html_use_index = True + +# If true, the index is split into individual pages for each letter. +#html_split_index = False + +# If true, links to the reST sources are added to the pages. +#html_show_sourcelink = True + +# If true, "Created using Sphinx" is shown in the HTML footer. Default is True. +#html_show_sphinx = True + +# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True. +#html_show_copyright = True + +# If true, an OpenSearch description file will be output, and all pages will +# contain a tag referring to it. The value of this option must be the +# base URL from which the finished HTML is served. +#html_use_opensearch = '' + +# This is the file name suffix for HTML files (e.g. ".xhtml"). +#html_file_suffix = None + +# Output file base name for HTML help builder. +htmlhelp_basename = 'Cockereldoc' + + +# -- Options for LaTeX output -------------------------------------------------- + +# The paper size ('letter' or 'a4'). +#latex_paper_size = 'letter' + +# The font size ('10pt', '11pt' or '12pt'). +#latex_font_size = '10pt' + +# Grouping the document tree into LaTeX files. List of tuples +# (source start file, target name, title, author, documentclass [howto/manual]). +latex_documents = [ + ('index', 'Cockerel.tex', u'Cockerel Documentation', + u'Dan Colish', 'manual'), +] + +# The name of an image file (relative to this directory) to place at the top of +# the title page. +#latex_logo = None + +# For "manual" documents, if this is true, then toplevel headings are parts, +# not chapters. +#latex_use_parts = False + +# If true, show page references after internal links. +#latex_show_pagerefs = False + +# If true, show URL addresses after external links. +#latex_show_urls = False + +# Additional stuff for the LaTeX preamble. +#latex_preamble = '' + +# Documents to append as an appendix to all manuals. +#latex_appendices = [] + +# If false, no module index is generated. +#latex_domain_indices = True + + +# -- Options for manual page output -------------------------------------------- + +# One entry per manual page. List of tuples +# (source start file, name, description, authors, manual section). +man_pages = [ + ('index', 'cockerel', u'Cockerel Documentation', + [u'Dan Colish'], 1) +] diff --git a/docs/coqd/index.rst b/docs/coqd/index.rst new file mode 100644 index 0000000..54bc61b --- /dev/null +++ b/docs/coqd/index.rst @@ -0,0 +1,26 @@ +Coqd: Coqtop Server +==================================== +Coqd allows you to connect with a coqtop interactive session + + +API Reference +------------- + +.. automodule:: coqd + :members: + +.. automodule:: coqd.base + :members: + +.. automodule:: coqd.connserv + :members: + +.. automodule:: coqd.runner + :members: + +.. automodule:: coqd.parser.gram + :members: + +.. automodule:: coqd.parser.lexer + + diff --git a/docs/index.rst b/docs/index.rst new file mode 100644 index 0000000..5e77de2 --- /dev/null +++ b/docs/index.rst @@ -0,0 +1,24 @@ +Welcome to Cockerel's documentation! +==================================== + +Cockerel is a prover, a lesson planner, and a companion for all education in all areas of mathematics. My experience in mathematical education is only as a student, however it has shown me that no good tools exist for providing a long distance interactive experience. Students have to deal with a system the expects perfection and understanding without any feedback and little to no motivation beyond the threat of failure. + +Cockerel is different. It provides an environment that is easy for instructors and students to use by focusing solely on lesson planning. Each class has a number of lesson plans associated with it. The lesson plan is simply a wiki document that instructors can use however they like. By providing any questions and proofs in-line with the instruction, students will have clear references for all their assignments. Additionally, each question or theorem, will be a clickable link to a prover in which the students can complete the questions. + +Contents +-------- + +.. toctree:: + :maxdepth: 2 + + cockerel/index + coqd/index + + +Indices and tables +------------------ + +* :ref:`genindex` +* :ref:`modindex` +* :ref:`search` + diff --git a/docs/make.bat b/docs/make.bat new file mode 100644 index 0000000..25fe194 --- /dev/null +++ b/docs/make.bat @@ -0,0 +1,155 @@ +@ECHO OFF + +REM Command file for Sphinx documentation + +if "%SPHINXBUILD%" == "" ( + set SPHINXBUILD=sphinx-build +) +set BUILDDIR=_build +set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% . +if NOT "%PAPER%" == "" ( + set ALLSPHINXOPTS=-D latex_paper_size=%PAPER% %ALLSPHINXOPTS% +) + +if "%1" == "" goto help + +if "%1" == "help" ( + :help + echo.Please use `make ^` where ^ is one of + echo. html to make standalone HTML files + echo. dirhtml to make HTML files named index.html in directories + echo. singlehtml to make a single large HTML file + echo. pickle to make pickle files + echo. json to make JSON files + echo. htmlhelp to make HTML files and a HTML help project + echo. qthelp to make HTML files and a qthelp project + echo. devhelp to make HTML files and a Devhelp project + echo. epub to make an epub + echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter + echo. text to make text files + echo. man to make manual pages + echo. changes to make an overview over all changed/added/deprecated items + echo. linkcheck to check all external links for integrity + echo. doctest to run all doctests embedded in the documentation if enabled + goto end +) + +if "%1" == "clean" ( + for /d %%i in (%BUILDDIR%\*) do rmdir /q /s %%i + del /q /s %BUILDDIR%\* + goto end +) + +if "%1" == "html" ( + %SPHINXBUILD% -b html %ALLSPHINXOPTS% %BUILDDIR%/html + echo. + echo.Build finished. The HTML pages are in %BUILDDIR%/html. + goto end +) + +if "%1" == "dirhtml" ( + %SPHINXBUILD% -b dirhtml %ALLSPHINXOPTS% %BUILDDIR%/dirhtml + echo. + echo.Build finished. The HTML pages are in %BUILDDIR%/dirhtml. + goto end +) + +if "%1" == "singlehtml" ( + %SPHINXBUILD% -b singlehtml %ALLSPHINXOPTS% %BUILDDIR%/singlehtml + echo. + echo.Build finished. The HTML pages are in %BUILDDIR%/singlehtml. + goto end +) + +if "%1" == "pickle" ( + %SPHINXBUILD% -b pickle %ALLSPHINXOPTS% %BUILDDIR%/pickle + echo. + echo.Build finished; now you can process the pickle files. + goto end +) + +if "%1" == "json" ( + %SPHINXBUILD% -b json %ALLSPHINXOPTS% %BUILDDIR%/json + echo. + echo.Build finished; now you can process the JSON files. + goto end +) + +if "%1" == "htmlhelp" ( + %SPHINXBUILD% -b htmlhelp %ALLSPHINXOPTS% %BUILDDIR%/htmlhelp + echo. + echo.Build finished; now you can run HTML Help Workshop with the ^ +.hhp project file in %BUILDDIR%/htmlhelp. + goto end +) + +if "%1" == "qthelp" ( + %SPHINXBUILD% -b qthelp %ALLSPHINXOPTS% %BUILDDIR%/qthelp + echo. + echo.Build finished; now you can run "qcollectiongenerator" with the ^ +.qhcp project file in %BUILDDIR%/qthelp, like this: + echo.^> qcollectiongenerator %BUILDDIR%\qthelp\Cockerel.qhcp + echo.To view the help file: + echo.^> assistant -collectionFile %BUILDDIR%\qthelp\Cockerel.ghc + goto end +) + +if "%1" == "devhelp" ( + %SPHINXBUILD% -b devhelp %ALLSPHINXOPTS% %BUILDDIR%/devhelp + echo. + echo.Build finished. + goto end +) + +if "%1" == "epub" ( + %SPHINXBUILD% -b epub %ALLSPHINXOPTS% %BUILDDIR%/epub + echo. + echo.Build finished. The epub file is in %BUILDDIR%/epub. + goto end +) + +if "%1" == "latex" ( + %SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex + echo. + echo.Build finished; the LaTeX files are in %BUILDDIR%/latex. + goto end +) + +if "%1" == "text" ( + %SPHINXBUILD% -b text %ALLSPHINXOPTS% %BUILDDIR%/text + echo. + echo.Build finished. The text files are in %BUILDDIR%/text. + goto end +) + +if "%1" == "man" ( + %SPHINXBUILD% -b man %ALLSPHINXOPTS% %BUILDDIR%/man + echo. + echo.Build finished. The manual pages are in %BUILDDIR%/man. + goto end +) + +if "%1" == "changes" ( + %SPHINXBUILD% -b changes %ALLSPHINXOPTS% %BUILDDIR%/changes + echo. + echo.The overview file is in %BUILDDIR%/changes. + goto end +) + +if "%1" == "linkcheck" ( + %SPHINXBUILD% -b linkcheck %ALLSPHINXOPTS% %BUILDDIR%/linkcheck + echo. + echo.Link check complete; look for any errors in the above output ^ +or in %BUILDDIR%/linkcheck/output.txt. + goto end +) + +if "%1" == "doctest" ( + %SPHINXBUILD% -b doctest %ALLSPHINXOPTS% %BUILDDIR%/doctest + echo. + echo.Testing of doctests in the sources finished, look at the ^ +results in %BUILDDIR%/doctest/output.txt. + goto end +) + +:end diff --git a/pavement.py b/pavement.py index cbd2927..0d77cbb 100644 --- a/pavement.py +++ b/pavement.py @@ -13,10 +13,20 @@ def setup(): print "Ready to boot servers" +@task +@needs('clean_pyc') +def clean_all(): + for area in 'cockerel', 'coqd': + for dir, _, files in os.walk(area): + for fn in files: + if fn.endswith('.pyc'): + path(dir + '/' + fn).unlink() + + @task def clean_pyc(): """Remove orphaned .pyc files.""" - for area in 'idealist', 'test', 'test2': + for area in 'cockerel', 'coqd': for dir, _, files in os.walk(area): sources = set(fn for fn in files if fn.endswith('.py')) for fn in files: diff --git a/setup.cfg b/setup.cfg new file mode 100644 index 0000000..9b99664 --- /dev/null +++ b/setup.cfg @@ -0,0 +1,7 @@ +[build_sphinx] +source-dir = docs/ +build-dir = docs/_build +all_files = 1 + +[upload_sphinx] +upload-dir = docs/_build/html diff --git a/setup.py b/setup.py index ee13eba..b2a89ac 100644 --- a/setup.py +++ b/setup.py @@ -49,6 +49,10 @@ ], }, + extras_require={ + 'doc': ['sphinx', 'Sphinx-PyPI-upload'], + }, + install_requires=[ 'flask', 'Flask-Markdown==dev',