CoqdocJS for coq-community

This project provides a collection of scripts to improve the HTML output of the coqdoc tool bundled with the Coq proof assistant.

The scripts are derived from CoqdocJS, but are tailored for the needs of coq-community projects. The results of using the scripts can be seen here: https://coq-community.github.io/huffman/docs/latest/coqdoc/Huffman.Huffman.html

The scripts provide the following features:

• Customizable Unicode display:
  • It only changes the display; copy-paste from the HTML produces pure ASCII
  • It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes
  • It does not replace randomly, e.g., in omega or tauto
  • To add new symbols, edit config.js
• Proof hiding:
  • All proofs longer than one line are hidden by default, and can be uncovered by clicking on Proof
  • All proofs can be shown at once (or hidden again)

All of this works with the ordinary coqdoc by configuring it to use a custom header file including the required JavasScript code and some custom CSS.

Usage

Copy Makefile.coq.local into your Coq project (assuming the file generated by coq_makefile is named Makefile.coq, otherwise rename the file appropriately). Next, copy the resources directory into your project.

You should then be able to run the following command to generate coqdoc documentation in the directory defined by the COQDOCDIR variable (docs/coqdoc by default):

make -f Makefile.coq coqdoc

or just

make coqdoc

if your main Makefile defers tasks to Makefile.coq.

Files

• Makefile.coq.local: Makefile tasks for generating GitHub-friendly documentation
• config.js: contains the unicode replacement table
• coqdoc.css: a replacement for the default coqdoc CSS style. Can be removed to use the default style
• coqdocjs.js and coqdocjs.css: the script rewriting the DOM and adding the dynamic features with a corresponding CSS style
• header.html and footer.html: custom header and footer files used in every generated html file