From 797eb524853e361f84c9c776024c142107f0c282 Mon Sep 17 00:00:00 2001 From: charguer Date: Thu, 12 Dec 2019 10:48:50 +0100 Subject: Fix #11195 and add other improvements: try loading .vio (and not just .vo) if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio. --- .../11280-bugfix-11195-vos-vio-interaction.rst | 4 ++++ doc/sphinx/addendum/parallel-proof-processing.rst | 18 +++++++++++++++--- doc/sphinx/practical-tools/coq-commands.rst | 1 + 3 files changed, 20 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst (limited to 'doc') diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst new file mode 100644 index 0000000000..97f456036d --- /dev/null +++ b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated. + (`#11280 `_, + by charguer). diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 35729d852d..7a50748c51 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with Batch mode --------------- + .. warning:: + + The ``-vio`` flag is subsumed, for most practical usage, by the + the more recent ``-vos`` flag. See :ref:`compiled-interfaces`. + + .. warning:: + + When working with ``.vio`` files, do not use the ``-vos`` option at + the same time, otherwise stale files might get loaded when executing + a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is + assigned higher priority than the loading of a ``.vio`` file. + When |Coq| is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other things, theorem statements and proofs. Hence to produce a .vo |Coq| @@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the -generation and checking of the proof objects. The ``-quick`` flag can be +generation and checking of the proof objects. The ``-vio`` flag can be passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, -the ``quick`` target can be used to compile all files using the ``-quick`` flag. +the ``vio`` target can be used to compile all files using the ``-vio`` flag. A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). @@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. -Compiling a set of files with the ``-quick`` flag allows one to work, +Compiling a set of files with the ``-vio`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..ba43128bdc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- -- cgit v1.2.3