Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

improvements to prover, better theorem tracking, added docs

  • Loading branch information...
commit 1e05931f1f20208512d85df7a4a10a9c93e5a1bf 1 parent c2c4aa3
@dcolish authored
View
3  .gitignore
@@ -9,4 +9,5 @@ lib64
parsetab.py
parser.out
*.v.d
-*.egg-info
+*.egg-info
+docs/_build
View
10 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 *
View
19 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
View
7 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)
View
3  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>
View
4 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");
View
15 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/<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:
View
21 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,
View
14 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)
View
10 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:
View
2  coqd/connserv.py
@@ -1,4 +1,6 @@
"""
+Connserv
+~~~~~~~~
Handle protocol for connections
"""
from json import JSONDecoder, JSONEncoder
View
96 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:
View
16 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':'
View
4 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)
View
38 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`
+
View
218 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
+# "<project> v<release> 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 <link> 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)
+]
View
26 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
+
+
View
24 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`
+
View
155 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 ^<target^>` where ^<target^> 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
View
12 pavement.py
@@ -14,9 +14,19 @@ def setup():
@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:
View
7 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
View
4 setup.py
@@ -49,6 +49,10 @@
],
},
+ extras_require={
+ 'doc': ['sphinx', 'Sphinx-PyPI-upload'],
+ },
+
install_requires=[
'flask',
'Flask-Markdown==dev',
Please sign in to comment.
Something went wrong with that request. Please try again.