3 files changed, 133 insertions, 12 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 48d5f4075e..70259ff565 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -184,6 +184,13 @@ and ``coqtop``, unless stated otherwise:
 :-verbose: Output the content of the input file as it is compiled.
   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
+  instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
+  when interpreting ``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
+  ``.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
   categories (see Section :ref:`controlling-display`).
@@ -245,6 +252,119 @@ and ``coqtop``, unless stated otherwise:
   currently associated color and exit.
 :-h, --help: Print a short usage and exit.
 
+
+
+Compiled interfaces (produced using ``-vos``)
+----------------------------------------------
+
+Compiled interfaces help saving time while developing Coq formalizations,
+by compiling the formal statements exported by a library independently of
+the proofs that it contains.
+
+   .. warning::
+
+      Compiled interfaces should only be used for development purposes.
+      At the end of the day, one still needs to proof check all files
+      by producing standard ``.vo`` files. (Technically, when using ``-vos``,
+      fewer universe constraints are collected.)
+      Moreover, this feature is still experimental, it may be subject to
+      change without prior notice.
+
+**Principle.**
+
+The compilation using ``coqc -vos foo.v`` produces a file called ``foo.vos``,
+which is similar to ``foo.vo`` except that all opaque proofs are skipped in
+the compilation process.
+
+The compilation using ``coqc -vok foo.v`` checks that the file ``foo.v``
+correctly compiles, including all its opaque proofs. If the compilation
+succeeds, then the output is a file called ``foo.vok``, with empty contents.
+This file is only a placeholder indicating that ``foo.v`` has been successfully
+compiled. (This placeholder is useful for build systems such as ``make``.)
+
+When compiling a file ``bar.v`` that depends on ``foo.v`` (for example via
+a ``Require Foo.`` command), if the compilation command is ``coqc -vos bar.v``
+or ``coqc -vok bar.v``, then the file ``foo.vos`` gets loaded (instead of
+``foo.vo``). A special case is if file ``foo.vos`` exists and has empty
+contents, and ``foo.vo`` exists, then ``foo.vo`` is loaded.
+
+Appart from the aforementioned case where ``foo.vo`` can be loaded in place
+of ``foo.vos``, in general the ``.vos`` and ``.vok`` files live totally
+independently from the ``.vo`` files.
+
+**Dependencies generated by ``coq_makefile``.**
+
+The files ``foo.vos`` and ``foo.vok`` both depend on ``foo.v``.
+
+Furthermore, if a file ``foo.v`` requires ``bar.v``, then ``foo.vos``
+and ``foo.vok`` also depend on ``bar.vos``.
+
+Note, however, that ``foo.vok`` does not depend on ``bar.vok``.
+Hence, as detailed further, parallel compilation of proofs is possible.
+
+In addition, ``coq_makefile`` generates for a file ``foo.v`` a target
+``foo.required_vos`` which depends on the list of ``.vos`` files that
+``foo.vos`` depends upon (excluding ``foo.vos`` itself). As explained
+next, the purpose of this target is to be able to request the minimal
+working state for editing interactively the file ``foo.v``.
+
+**Typical compilation of a set of file using a build system.**
+
+Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The
+command ``make foo.required_vos`` will compile ``f1.v`` and ``f2.v`` using
+the option ``-vos`` to skip the proofs, producing ``f1.vos`` and ``f2.vos``.
+At this point, one is ready to work interactively on the file ``foo.v``, even
+though it was never needed to compile the proofs involved in the files ``f1.v``
+and ``f2.v``.
+
+Assume a set of files ``f1.v ... fn.v`` with linear dependencies. The command
+``make vos`` enables compiling the statements (i.e. excluding the proofs) in all
+the files. Next, ``make -j vok`` enables compiling all the proofs in parallel.
+Thus, calling ``make -j vok`` directly enables taking advantage of a maximal
+amount of parallelism during the compilation of the set of files.
+
+Note that this comes at the cost of parsing and typechecking all definitions
+twice, once for the ``.vos`` file and once for the ``.vok`` file. However, if
+files contain nontrivial proofs, or if the files have many linear chains of
+dependencies, or if one has many cores available, compilation should be faster
+overall.
+
+**Need for ``Proof using``**
+
+When a theorem is part of a section, typechecking the statement of this theorem
+might be insufficient for deducing the type of this statement as of at the end
+of the section. Indeed, the proof of the theorem could make use of section
+variables or section hypotheses that are not mentioned in the statement of the
+theorem.
+
+For this reason, proofs inside section should begin with :cmd:`Proof using`
+instead of :cmd:`Proof`, where after the ``using`` clause one should provide
+the list of the names of the section variables that are required for the proof
+but are not involved in the typechecking of the statement. Note that it is safe
+to write ``Proof using.`` instead of ``Proof.`` also for proofs that are not
+within a section.
+
+.. warn:: You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof.
+
+     If |Coq| is invoked using the ``-vos`` option, whenever it finds the
+     command ``Proof.`` inside a section, it will compile the proof, that is,
+     refuse to skip it, and it will raise a warning. To disable the warning, one
+     may pass the flag ``-w -proof-without-using-in-section``.
+
+**Interaction with standard compilation**
+
+When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., without
+``-vos`` nor ``-vok``), an empty file ``foo.vos`` is created in addition to the
+regular output file ``foo.vo``. If ``coqc`` is subsequently invoked on some other
+file ``bar.v`` using option ``-vos`` or ``-vok``, and that ``bar.v`` requires
+``foo.v``, if |Coq| finds an empty file ``foo.vos``, then it will load
+``foo.vo`` instead of ``foo.vos``.
+
+The purpose of this feature is to allow users to benefit from the ``-vos``
+option even if they depend on libraries that were compiled in the traditional
+manner (i.e., never compiled using the ``-vos`` option).
+
+
 Compiled libraries checker (coqchk)
 ----------------------------------------
 
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 7d6171285e..b1f392c337 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -179,10 +179,13 @@ compilation, printing, web browsing. In the browser command, you may
 use `%s` to denote the URL to open, for example:
 `firefox -remote "OpenURL(%s)"`.
 
