12.4 Coq and LATEX

12.4.1 Embedded Coq phrases inside LATEX documents

When writing a documentation about a proof development, one may want to insert Coq phrases inside a LATEX document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such Coq phrases embedded in LATEX files: the coq-tex filter. This filter extracts Coq phrases embedded in LaTeX files, evaluates them, and insert the outcome of the evaluation after each phrase.

Starting with a file file.tex containing Coq phrases, the coq-tex filter produces a file named file.v.tex with the Coq outcome.

There are options to produce the Coq parts in smaller font, italic, between horizontal rules, etc. See the man page of coq-tex for more details.
Remark. This Reference Manual and the Tutorial have been completely produced with coq-tex.

12.4.2 Documenting Coq files with LATEX

coqweb is a ``literate programming'' tool for Coq, inspired by Knuth's WEB tool. The user documents his or her files with LATEX material inside Coq comments and coqweb produces a LATEX document from this unique source. Coq parts are displayed in a nice way (-> becomes ®, keywords are typeset in a bold face, etc.). Additionally, an index is produced which gives the places where the various globals are introduced.

coqweb is developped and distributed independently of the system Coq. It is freely available, with sources, binaries and a full documentation, at www.lri.fr/~filliatr/coqweb.