Merge PR #8642: Compiled interfaces with -vos and -vok options

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

2 files changed, 127 insertions, 0 deletions

diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst
new file mode 100644
index 0000000000..f612096880
--- /dev/null
+++ b/doc/changelog/08-tools/08642-vos-files.rst
@@ -0,0 +1,7 @@
+- `coqc` now provides the ability to generate compiled interfaces.
+  Use `coqc -vos foo.v` to skip all opaque proofs during the
+  compilation of `foo.v`, and output a file called `foo.vos`.
+  This feature is experimental. It enables working on a Coq file without the need to
+  first compile the proofs contained in its dependencies
+  (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by
+  Maxime Dénès and Emilio Gallego).
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)
 ----------------------------------------