Proviola

The Proviola is a tool set for generating a dynamic (HTML + JavaScript) page out of a Coq proof script. The generated page can be used to display proof states without having the reader load the script into a proof assistant instance, giving a considerable advantage over browsing a repository of static files.

The script below is a minimal example of a movie generated using the Proviola. Point to the tactics to see the proof state after executing that tactic:

Lemma simple_example: forall x, x->x.
1 subgoal

  ============================
   forall x : Type, x -> x

Proof.
 
  intros x H.
1 subgoal

  x : Type
  H : x
  ============================
   x

  exact H.
Proof completed.
  
Qed.
simple_example is defined

This method does not allow the reader to interact with the material directly on the web. This still requires loading the files to a proof assistant. To use the Coq proof assistant without installing it, you might want to consider ProofWeb.

This site consists of three sections:

• To see what the movies can look like, see the examples page.
• Download and installation instructions for the Proviola are on the installation page.
• A short overview of the basic Proviola workflow.

Comments, questions and bugs can be sent directly to me (carst 'at' cs 'dot' ru 'dot' nl), or by posting an issue in the bitbucket repository.