diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/README.md | 10 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 65 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 5 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 5 |
5 files changed, 89 insertions, 10 deletions
diff --git a/doc/README.md b/doc/README.md index 79d1e1b756..440b104c16 100644 --- a/doc/README.md +++ b/doc/README.md @@ -69,6 +69,16 @@ Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ latexmk fonts-freefont-otf +### Setting the locale for Python + +Make sure that the locale is configured on your platform so that Python encodes +printed messages with utf-8 rather than generating runtime exceptions +for non-ascii characters. The `.UTF-8` in `export LANG=C.UTF-8` sets UTF-8 encoding. +The `C` can be replaced with any supported language code. You can set the default +for a Docker build with `ENV LANG C.UTF-8`. (Python may look at other +environment variables to determine the locale; see the +[Python documentation](https://docs.python.org/3/library/locale.html#locale.getdefaultlocale)). + Compilation ----------- diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 7ad2605f4a..a10312972e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -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 diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index a750ce2892..766f7ab44e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1654,17 +1654,21 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacv:: instantiate (@natural := @term) - This variant allows to refer to an existential variable which was not named - by the user. The :n:`@natural` argument is the position of the existential variable - from right to left in the goal. Because this variant is not robust to slight - changes in the goal, its use is strongly discouraged. + This variant selects an existential variable by its position. The + :n:`@natural` argument is the position of the existential variable + *from right to left* in the conclusion of the goal. (Use one of + the variants below to select an existential variable in a + hypothesis.) Counting starts at 1 and multiple occurrences of the + same existential variable are counted multiple times. Because this + variant is not robust to slight changes in the goal, its use is + strongly discouraged. .. tacv:: instantiate ( @natural := @term ) in @ident instantiate ( @natural := @term ) in ( value of @ident ) instantiate ( @natural := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a - hypothesis or in the body or the type of a local definition. + hypothesis or in the body or the type of a local definition (named :n:`@ident`). .. tacv:: instantiate diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index c54701b153..07b7928847 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -487,7 +487,10 @@ the conversion in hypotheses :n:`{+ @ident}`. in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive - computations. + computations. Depending on the configuration, this tactic can either default to + :tacn:`vm_compute`, recompile dependencies or fail due to some missing + precompiled dependencies, + see :ref:`the native-compiler option <native-compiler-options>` for details. .. flag:: NativeCompute Timing diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index e24e534024..fa739e97bc 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -220,10 +220,7 @@ class CoqObject(ObjectDescription): # todo: then maybe the above "if" is not needed names_in_subdomain = self.subdomain_data() if name in names_in_subdomain: - try: - print("Duplicate", self.subdomain, "name: ", name) - except UnicodeEncodeError: # in CI - print("*** UnicodeEncodeError") + print("Duplicate", self.subdomain, "name: ", name) # self._warn_if_duplicate_name(names_in_subdomain, name, signode) return targetid |