diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 62 |
3 files changed, 57 insertions, 40 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..545bba4930 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise: it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This is equivalent to running :cmd:`Require` :n:`qualid`. +:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. @@ -172,7 +174,6 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. -:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only @@ -379,7 +380,7 @@ 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 +by their logical name or by their physical filename, which 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 diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index b1f392c337..42e752841d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,3 +1,5 @@ +.. |GtkSourceView| replace:: :smallcaps:`GtkSourceView` + .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment @@ -98,19 +100,6 @@ 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. -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 ----------------------------------- @@ -158,7 +147,18 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second and third sections are for controlling colors and style. +The second and third sections are for controlling colors and style of +the three main buffers. A predefined |Coq| highlighting style as well +as standard |GtkSourceView| styles are available. Other styles can be +added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see +the general documentation about |GtkSourceView| for the various +possibilities). Note that the style of the rest of graphical part of +Coqide is not under the control of |GtkSourceView| but of GTK+ and +governed by files such as ``settings.ini`` and ``gtk.css`` in +``$XDG_CONFIG_HOME/gtk-3.0`` or files in +``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment +variable ``GTK_THEME`` (search on internet for the various +possibilities). The fourth section is for customizing the editor. It includes in particular the ability to activate an Emacs mode named @@ -206,7 +206,7 @@ Displaying Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~ You just need to define suitable notations as described in the chapter -:ref:`syntaxextensionsandinterpretationscopes`. For example, to use the +:ref:`syntax-extensions-and-notation-scopes`. For example, to use the mathematical symbols ∀ and ∃, you may define: .. coqtop:: in diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index d61e5ddce7..408f8fc3ec 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -42,6 +42,8 @@ As of today it is possible to build Coq projects using two tools: - coq_makefile, which is distributed by Coq and is based on generating a makefile, - Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries. +.. _coq_makefile: + Building a |Coq| project with coq_makefile ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -243,16 +245,17 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (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 + ``time-of-build.log``, and displays a table of the times and peak + memory usages, 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"``. .. note:: @@ -269,24 +272,29 @@ file timing data: ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times rather than user times in the table. + .. note:: + Passing ``TIMING_INCLUDE_MEM=0`` to ``make`` will result in the + tables not including peak memory usage information. Passing + ``TIMING_SORT_BY_MEM=1`` to ``make`` will result in the tables + be sorted by peak memory usage rather than by the time taken. + .. example:: For example, the output of ``make pretty-timed`` may look like this: :: - COQDEP Fast.v - COQDEP Slow.v + COQDEP VFILES COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (real: 0.52, user: 0.39, sys: 0.12, mem: 394648 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) - Time | File Name - -------------------- - 0m00.41s | Total - -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + Fast.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 56980 ko) + Time | Peak Mem | File Name + -------------------------------------------- + 0m00.41s | 394648 ko | Total Time / Peak Mem + -------------------------------------------- + 0m00.39s | 394648 ko | Slow.vo + 0m00.02s | 56980 ko | Fast.vo + ``print-pretty-timed-diff`` @@ -323,7 +331,15 @@ file timing data: .. note:: Just like ``pretty-timed``, this table defaults to using user - times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line + to show real times instead. + + .. note:: + Just like ``pretty-timed``, passing ``TIMING_INCLUDE_MEM=0`` to + ``make`` will result in the tables not including peak memory + usage information. Passing ``TIMING_SORT_BY_MEM=1`` to + ``make`` will result in the tables be sorted by peak memory + usage rather than by the time taken. .. example:: @@ -332,12 +348,12 @@ file timing data: :: - 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% + After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) + ----------------------------------------------------------------------------------------------------------------------------- + 0m00.43s | 394700 ko | Total Time / Peak Mem | 0m00.41s | 394648 ko || +0m00.01s || 52 ko | +4.87% | +0.01% + ----------------------------------------------------------------------------------------------------------------------------- + 0m00.39s | 394700 ko | Fast.vo | 0m00.02s | 56980 ko || +0m00.37s || 337720 ko | +1850.00% | +592.69% + 0m00.04s | 56772 ko | Slow.vo | 0m00.39s | 394648 ko || -0m00.35s || -337876 ko | -89.74% | -85.61% The following targets and ``Makefile`` variables allow collection of per- |