Document the changes regarding the order of command-line options.

2 files changed, 62 insertions, 24 deletions

diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
index a07e48d2d8..ff736641b4 100644
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
@@ -1,6 +1,9 @@
 - **Changed:**
-  The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc.
-  and the option set flags `-set`, `-unset` are processed have been reversed.
-  In the new behavior, require/load flags are processed before option flags.
-  (`#11851 <https://github.com/coq/coq/pull/11851>`_,
+  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
+  and the option flags `-set`, `-unset` are given now matters.  In
+  particular, it is now possible to interleave the loading of plugins
+  and the setting of options by choosing the right order for these
+  flags.  The load flags `-l` and `-lv` are still processed afterward
+  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
+  `#12097 <https://github.com/coq/coq/pull/12097>`_,
   by Lasse Blaauwbroek).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 545bba4930..ca167c8b4b 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise:
   while processing options such as -R and -Q. By default, only the
   conventional version control management directories named CVS
   and_darcs are excluded.
-:-nois: Start from an empty state instead of loading the Init.Prelude
+:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude`
   module.
 :-init-file *file*: Load *file* as the resource file instead of
   loading the default resource file from the standard configuration
@@ -163,17 +163,44 @@ and ``coqtop``, unless stated otherwise:
   |Coq| script from *file.v*. Write its contents to the standard output as
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
-  is equivalent to running :cmd:`Require` :n:`qualid`.
+  is equivalent to running :cmd:`Require` :n:`@qualid`.
+
+  .. _interleave-command-line:
+
+  .. note::
+
+     Note that the relative order of this command-line option and its
+     variants (`-rfrom`, `-ri`, `-re`, etc.)  and of the `-set` and
+     `-unset` options matters since the various :cmd:`Require`,
+     :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and
+     :cmd:`Unset` commands will be executed in the order specified on
+     the command-line.
+
 :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
-:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
-  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`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and import it.  This is
+  equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath`
+  :cmd:`Require Import <From ... Require>` :n:`@qualid`.  See the
+  :ref:`note above <interleave-command-line>` regarding the order of
+  command-line options.
+:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and transitively import it.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the
+  order of command-line options.
 :-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
@@ -184,11 +211,11 @@ and ``coqtop``, unless stated otherwise:
   This option is available for ``coqc`` only; it is the counterpart of
   -compile-verbose.
 :-vos: Indicate |Coq| to skip the processing of opaque proofs
-  (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files
+  (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
-  when interpreting ``Require`` commands.
+  when interpreting :cmd:`Require` commands.
 :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
-  of ``.vo`` files when interpreting ``Require`` commands, and to output an empty
+  of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty
   ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
@@ -198,7 +225,7 @@ and ``coqtop``, unless stated otherwise:
   the output channel supports ANSI escape sequences.
 :-diffs (on|off|removed): *Coqtop only*.  Controls highlighting of differences
   between proof steps.  ``on`` highlights added tokens, ``removed`` highlights both added and
-  removed tokens.  Requires that ``–color`` is enabled.  (see Section
+  removed tokens.  Requires that ``-color`` is enabled.  (see Section
   :ref:`showing_diffs`).
 :-beautify: Pretty-print each command to *file.beautified* when
   compiling *file.v*, in order to get old-fashioned
@@ -224,17 +251,25 @@ and ``coqtop``, unless stated otherwise:
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-set *string*: Enable flags and set options. *string* should be
-   ``Option Name=value``, the value is interpreted according to the
-   type of the option. For flags ``Option Name`` is equivalent to
-   ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
+   :n:`@setting_name=value`, the value is interpreted according to the
+   type of the option. For flags :n:`@setting_name` is equivalent to
+   :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   shell syntax, Coq does not see them. Flags are processed after initialization
-   of the document. This includes the `Prelude` if loaded and any libraries loaded
-   through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom`
-   options.
+   shell syntax, Coq does not see them.
+   See the :ref:`note above <interleave-command-line>` regarding the order
+   of command-line options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
-:-compat *version*: Attempt to maintain some backward-compatibility
-  with a previous version.
+  *string* must be :n:`"@setting_name"`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-compat *version*: Load a file that sets a few options to maintain
+  partial backward-compatibility with a previous version.  This is
+  equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX`
+  one of the last three released versions (including the current
+  version).  Note that the :ref:`explanations above
+  <interleave-command-line>` regarding the order of command-line
+  options apply, and this could be relevant if you are resetting some
+  of the compatibility options.
 :-dump-glob *file*: Dump references for global names in file *file*
   (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.