diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 21 |
2 files changed, 32 insertions, 10 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 343ca9ed7d..de9e327740 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -85,6 +85,8 @@ 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 @@ -93,6 +95,15 @@ list of assignments of the form :n:`name={*; attr}` where 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 @@ -164,9 +175,13 @@ and ``coqtop``, unless stated otherwise: :-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): Enable or not the coloring of output of `coqtop`. - Default is auto, meaning that `coqtop` dynamically decides, depending on - whether the output channel supports ANSI escape sequences. +:-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. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d300c3d6d..7c78e1a50f 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -21,16 +21,16 @@ The most basic custom toplevel is built using: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ -package coq.toplevel \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + topbin/coqtop_bin.ml -o my_toplevel.native -For example, to statically link |L_tac|, you can just do: +For example, to statically link |Ltac|, you can just do: :: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ - -package coq.toplevel -package coq.ltac \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native and similarly for other plugins. @@ -41,15 +41,17 @@ 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``, ``-I``, see also: section -:ref:`command-line-options`). Collecting the list of files and options is the job -of the ``_CoqProject`` file. +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/ @@ -57,6 +59,11 @@ A simple example of a ``_CoqProject`` file follows: 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. |