Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and not just…

Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot

3 files changed, 20 insertions, 3 deletions

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 <https://github.com/coq/coq/pull/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``)
 ----------------------------------------------