Skip to content

coq-community/coqdocjs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

50 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

CoqdocJS

CoqdocJS is a little script to dynamically improve the coqdoc output. The result can be seen here:

https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html

It offers the following features:

  • Customizable Unicode display: It only changes the display, copy-paste from the website produces pure ASCII. It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes. It does not replace randomly, like in "omega." or "tauto." To add new symbols, edit config.js.
  • Proof hiding: All proofs longer than one line are hidden by default. They can be uncovered by clicking on "Proof...".

All of this works with the ordinary coqdoc, by asking coqdoc to use a header file including the javascript files and some custom CSS.

Usage

  1. Clone this repository as a subdirectory or submodule;
  2. Include Makefile.doc in your Makefile, or copy it as, e.g., Makefile.coq.local;
  3. Run make coqdoc to build documentations.

A minimal example is shown here.

Environment Variables

Name Usage Default
COQDOCFLAGS Override the flags passed to coqdoc see Makefile.doc
COQDOCEXTRAFLAGS Extend the flags passed to coqdoc empty
COQDOCJS_LN If set to true then symlink resource files; otherwise copy false
COQDOCJS_DIR Folder containing CoqdocJS coqdocjs
COQMAKEFILE Makefile generated by coq_makefile Makefile.coq

Files

  • Makefile.doc: a generic Makefile setup that calls coqc and coqdoc with the right parameters
  • 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