Cockerel

The main web application

System Overview

Pre-Requisites

The Cockerel system is simple to install provided you have the following requirements satisfied:

• Ocaml >= 3.11
• Coq >= 8.2pl1
• Python >= 2.6
• Virtualenv
• Pip

For information on installing these see their respective sites.

Installation

I strongly recommend using the virtualenv project for managing the python namespace. Assuming you have a project python install with setuptools, you can create a new virtualenv around the project directory to install into. This can be done with:

git clone git://github.com/dcolish/Cockerel.git

Then

virtualenv some_env_path . some_env_path/bin/activate python setup.py develop

To start Cockerel run

cockerel

To start Coqd run

coqd

The Cockerel webpage will be at http://localhost:5000 by default

API Reference

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.

cockerel.webapp.update_config()

syncronizes the config with the g global request object

classes.py

Controller functions for classes. A class object allows you to add associated lesson plans.

cockerel.webapp.views.classes.add(*args, **kwargs)

Users can add classes if they are authenticated

cockerel.webapp.views.classes.edit(*args, **kwargs)

Make modifications to a class

cockerel.webapp.views.classes.index()

Shows all classes currently in the system

cockerel.webapp.views.classes.register(*args, **kwargs)

As a student user, register for access to a class

cockerel.webapp.views.classes.view(class_id)

View the lesson plans offered by a specific class. The user must be either the admin or registered for that class

Prover Extension for Python-Markdown

Added parsing of Theorems to Python-Markdown.

A simple example:

<<< Goal True -> True. >>>

class cockerel.webapp.views.prover.mdx_prover.ProverExtension(configs={})

Add definition lists to Markdown.

extendMarkdown(md, md_globals)

Add an instance of ProverPreprocessor to Markdown.

class cockerel.webapp.views.prover.mdx_prover.ProverPreprocessor(md)

Process Theorem.

cockerel.webapp.views.prover.mdx_prover.makeExtension

alias of ProverExtension

cockerel.webapp.views.prover.prover.readscript(script)

Chew up blank lines

Indices and tables

• Index
• Module Index
• Search Page