diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 294 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 302 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 968 |
3 files changed, 1564 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst new file mode 100644 index 0000000000..9bc67147f7 --- /dev/null +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -0,0 +1,294 @@ +.. _thecoqcommands: + +The |Coq| commands +==================== + +There are three |Coq| commands: + ++ ``coqtop``: the |Coq| toplevel (interactive mode); ++ ``coqc``: the |Coq| compiler (batch compilation); ++ ``coqchk``: the |Coq| checker (validation of compiled libraries). + + +The options are (basically) the same for the first two commands, and +roughly described below. You can also look at the ``man`` pages of +``coqtop`` and ``coqc`` for more details. + +.. _interactive-use: + +Interactive use (coqtop) +------------------------ + +In the interactive mode, also known as the |Coq| toplevel, the user can +develop his theories and proofs step by step. The |Coq| toplevel is run +by the command ``coqtop``. + +There are two different binary images of |Coq|: the byte-code one and the +native-code one (if OCaml provides a native-code compiler for +your platform, which is supposed in the following). By default, +``coqtop`` executes the native-code version; run ``coqtop.byte`` to get +the byte-code version. + +The byte-code toplevel is based on an OCaml toplevel (to +allow dynamic linking of tactics). You can switch to the OCaml toplevel +with the command ``Drop.``, and come back to the |Coq| +toplevel with the command ``Coqloop.loop();;``. + +Batch compilation (coqc) +------------------------ + +The ``coqc`` command takes a name *file* as argument. Then it looks for a +vernacular file named *file*.v, and tries to compile it into a +*file*.vo file (See :ref:`compiled-files`). + +.. caution:: + + The name *file* should be a regular |Coq| identifier as defined in Section :ref:`lexical-conventions`. + It should contain only letters, digits or underscores (_). For example ``/bar/foo/toto.v`` is valid, + but ``/bar/foo/to-to.v`` is not. + + +Customization at launch time +--------------------------------- + +By resource file +~~~~~~~~~~~~~~~~~~~~~~~ + +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` +is the configuration directory of the user (by default it's ``~/.config``) +and ``xxx`` is the version number (e.g. 8.8). If +this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file +(see option ``-init-file`` below). + +The resource file may contain, for instance, ``Add LoadPath`` commands to add +directories to the load path of |Coq|. It is possible to skip the +loading of the resource file with the option ``-q``. + +.. _customization-by-environment-variables: + +By environment variables +~~~~~~~~~~~~~~~~~~~~~~~~~ + +Load path can be specified to the |Coq| system by setting up ``$COQPATH`` +environment variable. It is a list of directories separated by +``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and +``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`). + +Some |Coq| commands call other |Coq| commands. In this case, they look for +the commands in directory specified by ``$COQBIN``. If this variable is +not set, they look for the commands in the executable path. + +.. _COQ_COLORS: + +The ``$COQ_COLORS`` environment variable can be used to specify the set +of colors used by ``coqtop`` to highlight its output. It uses the same +syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated +list of assignments of the form :n:`name={*; attr}` where +``name`` is the name of the corresponding highlight tag and each ``attr`` is an +ANSI escape code. The list of highlight tags can be retrieved with the +``-list-tags`` command-line option of ``coqtop``. + +The string uses ANSI escape codes to represent attributes. For example: + + ``export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”`` + +sets the highlights for added text in diffs to underlined (the 4) with a background RGB +color (0, 0, 240) and for removed text in diffs to a red background. +Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. + + +.. _command-line-options: + +By command line options +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following command-line options are recognized by the commands ``coqc`` +and ``coqtop``, unless stated otherwise: + +:-I *directory*, -include *directory*: Add physical path *directory* + to the OCaml loadpath. + + .. seealso:: + + :ref:`names-of-libraries` and the + command Declare ML Module Section :ref:`compiled-files`. +:-Q *directory* dirpath: Add physical path *directory* to the list of + directories where |Coq| looks for a file and bind it to the logical + directory *dirpath*. The subdirectory structure of *directory* is + recursively available from |Coq| using absolute names (extending the + dirpath prefix) (see Section :ref:`qualified-names`).Note that only those + subdirectories and files which obey the lexical conventions of what is + an :n:`@ident` are taken into account. Conversely, the + underlying file systems or operating systems may be more restrictive + than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive + layout (within the limit of 255 bytes per filename), the default on + NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to + disallow two files differing only in the case in the same directory. + + .. seealso:: Section :ref:`names-of-libraries`. +:-R *directory* dirpath: Do as -Q *directory* dirpath but make the + subdirectory structure of *directory* recursively visible so that the + recursive contents of physical *directory* is available from |Coq| using + short or partially qualified names. + + .. seealso:: Section :ref:`names-of-libraries`. +:-top dirpath: Set the toplevel module name to dirpath instead of Top. + Not valid for `coqc` as the toplevel module name is inferred from the + name of the output file. +:-exclude-dir *directory*: Exclude any subdirectory named *directory* + while processing options such as -R and -Q. By default, only the + conventional version control management directories named CVS + and_darcs are excluded. +:-nois: Start from an empty state instead of loading the Init.Prelude + module. +:-init-file *file*: Load *file* as the resource file instead of + loading the default resource file from the standard configuration + directories. +:-q: Do not to load the default resource file. +:-load-ml-source *file*: Load the OCaml source file *file*. +:-load-ml-object *file*: Load the OCaml object file *file*. +:-l *file*, -load-vernac-source *file*: Load and execute the |Coq| + script from *file.v*. +:-lv *file*, -load-vernac-source-verbose *file*: Load and execute the + |Coq| script from *file.v*. Write its contents to the standard output as + it is executed. +:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This + is equivalent to runningRequire dirpath. +:-require dirpath: Load |Coq| compiled library dirpath and import it. + This is equivalent to running Require Import dirpath. +:-batch: Exit just after argument parsing. Available for `coqtop` only. +:-compile *file.v*: Compile file *file.v* into *file.vo*. This option + implies -batch (exit just after argument parsing). It is available only + for `coqtop`, as this behavior is the purpose of `coqc`. +:-compile-verbose *file.v*: Same as -compile but also output the + content of *file.v* as it is compiled. +:-verbose: Output the content of the input file as it is compiled. + This option is available for `coqc` only; it is the counterpart of + -compile-verbose. +:-w (all|none|w₁,…,wₙ): Configure the display of warnings. This + option expects all, none or a comma-separated list of warning names or + categories (see Section :ref:`controlling-display`). +:-color (on|off|auto): *Coqtop only*. Enable or disable color output. + Default is auto, meaning color is shown only if + the output channel supports ANSI escape sequences. +:-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences + between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and + removed tokens. Requires that ``–color`` is enabled. (see Section + :ref:`showing_diffs`). +:-beautify: Pretty-print each command to *file.beautified* when + compiling *file.v*, in order to get old-fashioned + syntax/definitions/notations. +:-emacs, -ide-slave: Start a special toplevel to communicate with a + specific IDE. +:-impredicative-set: Change the logical theory of |Coq| by declaring the + sort Set impredicative. + + .. warning:: + + This is known to be inconsistent with some + standard axioms of classical mathematics such as the functional + axiom of choice or the principle of description. +:-type-in-type: Collapse the universe hierarchy of |Coq|. + + .. warning:: This makes the logic inconsistent. +:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace + Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, + etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on, + and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature + is intended to be used as a linter for developments that want to be robust to + changes in the auto-generated name scheme. The options are provided to + facilitate tracking down problems. +:-compat *version*: Attempt to maintain some backward-compatibility + with a previous version. +:-dump-glob *file*: Dump references for global names in file *file* + (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being + compiled, *file.glob* is used. +:-no-glob: Disable the dumping of references for global names. +:-image *file*: Set the binary image to be used by `coqc` to be *file* + instead of the standard one. Not of general use. +:-bindir *directory*: Set the directory containing |Coq| binaries to be + used by `coqc`. It is equivalent to doing export COQBIN= *directory* + before launching `coqc`. +:-where: Print the location of |Coq|’s standard library and exit. +:-config: Print the locations of |Coq|’s binaries, dependencies, and + libraries, then exit. +:-filteropts: Print the list of command line arguments that `coqtop` has + recognized as options and exit. +:-v: Print |Coq|’s version and exit. +:-list-tags: Print the highlight tags known by |Coq| as well as their + currently associated color and exit. +:-h, --help: Print a short usage and exit. + +Compiled libraries checker (coqchk) +---------------------------------------- + +The ``coqchk`` command takes a list of library paths as argument, described either +by their logical name or by their physical filename, hich must end in ``.vo``. The +corresponding compiled libraries (``.vo`` files) are searched in the path, +recursively processing the libraries they depend on. The content of all these +libraries is then type checked. The effect of ``coqchk`` is only to return with +normal exit code in case of success, and with positive exit code if an error has +been found. Error messages are not deemed to help the user understand what is +wrong. In the current version, it does not modify the compiled libraries to mark +them as successfully checked. + +Note that non-logical information is not checked. By logical +information, we mean the type and optional body associated to names. +It excludes for instance anything related to the concrete syntax of +objects (customized syntax rules, association between short and long +names), implicit arguments, etc. + +This tool can be used for several purposes. One is to check that a +compiled library provided by a third-party has not been forged and +that loading it cannot introduce inconsistencies [#]_. Another point is +to get an even higher level of security. Since ``coqtop`` can be extended +with custom tactics, possibly ill-typed code, it cannot be guaranteed +that the produced compiled libraries are correct. ``coqchk`` is a +standalone verifier, and thus it cannot be tainted by such malicious +code. + +Command-line options ``-Q``, ``-R``, ``-where`` and ``-impredicative-set`` are supported +by ``coqchk`` and have the same meaning as for ``coqtop``. As there is no notion of +relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. + +:-norec *module*: Check *module* but do not check its dependencies. +:-admit *module*: Do not check *module* and any of its dependencies, + unless explicitly required. +:-o: At exit, print a summary about the context. List the names of all + assumptions and variables (constants without body). +:-silent: Do not write progress information to the standard output. + +Environment variable ``$COQLIB`` can be set to override the location of +the standard library. + +The algorithm for deciding which modules are checked or admitted is +the following: assuming that ``coqchk`` is called with argument ``M``, option +``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the +set of reflexive transitive dependencies of set :math:`S`. Then: + ++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type checked before being added + to the context. ++ And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the + context without type checking. Basic integrity checks (checksums) are + nonetheless performed. + +As a rule of thumb, -admit can be used to tell Coq that some libraries +have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && +``coqchk B -admit A`` without type checking any definition twice. Of +course, the latter is slightly slower since it makes more disk access. +It is also less secure since an attacker might have replaced the +compiled library ``A`` after it has been read by the first command, but +before it has been read by the second command. + +.. [#] Ill-formed non-logical information might for instance bind + Coq.Init.Logic.True to short name False, so apparently False is + inhabited, but using fully qualified names, Coq.Init.Logic.False will + always refer to the absurd proposition, what we guarantee is that + there is no proof of this latter constant. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst new file mode 100644 index 0000000000..9455228e7d --- /dev/null +++ b/doc/sphinx/practical-tools/coqide.rst @@ -0,0 +1,302 @@ +.. _coqintegrateddevelopmentenvironment: + +|Coq| Integrated Development Environment +======================================== + +The Coq Integrated Development Environment is a graphical tool, to be +used as a user-friendly replacement to `coqtop`. Its main purpose is to +allow the user to navigate forward and backward into a Coq vernacular +file, executing corresponding commands or undoing them respectively. + +|CoqIDE| is run by typing the command `coqide` on the command line. +Without argument, the main screen is displayed with an “unnamed +buffer”, and with a filename as argument, another buffer displaying +the contents of that file. Additionally, `coqide` accepts the same +options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously +no meaning for |CoqIDE| being ignored. + +.. _coqide_mainscreen: + + .. image:: ../_static/coqide.png + :alt: |CoqIDE| main screen + +A sample |CoqIDE| main screen, while navigating into a file `Fermat.v`, +is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`. +At the top is a menu bar, and a tool bar +below it. The large window on the left is displaying the various +*script buffers*. The upper right window is the *goal window*, where +goals to be proven are displayed. The lower right window is the *message +window*, where various messages resulting from commands are displayed. +At the bottom is the status bar. + +Managing files and buffers, basic editing +---------------------------------------------- + +In the script window, you may open arbitrarily many buffers to edit. +The *File* menu allows you to open files or create some, save them, +print or export them into various formats. Among all these buffers, +there is always one which is the current *running buffer*, whose name +is displayed on a background in the *processed* color (green by default), which +is the one where Coq commands are currently executed. + +Buffers may be edited as in any text editor, and classical basic +editing commands (Copy/Paste, …) are available in the *Edit* menu. +|CoqIDE| offers only basic editing commands, so if you need more complex +editing commands, you may launch your favorite text editor on the +current buffer, using the *Edit/External Editor* menu. + +Interactive navigation into Coq scripts +-------------------------------------------- + +The running buffer is the one where navigation takes place. The toolbar offers +five basic commands for this. The first one, represented by a down arrow icon, +is for going forward executing one command. If that command is successful, the +part of the script that has been executed is displayed on a background with the +processed color. If that command fails, the error message is displayed in the +message window, and the location of the error is emphasized by an underline in +the error foreground color (red by default). + +In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`, +the running buffer is `Fermat.v`, all commands until +the ``Theorem`` have been already executed, and the user tried to go +forward executing ``Induction n``. That command failed because no such +tactic exists (names of standard tactics are written in lowercase), +and the failing command is underlined. + +Notice that the processed part of the running buffer is not editable. If +you ever want to modify something you have to go backward using the up +arrow tool, or even better, put the cursor where you want to go back +and use the goto button. Unlike with `coqtop`, you should never use +``Undo`` to go backward. + +There are two additional buttons for navigation within the running buffer. The +"down" button with a line goes directly to the end; the "up" button with a line +goes back to the beginning. The handling of errors when using the go-to-the-end +button depends on whether |Coq| is running in asynchronous mode or not (see +Chapter :ref:`asynchronousandparallelproofprocessing`). If it is not running in that mode, execution +stops as soon as an error is found. Otherwise, execution continues, and the +error is marked with an underline in the error foreground color, with a +background in the error background color (pink by default). The same +characterization of error-handling applies when running several commands using +the "goto" button. + +If you ever try to execute a command that runs for a long time +and would like to abort it before it terminates, you may +use the interrupt button (the white cross on a red circle). + +There are other buttons on the |CoqIDE| toolbar: a button to save the running +buffer; a button to close the current buffer (an "X"); buttons to switch among +buffers (left and right arrows); an "information" button; and a "gears" button. + +The "information" button is described in Section :ref:`try-tactics-automatically`. + +The "gears" button submits proof terms to the |Coq| kernel for type checking. +When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), +proofs may have been completed without kernel-checking of generated proof terms. +The presence of unchecked proof terms is indicated by ``Qed`` statements that +have a subdued *being-processed* color (light blue by default), rather than the +processed color, though their preceding proofs have the processed color. + +Notice that for all these buttons, except for the "gears" button, their operations +are also available in the menu, where their keyboard shortcuts are given. + +.. _try-tactics-automatically: + +Trying tactics automatically +------------------------------ + +The menu Try Tactics provides some features for automatically trying +to solve the current goal using simple tactics. If such a tactic +succeeds in solving the goal, then its text is automatically inserted +into the script. There is finally a combination of these tactics, +called the *proof wizard* which will try each of them in turn. This +wizard is also available as a tool button (the "information" button). The set of +tactics tried by the wizard is customizable in the preferences. + +These tactics are general ones, in particular they do not refer to +particular hypotheses. You may also try specific tactics related to +the goal or one of the hypotheses, by clicking with the right mouse +button on the goal or the considered hypothesis. This is the +“contextual menu on goals” feature, that may be disabled in the +preferences if undesirable. + + +Proof folding +------------------ + +As your script grows bigger and bigger, it might be useful to hide the +proofs of your theorems and lemmas. + +This feature is toggled via the Hide entry of the Navigation menu. The +proof shall be enclosed between ``Proof.`` and ``Qed.``, both with their final +dots. The proof that shall be hidden or revealed is the first one +whose beginning statement (such as ``Theorem``) precedes the insertion +cursor. + + +Vernacular commands, templates +----------------------------------- + +The Templates menu allows using shortcuts to insert vernacular +commands. This is a nice way to proceed if you are not sure of the +syntax of the command you want. + +Moreover, from this menu you can automatically insert templates of complex +commands like ``Fixpoint`` that you can conveniently fill afterwards. + +Queries +------------ + +.. image:: ../_static/coqide-queries.png + :alt: |CoqIDE| queries + +We call *query* any vernacular command that does not change the current state, +such as ``Check``, ``Search``, etc. To run such commands interactively, without +writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be +displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. +Queries can also be performed by selecting a particular phrase, then choosing an +item from the ``Queries`` menu. The response then appears in the message window. +The image above shows the result after selecting of the phrase +``Nat.mul`` in the script window, and choosing ``Print`` from the ``Queries`` +menu. + + +Compilation +---------------- + +The `Compile` menu offers direct commands to: + ++ compile the current buffer ++ run a compilation using `make` ++ go to the last compilation error ++ create a `Makefile` using `coq_makefile`. + +Customizations +------------------- + +You may customize your environment using the menu Edit/Preferences. A new +window will be displayed, with several customization sections +presented as a notebook. + +The first section is for selecting the text font used for scripts, +goal and message windows. + +The second section is devoted to file management: you may configure +automatic saving of files, by periodically saving the contents into +files named `#f#` for each opened file `f`. You may also activate the +*revert* feature: in case a opened file is modified on the disk by a +third party, |CoqIDE| may read it again for you. Note that in the case +you edited that same file, you will be prompted to choose to either +discard your changes or not. The File charset encoding choice is +described below in :ref:`character-encoding-saved-files`. + +The `Externals` section allows customizing the external commands for +compilation, printing, web browsing. In the browser command, you may +use `%s` to denote the URL to open, for example: +`firefox -remote "OpenURL(%s)"`. + +The `Tactics Wizard` section allows defining the set of tactics that +should be tried, in sequence, to solve the current goal. + +The last section is for miscellaneous boolean settings, such as the +“contextual menu on goals” feature presented in the section +:ref:`Try tactics automatically <try-tactics-automatically>`. + +Notice that these settings are saved in the file `.coqiderc` of your +home directory. + +A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It +is not recommended to edit this file manually: to modify a given menu +shortcut, go to the corresponding menu item without releasing the +mouse button, press the key you want for the new shortcut, and release +the mouse button afterwards. If your system does not allow it, you may +still edit this configuration file by hand, but this is more involved. + + +Using Unicode symbols +-------------------------- + +|CoqIDE| is based on GTK+ and inherits from it support for Unicode in +its text windows. Consequently a large set of symbols is available for +notations. + + +Displaying Unicode symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +You just need to define suitable notations as described in the chapter +:ref:`syntaxextensionsandinterpretationscopes`. For example, to use the +mathematical symbols ∀ and ∃, you may define: + +.. coqtop:: in + + Notation "∀ x : T, P" := + (forall x : T, P) (at level 200, x ident). + Notation "∃ x : T, P" := + (exists x : T, P) (at level 200, x ident). + +There exists a small set of such notations already defined, in the +file `utf8.v` of Coq library, so you may enable them just by +``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently, +by starting |CoqIDE| with ``coqide -l utf8``. + +However, there are some issues when using such Unicode symbols: you of +course need to use a character font which supports them. In the Fonts +section of the preferences, the Preview line displays some Unicode +symbols, so you could figure out if the selected font is OK. Related +to this, one thing you may need to do is choosing whether GTK+ should +use antialiased fonts or not, by setting the environment variable +`GDK_USE_XFT` to 1 or 0 respectively. + + +Defining an input method for non-ASCII symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To input a Unicode symbol, a general method provided by GTK+ is to +simultaneously press the Control, Shift and “u” keys, release, then +type the hexadecimal code of the symbol required, for example `2200` +for the ∀ symbol. A list of symbol codes is available at +`http://www.unicode.org`. + +An alternative method which does not require to know the hexadecimal +code of the character is to use an Input Method Editor. On POSIX +systems (Linux distributions, BSD variants and MacOS X), you can +use `uim` version 1.6 or later which provides a LaTeX-style input +method. + +To configure uim, execute uim-pref-gtk as your regular user. In the +"Global Settings" group set the default Input Method to "ELatin" +(don’t forget to tick the checkbox "Specify default IM"). In the +"ELatin" group set the layout to "TeX", and remember the content of +the "[ELatin] on" field (by default Control-\\). You can now execute +|CoqIDE| with the following commands (assuming you use a Bourne-style +shell): + +:: + + $ export GTK_IM_MODULE=uim + $ coqide + + +Activate the ELatin Input Method with Control-\\, then type the +sequence `\\Gamma`. You will see the sequence being replaced by Γ as +soon as you type the second "a". + +.. _character-encoding-saved-files: + +Character encoding for saved files +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In the Files section of the preferences, the encoding option is +related to the way files are saved. + +If you have no need to exchange files with non UTF-8 aware +applications, it is better to choose the UTF-8 encoding, since it +guarantees that your files will be read again without problems. (This +is because when |CoqIDE| reads a file, it tries to automatically detect +its character encoding.) + +If you choose something else than UTF-8, then missing characters will +be written encoded by `\x{....}` or `\x{........}` where each dot is +an hexadecimal digit: the number between braces is the hexadecimal +Unicode index for the missing character. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst new file mode 100644 index 0000000000..7c78e1a50f --- /dev/null +++ b/doc/sphinx/practical-tools/utilities.rst @@ -0,0 +1,968 @@ +.. _utilities: + +--------------------- + Utilities +--------------------- + +The distribution provides utilities to simplify some tedious works +beside proof development, tactics writing or documentation. + + +Using Coq as a library +---------------------- + +In previous versions, ``coqmktop`` was used to build custom +toplevels - for example for better debugging or custom static +linking. Nowadays, the preferred method is to use ``ocamlfind``. + +The most basic custom toplevel is built using: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel \ + topbin/coqtop_bin.ml -o my_toplevel.native + + +For example, to statically link |Ltac|, you can just do: + +:: + + % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native + +and similarly for other plugins. + + +Building a |Coq| project with coq_makefile +------------------------------------------ + +The majority of |Coq| projects are very similar: a collection of ``.v`` +files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of +metadata needed in order to build the project are the command line +options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command +line options <command-line-options>`). Collecting the list of files +and options is the job of the ``_CoqProject`` file. + +A simple example of a ``_CoqProject`` file follows: + +:: + + -R theories/ MyCode + -arg -w + -arg all + theories/foo.v + theories/bar.v + -I src/ + src/baz.ml4 + src/bazaux.ml + src/qux_plugin.mlpack + +where options ``-R``, ``-Q`` and ``-I`` are natively recognized, as well as +file names. The lines of the form ``-arg foo`` are used in order to tell +to literally pass an argument ``foo`` to ``coqc``: in the +example, this allows to pass the two-word option ``-w all`` (see +:ref:`command line options <command-line-options>`). + +Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``) +understand ``_CoqProject`` files and invoke |Coq| with the desired options. + +The ``coq_makefile`` utility can be used to set up a build infrastructure +for the |Coq| project based on makefiles. The recommended way of +invoking ``coq_makefile`` is the following one: + +:: + + coq_makefile -f _CoqProject -o CoqMakefile + + +Such command generates the following files: + +CoqMakefile + is a generic makefile for ``GNU Make`` that provides + targets to build the project (both ``.v`` and ``.ml*`` files), to install it + system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed) + as well as to invoke coqdoc to generate HTML documentation. + +CoqMakefile.conf + contains make variables assignments that reflect + the contents of the ``_CoqProject`` file as well as the path relevant to + |Coq|. + + +An optional file ``CoqMakefile.local`` can be provided by the user in order to +extend ``CoqMakefile``. In particular one can declare custom actions to be +performed before or after the build process. Similarly one can customize the +install target or even provide new targets. Extension points are documented in +paragraph :ref:`coqmakefilelocal`. + +The extensions of the files listed in ``_CoqProject`` is used in order to +decide how to build them. In particular: + + ++ |Coq| files must use the ``.v`` extension ++ |OCaml| files must use the ``.ml`` or ``.mli`` extension ++ |OCaml| files that require pre processing for syntax + extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension ++ In order to generate a plugin one has to list all |OCaml| + modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib`` + file). + + +The use of ``.mlpack`` files has to be preferred over ``.mllib`` files, +since it results in a “packed” plugin: All auxiliary modules (as +``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace" +(``Qux_plugin``). This reduces the chances of begin unable to load two +distinct plugins because of a clash in their auxiliary module names. + +.. _coqmakefilelocal: + +CoqMakefile.local +~~~~~~~~~~~~~~~~~ + +The optional file ``CoqMakefile.local`` is included by the generated +file ``CoqMakefile``. It can contain two kinds of directives. + +**Variable assignment** + +The variable must belong to the variables listed in the ``Parameters`` +section of the generated makefile. +Here we describe only few of them. + +:CAMLPKGS: + can be used to specify third party findlib packages, and is + passed to the OCaml compiler on building or linking of modules. Eg: + ``-package yojson``. +:CAMLFLAGS: + can be used to specify additional flags to the |OCaml| + compiler, like ``-bin-annot`` or ``-w``.... +:COQC, COQDEP, COQDOC: + can be set in order to use alternative binaries + (e.g. wrappers) +:COQ_SRC_SUBDIRS: + can be extended by including other paths in which ``*.cm*`` files + are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` + lets you build a plugin containing OCaml code that depends on the + OCaml code of ``Unicoq`` +:COQFLAGS: + override the flags passed to ``coqc``. By default ``-q``. +:COQEXTRAFLAGS: + extend the flags passed to ``coqc`` +:COQCHKFLAGS: + override the flags passed to ``coqchk``. By default ``-silent -o``. +:COQCHKEXTRAFLAGS: + extend the flags passed to ``coqchk`` +:COQDOCFLAGS: + override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``. +:COQDOCEXTRAFLAGS: + extend the flags passed to ``coqdoc`` + +**Rule extension** + +The following makefile rules can be extended. + +.. example:: + + :: + + pre-all:: + echo "This line is print before making the all target" + install-extra:: + cp ThisExtraFile /there/it/goes + +``pre-all::`` + run before the ``all`` target. One can use this to configure + the project, or initialize sub modules or check dependencies are met. + +``post-all::`` + run after the ``all`` target. One can use this to run a test + suite, or compile extracted code. + +``install-extra::`` + run after ``install``. One can use this to install extra files. + +``install-doc::`` + One can use this to install extra doc. + +``uninstall::`` + \ + +``uninstall-doc::`` + \ + +``clean::`` + \ + +``cleanall::`` + \ + +``archclean::`` + \ + +``merlin-hook::`` + One can append lines to the generated ``.merlin`` file extending this + target. + +Timing targets and performance testing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The generated ``Makefile`` supports the generation of two kinds of timing +data: per-file build-times, and per-line times for an individual file. + +The following targets and Makefile variables allow collection of per- +file timing data: + + ++ ``TIMED=1`` + passing this variable will cause ``make`` to emit a line + describing the user-space build-time and peak memory usage for each + file built. + + .. note:: + On ``Mac OS``, this works best if you’ve installed ``gnu-time``. + + .. example:: + + For example, the output of ``make TIMED=1`` may look like + this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.34 mem: 395448 ko) + COQC Fast.v + Fast (user: 0.01 mem: 45184 ko) + ++ ``pretty-timed`` + this target stores the output of ``make TIMED=1`` into + ``time-of-build.log``, and displays a table of the times, sorted from + slowest to fastest, which is also stored in ``time-of-build-pretty.log``. + If you want to construct the ``log`` for targets other than the default + one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed + TGTS="a.vo b.vo"``. + + .. :: + This target requires ``python`` to build the table. + + .. note:: + This target will *append* to the timing log; if you want a + fresh start, you must remove the ``filetime-of-build.log`` or + ``run make cleanall``. + + .. example:: + + For example, the output of ``make pretty-timed`` may look like this: + + :: + + COQDEP Fast.v + COQDEP Slow.v + COQC Slow.v + Slow (user: 0.36 mem: 393912 ko) + COQC Fast.v + Fast (user: 0.05 mem: 45992 ko) + Time | File Name + -------------------- + 0m00.41s | Total + -------------------- + 0m00.36s | Slow + 0m00.05s | Fast + + ++ ``print-pretty-timed-diff`` + this target builds a table of timing changes between two compilations; run + ``make make-pretty-timed-before`` to build the log of the “before” times, + and run ``make make-pretty-timed-after`` to build the log of the “after” + times. The table is printed on the command line, and stored in + ``time-of-build-both.log``. This target is most useful for profiling the + difference between two commits in a repository. + + .. note:: + This target requires ``python`` to build the table. + + .. note:: + The ``make-pretty-timed-before`` and ``make-pretty-timed-after`` targets will + *append* to the timing log; if you want a fresh start, you must remove + the files ``time-of-build-before.log`` and ``time-of-build-after.log`` or run + ``make cleanall`` *before* building either the “before” or “after” + targets. + + .. note:: + The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then by + times in the “after” column, and finally lexicographically by file + name. This will put the biggest changes in either direction first, and + will prefer sorting by build-time over subsecond changes in build time + (which are frequently noise); lexicographic sorting forces an order on + files which take effectively no time to compile. + + .. example:: + + For example, the output table from + ``make print-pretty-timed-diff`` may look like this: + + :: + + After | File Name | Before || Change | % Change + -------------------------------------------------------- + 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% + -------------------------------------------------------- + 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + + +The following targets and ``Makefile`` variables allow collection of per- +line timing data: + + ++ ``TIMING=1`` + passing this variable will cause ``make`` to use ``coqc -time`` to + write to a ``.v.timing`` file for each ``.v`` file compiled, which contains + line-by-line timing information. + + .. example:: + + For example, running ``make all TIMING=1`` may result in a file like this: + + :: + + Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) + Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) + Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) + Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) + ++ ``print-pretty-single-time-diff`` + + :: + + print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + + this target will make a sorted table of the per-line timing differences + between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and + save it to the file specified by the ``TIME_OF_PRETTY_BUILD_FILE`` variable, + which defaults to ``time-of-build-pretty.log``. + To generate the ``.v.before-timing`` or ``.v.after-timing`` files, you should + pass ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``. + + .. note:: + The sorting used here is the same as in the ``print-pretty-timed -diff`` target. + + .. note:: + This target requires python to build the table. + + .. example:: + + For example, running ``print-pretty-single-time-diff`` might give a table like this: + + :: + + After | Code | Before || Change | % Change + --------------------------------------------------------------------------------------------------- + 0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% + --------------------------------------------------------------------------------------------------- + 0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% + 0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A + 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A + 0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% + + ++ ``all.timing.diff``, ``path/to/file.v.timing.diff`` + The ``path/to/file.v.timing.diff`` target will make a ``.v.timing.diff`` file for + the corresponding ``.v`` file, with a table as would be generated by + the ``print-pretty-single-time-diff`` target; it depends on having already + made the corresponding ``.v.before-timing`` and ``.v.after-timing`` files, + which can be made by passing ``TIMING=before`` and ``TIMING=after``. + The ``all.timing.diff`` target will make such timing difference files for + all of the ``.v`` files that the ``Makefile`` knows about. It will fail if + some ``.v.before-timing`` or ``.v.after-timing`` files don’t exist. + + .. note:: + This target requires python to build the table. + + +Reusing/extending the generated Makefile +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Including the generated makefile with an include directive is +discouraged. The contents of this file, including variable names and +status of rules shall change in the future. Users are advised to +include ``Makefile.conf`` or call a target of the generated Makefile as in +``make -f Makefile target`` from another Makefile. + +One way to get access to all targets of the generated ``CoqMakefile`` is to +have a generic target for invoking unknown targets. + +.. example:: + + :: + + # KNOWNTARGETS will not be passed along to CoqMakefile + KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 + # KNOWNFILES will not get implicit targets from the final rule, and so + # depending on them won't invoke the submake + # Warning: These files get declared as PHONY, so any targets depending + # on them always get rebuilt + KNOWNFILES := Makefile _CoqProject + + .DEFAULT_GOAL := invoke-coqmakefile + + CoqMakefile: Makefile _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile + + invoke-coqmakefile: CoqMakefile + $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) + + .PHONY: invoke-coqmakefile $(KNOWNFILES) + + #################################################################### + ## Your targets here ## + #################################################################### + + # This should be the last rule, to handle any targets not declared above + %: invoke-coqmakefile + @true + + + +Building a subset of the targets with ``-j`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To build, say, two targets foo.vo and bar.vo in parallel one can use +``make only TGTS="foo.vo bar.vo" -j``. + +.. note:: + + ``make foo.vo bar.vo -j`` has a different meaning for the make + utility, in particular it may build a shared prerequisite twice. + + +.. note:: + + For users of coq_makefile with version < 8.7 + + + Support for "subdirectory" is deprecated. To perform actions before + or after the build (like invoking ``make`` on a subdirectory) one can hook + in pre-all and post-all extension points. + + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target + (``.PHONY`` or not) please use ``CoqMakefile.local``. + + + +Module dependencies +-------------------- + +In order to compute module dependencies (so to use ``make``), |Coq| comes +with an appropriate tool, ``coqdep``. + +``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +programs, and prints the dependencies on the standard output in a +format readable by make. When a directory is given as argument, it is +recursively looked at. + +Dependencies of |Coq| modules are computed by looking at ``Require`` +commands (``Require``, ``Require Export``, ``Require Import``), but also at the +command ``Declare ML Module``. + +Dependencies of |OCaml| modules are computed by looking at +`open` commands and the dot notation *module.value*. However, this is +done approximately and you are advised to use ``ocamldep`` instead for the +|OCaml| module dependencies. + +See the man page of ``coqdep`` for more details and options. + +The build infrastructure generated by ``coq_makefile`` uses ``coqdep`` to +automatically compute the dependencies among the files part of the +project. + + +.. _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: 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. + + +**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``. + +Embedded Coq phrases inside |Latex| documents +--------------------------------------------- + +When writing 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. + + +Man pages +--------- + +There are man pages for the commands ``coqdep`` and ``coq-tex``. Man +pages are installed at installation time (see installation +instructions in file ``INSTALL``, step 6). |