-Notice that these settings are saved in the file `.coqiderc` of your
-home directory.
+Notice that these settings are saved in the file ``coqiderc`` in the
+``coq`` subdirectory of the user configuration directory which
+is the value of ``$XDG_CONFIG_HOME`` if this environment variable is
+set and which otherwise is ``$HOME/.config/``.
 
-A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It
+A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in
+the same ``coq`` subdirectory of the user configuration directory. It
 is not recommended to edit this file manually: to modify a given menu
 shortcut, go to the corresponding menu item without releasing the
 mouse button, press the key you want for the new shortcut, and release
@@ -259,8 +262,9 @@ Adding custom bindings
 ~~~~~~~~~~~~~~~~~~~~~~
 
 To extend the default set of bindings, create a file named ``coqide.bindings``
-and place it in the same folder as ``coqide.keys``. On Linux, this would be
-the folder ``~/.config/coq``. The file `coqide.bindings` should contain one
+and place it in the same folder as ``coqide.keys``. This would be
+the folder ``$XDG_CONFIG_HOME/coq``, defaulting to ``~/.config/coq``
+if ``XDG_CONFIG_HOME`` is unset. The file `coqide.bindings` should contain one
 binding per line, in the form ``\key value``, followed by an optional priority
 integer. (The key and value should not contain any space character.)
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 554f6bf230..e5edd08995 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows:
     theories/foo.v
     theories/bar.v
     -I src/
-    src/baz.ml4
+    src/baz.mlg
     src/bazaux.ml
     src/qux_plugin.mlpack
 
@@ -111,7 +111,7 @@ decide how to build them. In particular:
 + |Coq| files must use the ``.v`` extension
 + |OCaml| files must use the ``.ml`` or ``.mli`` extension
 + |OCaml| files that require pre processing for syntax
-  extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension
+  extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
 + In order to generate a plugin one has to list all |OCaml|
   modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
   file).
@@ -359,7 +359,7 @@ line timing data:
     pass  ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``.
 
     .. note::
-       The sorting used here is the same as in the ``print-pretty-timed -diff`` target.
+       The sorting used here is the same as in the ``print-pretty-timed-diff`` target.
 
     .. note::
        This target requires python to build the table.
@@ -522,10 +522,7 @@ of your project.
         (flags :standard -warn-error -3-9-27-32-33-50)
         (libraries coq.plugins.cc coq.plugins.extraction))
 
-       (rule
-        (targets g_equations.ml)
-        (deps (:pp-file g_equations.mlg))
-        (action (run coqpp %{pp-file})))
+       (coq.pp (modules g_equations))
 
    And a Coq-specific part that depends on it via the ``libraries`` field: