Split coqdoc section out of utility chapter (octopus merge).

This octopus merge is meant to preserve the commit history / blame of
both parts.

2 files changed, 464 insertions, 0 deletions

diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
new file mode 100644
index 0000000000..cada680895
--- /dev/null
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -0,0 +1,463 @@
+.. _coqdoc:
+
+Documenting |Coq| files with coqdoc
+-----------------------------------
+
+coqdoc is a documentation tool for the proof assistant |Coq|, similar to
+``javadoc`` or ``ocamldoc``. The task of coqdoc is
+
+
+#. to produce a nice |Latex| and/or HTML document from |Coq| source files,
+   readable for a human and not only for the proof assistant;
+#. to help the user navigate his own (or third-party) sources.
+
+
+
+Principles
+~~~~~~~~~~
+
+Documentation is inserted into |Coq| files as *special comments*. Thus
+your files will compile as usual, whether you use coqdoc or not. coqdoc
+presupposes that the given |Coq| files are well-formed (at least
+lexically). Documentation starts with ``(**``, followed by a space, and
+ends with ``*)``. The documentation format is inspired by Todd
+A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with
+some syntax-light controls, described below. coqdoc is robust: it
+shouldn’t fail, whatever the input is. But remember: “garbage in,
+garbage out”.
+
+
+|Coq| material inside documentation.
+++++++++++++++++++++++++++++++++++++
+
+|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets
+may be nested, the inner ones being understood as being part of the
+quoted code (thus you can quote a term like ``fun x => u`` by writing  ``[fun
+x => u]``). Inside quotations, the code is pretty-printed in the same
+way as it is in code parts.
+
+Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be
+followed by a newline and the latter must follow a newline.
+
+
+Pretty-printing.
+++++++++++++++++
+
+coqdoc uses different faces for identifiers and keywords. The pretty-
+printing of |Coq| tokens (identifiers or symbols) can be controlled
+using one of the following commands:
+
+::
+
+
+    (** printing  *token* %...LATEX...% #...html...# *)
+
+
+or
+
+::
+
+
+    (** printing  *token* $...LATEX math...$ #...html...# *)
+
+
+It gives the |Latex| and HTML texts to be produced for the given |Coq|
+token. Either the |Latex| or the HTML rule may be omitted, causing the
+default pretty-printing to be used for this token.
+
+The printing for one token can be removed with
+
+::
+
+
+    (** remove printing  *token* *)
+
+
+Initially, the pretty-printing table contains the following mapping:
+
+===== === ==== ===== === ==== ==== ===
+`->`   →       `<-`   ←       `*`   ×
+`<=`   ≤       `>=`   ≥       `=>`  ⇒
+`<>`   ≠       `<->`  ↔       `|-`  ⊢
+`\\/`  ∨       `/\\`  ∧       `~`   ¬
+===== === ==== ===== === ==== ==== ===
+
+Any of these can be overwritten or suppressed using the printing
+commands.
+
+.. note::
+
+   The recognition of tokens is done by a (``ocaml``) lex
+   automaton and thus applies the longest-match rule. For instance, `->~`
+   is recognized as a single token, where |Coq| sees two tokens. It is the
+   responsibility of the user to insert space between tokens *or* to give
+   pretty-printing rules for the possible combinations, e.g.
+
+   ::
+
+      (** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
+
+
+
+Sections
+++++++++
+
+Sections are introduced by 1 to 4 asterisks at the beginning of a line
+followed by a space and the title of the section. One asterisk is a section,
+two a subsection, etc.
+
+.. example::
+
+   ::
+
+          (** * Well-founded relations
+
+              In this section, we introduce...  *)
+
+
+Lists.
+++++++
+
+List items are introduced by a leading dash. coqdoc uses whitespace to
+determine the depth of a new list item and which text belongs in which
+list items. A list ends when a line of text starts at or before the
+level of indenting of the list’s dash. A list item’s dash must always
+be the first non-space character on its line (so, in particular, a
+list can not begin on the first line of a comment - start it on the
+second line instead).
+
+.. example::
+
+  ::
+
+           We go by induction on [n]:
+           - If [n] is 0...
+           - If [n] is [S n'] we require...
+
+             two paragraphs of reasoning, and two subcases:
+
+             - In the first case...
+             - In the second case...
+
+           So the theorem holds.
+
+
+
+Rules.
+++++++
+
+More than 4 leading dashes produce a horizontal rule.
+
+
+Emphasis.
++++++++++
+
+Text can be italicized by enclosing it in underscores. A non-identifier
+character must precede the leading underscore and follow the trailing
+underscore, so that uses of underscores in names aren’t mistaken for
+emphasis. Usually, these are spaces or punctuation.
+
+::
+
+        This sentence contains some _emphasized text_.
+
+
+
+Escaping to |Latex| and HTML.
++++++++++++++++++++++++++++++++
+
+Pure |Latex| or HTML material can be inserted using the following
+escape sequences:
+
+
++ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode.
+  Simply discarded in HTML output.
++ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply
+  discarded in HTML output.
++ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in
+  |Latex| output.
+
+.. note::
+  to simply output the characters ``$``, ``%`` and ``#`` and escaping
+  their escaping role, these characters must be doubled.
+
+
+Verbatim
+++++++++
+
+Verbatim material is introduced by a leading ``<<`` and closed by ``>>``
+at the beginning of a line.
+
+.. example::
+
+  ::
+
+      Here is the corresponding caml code:
+      <<
+        let rec fact n =
+          if n <= 1 then 1 else n * fact (n-1)
+      >>
+
+
+
+Hyperlinks
+++++++++++
+
+Hyperlinks can be inserted into the HTML output, so that any
+identifier is linked to the place of its definition.
+
+``coqc file.v`` automatically dumps localization information in
+``file.glob`` or appends it to a file specified using the option ``--dump-glob
+file``. Take care of erasing this global file, if any, when starting
+the whole compilation process.
+
+Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look
+for name resolutions in the file ``file`` (it will look in ``file.glob``
+by default).
+
+Identifiers from the |Coq| standard library are linked to the Coq website
+`<http://coq.inria.fr/library/>`_. This behavior can be changed
+using command line options ``--no-externals`` and ``--coqlib``; see below.
+
+
+Hiding / Showing parts of the source.
++++++++++++++++++++++++++++++++++++++
+
+Some parts of the source can be hidden using command line options ``-g``
+and ``-l`` (see below), or using such comments:
+
+::
+
+
+    (* begin hide *)
+     *some Coq material*
+    (* end hide *)
+
+
+Conversely, some parts of the source which would be hidden can be
+shown using such comments:
+
+::
+
+
+    (* begin show *)
+     *some Coq material*
+    (* end show *)
+
+
+The latter cannot be used around some inner parts of a proof, but can
+be used around a whole proof.
+
+
+Usage
+~~~~~
+
+coqdoc is invoked on a shell command line as follows:
+``coqdoc <options and files>``.
+Any command line argument which is not an option is considered to be a
+file (even if it starts with a ``-``). |Coq| files are identified by the
+suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
+
+
+:HTML output: This is the default output format. 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.
+:|Latex| output: A single |Latex| file is created, on standard
+  output. It can be redirected to a file using the option ``-o``. The order of
+  files on the command line is kept in the final document. |Latex|
+  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.
+
+
+
+Command line options
+++++++++++++++++++++
+
+
+**Overall options**
+
+
+  :--HTML: Select a HTML output.
+  :--|Latex|: Select a |Latex| output.
+  :--dvi: Select a DVI output.
+  :--ps: Select a PostScript output.
+  :--texmacs: Select a TEXmacs output.
+  :--stdout: Write output to stdout.
+  :-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
+    the current directory (option ``-d`` does not change the filename specified
+    with the option ``-o``, if any).
+  :--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 |Latex|
+    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 filenames to be processed from the file ‘file’ as if
+    they were given on the command line. Useful for program sources split
+    up into 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**
+
+  The default behavior is to build an index, for the HTML output only,
+  into ``index.html``.
+
+  :--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``.
+  :--index string: Make the filename of the index string instead of
+    “index”. Useful since “index.html” is special.
+
+
+
+**Table of contents option**
+
+  :-toc, --table-of-contents: Insert a table of contents. For a |Latex|
+    output, it inserts a ``\tableofcontents`` at the beginning of the
+    document. For a HTML output, it builds a table of contents into
+    ``toc.html``.
+  :--toc-depth int: Only include headers up to depth ``int`` in the table of
+    contents.
+
+
+**Hyperlink 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.
+  :--external url coqdir: Use given URL for linking references whose
+    name starts with prefix ``coqdir``.
+  :--coqlib url: Set base URL for the Coq standard library (default is
+    `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url
+    Coq``.
+  :-R dir coqdir: Recursively map physical directory dir to |Coq| logical
+    directory  ``coqdir`` (similarly to |Coq| option ``-R``).
+  :-Q dir coqdir: Map physical directory dir to |Coq| logical
+    directory  ``coqdir`` (similarly to |Coq| option ``-Q``).
+
+    .. note::
+
+       options ``-R`` and ``-Q`` only have
+       effect on the files *following* them on the command line, so you will
+       probably need to put this option first.
+
+
+**Title options**
+
+  :-s , --short: Do not insert titles for the files. The default
+     behavior is to insert a title like “Library Foo” for each file.
+  :--lib-name string: Print “string Foo” instead of “Library Foo” in
+     titles. For example “Chapter” and “Module” are reasonable choices.
+  :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles.
+  :--lib-subtitles: Look for library subtitles. When enabled, the
+     beginning of each file is checked for a comment of the form:
+
+     ::
+
+        (** * ModuleName : text *)
+
+     where ``ModuleName`` must be the name of the file. If it is present, the
+     text is used as a subtitle for the module in appropriate places.
+  :-t string, --title string: Set the document title.
+
+
+**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
+
+
+
+    The behavior of options ``-g`` and ``-l`` can be locally overridden using the
+    ``(* begin show *) … (* end show *)`` environment (see above).
+
+    There are a few options that control the parsing of comments:
+
+  :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as
+    well. They are typeset inline.
+  :--plain-comments: Do not interpret comments, simply copy them as
+    plain-text.
+  :--interpolate: Use the globalization information to typeset
+    identifiers appearing in |Coq| escapings inside comments.
+
+**Language options**
+
+
+  The default behavior is to assume ASCII 7 bit input files.
+
+  :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to
+    --inputenc latin1 --charset iso-8859-1.
+  :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset
+    utf-8 for HTML output. Also use Unicode replacements for a couple of
+    standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex|
+    UTF-8 support can be found
+    at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode
+    characters by |Latex|, extra packages which coqdoc does not provide
+    by default might be required, such as textgreek for some Greek letters
+    or ``stmaryrd`` for some mathematical symbols. If a Unicode character is
+    missing an interpretation in the utf8x input encoding, add
+    ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages
+    and declarations can be added with option ``-p``.
+  :--inputenc string: Give a |Latex| input encoding, as an option to |Latex|
+    package ``inputenc``.
+  :--charset string: Specify the HTML character set, to be inserted in
+    the HTML header.
+
+
+
+The coqdoc |Latex| style file
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In case you choose to produce a document without the default |Latex|
+preamble (by using option ``--no-preamble``), then you must insert into
+your own preamble the command
+
+::
+
+  \usepackage{coqdoc}
+
+The package optionally takes the argument ``[color]`` to typeset
+identifiers with colors (this requires the ``xcolor`` package).
+
+Then you may alter the rendering of the document by redefining some
+macros:
+
+: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``.
diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst
index 4381c4d63d..dfe38dfce9 100644
--- a/doc/sphinx/using/tools/index.rst
+++ b/doc/sphinx/using/tools/index.rst
@@ -16,5 +16,6 @@ on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_.
 
    ../../practical-tools/coq-commands
    ../../practical-tools/utilities
+   coqdoc
    ../../practical-tools/coqide
    ../../addendum/parallel-proof-processing