Proviola

Proviola is a tool for creating "proof movies" out of proof scripts, in particular, scripts for the Coq and Isabelle proof assistants, and transforming these movies into "dynamic" HTML pages.

Meta

• Author(s):
  • Carst Tankink (initial)
• Coq-community maintainer(s):
  • Jason Gross (@JasonGross)
• License: GNU General Public License v3.0 or later
• Additional dependencies:
  • lxml library
• Related publication(s):
  • Proviola: a Tool for Proof Re-animation doi:10.1007/978-3-642-14128-7_37

Usage

Run coqdoc on your sources, then run the camera.py script on the generated HTML file. Optionally provide an output file. On the generated xml file (default extension: .flm), run an XSL processor such as xsltproc (linux) to get an HTML page. The default XSL template is proviola/coq/proviola.xsl, which includes the required JavaScript and CSS.

There is a known bug in processing "plain" scripts, not pre-processed by coqdoc.