coqdoc: a documentation tool for Coq

Jean-Christophe Filliâtre
http://www.lri.fr/~filliatr/coqdoc

Table of Contents

1  Introduction

1. to produce a nice L^AT_EX and/or HTML document from the Coq sources, readable for a human and not only for the proof assistant;
2. to help the user navigating in his own (or third-party) sources.

2  Principles

Coq material inside documentation.

Pretty-printing.

(** printing token %...LATEX...% #...HTML...# *)

(** printing token $...LATEX math...$ #...HTML...# *)

(** remove printing token *)

(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)

Sections.

    (** * Well-founded relations
  
        In this section, we introduce...  *)

Lists.

    This module defines
        - the predecessor [pred]
        - the addition [plus]
        - order relations:
          -- less or equal [le]
          -- less [lt]

Rules.

Escapings to L^AT_EX and HTML.

• $...LaTeX stuff...$ inserts some L^AT_EX material in math mode. Simply discarded in HTML output.
  
  
• %...LaTeX stuff...% inserts some L^AT_EX material. Simply discarded in HTML output.
  
  
• #...HTML stuff...# inserts some HTML material. Simply discarded in L^AT_EX output.

Verbatim.

Here is the corresponding caml code:
<<
  let rec fact n = 
    if n <= 1 then 1 else n * fact (n-1)
>>

Hyperlinks.

Hiding / Showing parts of the source.

(* begin hide *)
some Coq material
(* end hide *)

(* begin show *)
some Coq material
(* end show *)

3  Usage

HTML output

 

This is the default output. One HTML file is created for each Coq file given on the command line, together with a file index.html (unless option -no-index is passed). The HTML pages use a style sheet named style.css. Such a file is distributed with coqdoc.

L^AT_EX output

 

A single L^AT_EX file is created, on standard output. It can be redirected to a file with option -o. The order of files on the command line is kept in the final document. L^AT_EX files given on the command line are copied `as is' in the final document . DVI and PostScript can be produced directly with the options -dvi and -ps respectively.

TeXmacs output

 

To translate the input files to TeXmacs format, to be used by the TeXmacs Coq interface (see http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/).

Command line options

Overall options

--html

 

Select a HTML output.

--latex

 

Select a L^AT_EX output.

--dvi

 

Select a DVI output.

--ps

 

Select a PostScript output.

--texmacs

 

Select a TeXmacs output.

-o file, --output file

 

Redirect the output into the file `file' (meaningless with -html).

-d dir, --directory dir

 

Output files into directory `dir' instead of current directory (option -d does not change the filename specified with option -o, if any).

-s , --short

 

Do not insert titles for the files. The default behavior is to insert a title like ``Library Foo'' for each file.

-t string, --title string

 

Set the document title.

--body-only

 

Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one.

-p string, --preamble string

 

Insert some material in the L^AT_EX preamble, right before \begin{document} (meaningless with -html).

--vernac-file file, --tex-file file

 

Considers the file `file' respectively as a .v (or .g) file or a .tex file.

--files-from file

 

Read file names to process in file `file' as if they were given on the command line. Useful for program sources splitted in several directories.

-q, --quiet

 

Be quiet. Do not print anything except errors.

-h, --help

 

Give a short summary of the options and exit.

-v, --version

 

Print the version and exit.

Index options

--no-index

 

Do not output the index.

--multi-index

 

Generate one page for each category and each letter in the index, together with a top page index.html.

Table of contents option

-toc, --table-of-contents

 

Insert a table of contents. For a L^AT_EX output, it inserts a \tableofcontents at the beginning of the document. For a HTML output, it builds a table of contents into toc.html.

Hyperlinks options

--glob-from file

 

Make references using Coq globalizations from file file. (Such globalizations are obtained with Coq option -dump-glob).

--no-externals

 

Do not insert links to the Coq standard library.

--coqlib url

 

Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).

-R dir coqdir

 

Map physical directory dir to Coq logical directory coqdir (similarly to Coq option -R).

Note: option -R only has effect on the files following it on the command line, so you will probably need to put this option first.

Contents options

-g, --gallina

 

Do not print proofs.

-l, --light

 

Light mode. Suppress proofs (as with -g) and the following commands:

• [Recursive] Tactic Definition
• Hint / Hints
• Require
• Transparent / Opaque
• Implicit Argument / Implicits
• Section / Variable / Hypothesis / End

Language options

-latin1, --latin1

 

Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1.

-utf8, --utf8

 

Select UTF-8 (Unicode) input files. It is equivalent to --inputenc utf8 --charset utf-8. L^AT_EX UTF-8 support can be found at http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc string

 

Give a L^AT_EX input encoding, as an option to L^AT_EX package inputenc.

--charset string

 

Specify the HTML character set, to be inserted in the HTML header.

4  The coqdoc L^AT_EX style file

\usepackage{coqdoc}

coqdockw, coqdocid

 

The one-argument macros for typesetting keywords and identifiers. Defaults are sans-serif for keywords and italic for identifiers.

For example, if you would like a slanted font for keywords, you may insert

     \renewcommand{\coqdockw}[1]{\textsl{#1}}

anywhere between \usepackage{coqdoc} and \begin{document}.

coqdocmodule

 

One-argument macro for typesetting the title of a .v file. Default is

\newcommand{\coqdocmodule}[1]{\section*{Module #1}}

and you may redefine it using \renewcommand.

This document was translated from L^AT_EX by H^EV^EA.