From 4da3fe8aafe2d5ceadb505ba16cfbb4482755c61 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 27 Mar 2020 14:11:20 +0100 Subject: Move section on coqdoc to new location. --- doc/sphinx/practical-tools/utilities.rst | 463 ------------------------------- doc/sphinx/using/tools/coqdoc.rst | 463 +++++++++++++++++++++++++++++++ doc/sphinx/using/tools/index.rst | 2 +- 3 files changed, 464 insertions(+), 464 deletions(-) delete mode 100644 doc/sphinx/practical-tools/utilities.rst create mode 100644 doc/sphinx/using/tools/coqdoc.rst diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst deleted file mode 100644 index cada680895..0000000000 --- a/doc/sphinx/practical-tools/utilities.rst +++ /dev/null @@ -1,463 +0,0 @@ -.. _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 -``_. 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 ``. -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 - ``_). 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 ``_. 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/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 +``_. 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 ``. +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 + ``_). 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 ``_. 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..9472cc165b 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -15,6 +15,6 @@ on the `Coq website `_. :maxdepth: 1 ../../practical-tools/coq-commands - ../../practical-tools/utilities + coqdoc ../../practical-tools/coqide ../../addendum/parallel-proof-processing -- cgit v1.2.3