Skip to content

Latest commit

 

History

History
34 lines (25 loc) · 1.08 KB

README.md

File metadata and controls

34 lines (25 loc) · 1.08 KB
Raw

coq-lit.py: Literate Coq Blogging

This python script processes special commands inside comments in Coq source files to produce markdown and raw html that generates a blog post. An example may be found here (source).

Dependencies

You'll need:

  • python 3.x
  • jQuery (tested with 2.1.1)
  • jQuery UI (tested with 1.11.1)

Commands

Note: All commands must appear at the very beginning of a line. This includes comment-closing characters.

  • (** begins a blog output comment, ended by *)

  • (*begin code*) begins a block of Coq code to be pretty printed to the blog, ended by (*end code*). Coq code not appearing between such commands will not be printed. (This can be useful for glossing over things such as Undo and Abort.)

  • (*context begins a tooltip (popup) proof context block, ended by *). This captures the line of code following the *) and makes it pop up the given context on hover.