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:

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.