diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 69 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 10 |
2 files changed, 72 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d20a82e6c0..a10312972e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -43,7 +43,7 @@ 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 named *file*.v, and tries to compile it into a *file*.vo file (See :ref:`compiled-files`). .. caution:: @@ -219,6 +219,71 @@ and ``coqtop``, unless stated otherwise: :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-verbose: Output the content of the input file as it is compiled. This option is available for ``coqc`` only. +:-native-compiler (yes|no|ondemand): Enable the :tacn:`native_compute` + reduction machine and precompilation to ``.cmxs`` files for future use + by :tacn:`native_compute`. + Setting ``yes`` enables :tacn:`native_compute`; it also causes Coq + to precompile the native code for future use; all dependencies need + to have been precompiled beforehand. Setting ``no`` disables + :tacn:`native_compute` which defaults back to :tacn:`vm_compute`; no files are precompiled. + Setting ``ondemand`` enables :tacn:`native_compute` + but disables precompilation; all missing dependencies will be recompiled + every time :tacn:`native_compute` is called. + + .. _native-compiler-options: + + .. versionchanged:: 8.13 + + The default value is set at configure time, + ``-config`` can be used to retrieve it. + All this can be summarized in the following table: + + .. list-table:: + :header-rows: 1 + + * - ``configure`` + - ``coqc`` + - ``native_compute`` + - outcome + - requirements + * - yes + - yes (default) + - native_compute + - ``.cmxs`` + - ``.cmxs`` of deps + * - yes + - no + - vm_compute + - none + - none + * - yes + - ondemand + - native_compute + - none + - none + * - no + - yes, no, ondemand + - vm_compute + - none + - none + * - ondemand + - yes + - native_compute + - ``.cmxs`` + - ``.cmxs`` of deps + * - ondemand + - no + - vm_compute + - none + - none + * - ondemand + - ondemand (default) + - native_compute + - none + - none + +:-native-output-dir: Set the directory in which to put the aforementioned + ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``. :-vos: Indicate Coq to skip the processing of opaque proofs (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files @@ -434,7 +499,7 @@ 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. +information, we mean the type and optional body associated with 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. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index c239797cc2..dcc60195ed 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -7,7 +7,7 @@ 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 +allow the user to navigate forward and backward into a Coq file, executing corresponding commands or undoing them respectively. CoqIDE is run by typing the command `coqide` on the command line. @@ -100,10 +100,10 @@ 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. -Vernacular commands, templates ------------------------------------ +Commands and templates +---------------------- -The Templates menu allows using shortcuts to insert vernacular +The Templates menu allows using shortcuts to insert commands. This is a nice way to proceed if you are not sure of the syntax of the command you want. @@ -116,7 +116,7 @@ Queries .. image:: ../_static/coqide-queries.png :alt: CoqIDE queries -We call *query* any vernacular command that does not change the current state, +We call *query* any 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``. |