From 72dc33fb0f99d403e8693db178a73c1e28096400 Mon Sep 17 00:00:00 2001 From: charguer Date: Thu, 8 Nov 2018 16:50:13 +0100 Subject: Implementing support for vos/vok files. A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file. --- doc/sphinx/practical-tools/coq-commands.rst | 87 +++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 48d5f4075e..be74b86b30 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,86 @@ 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.) + + .. warning:: + + In the current implementation, the use of the command ``Include`` for + importing modules compiled using `-vos` might not work properly. + + +**Typical usage.** + +Assume a file ``foo.v`` that depends on two files ``bar1.v`` and ``bar2.v``. The +command ``make foo.requires_vos`` will compile ``bar1.v`` and ``bar2.v`` using +the option ``-vos`` to skip the proofs, producing ``bar1.vos`` and ``bar2.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 ``bar*.v`` +files. + +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) ---------------------------------------- -- cgit v1.2.3 From a779415f6c39cebcb0384dec0673cde71c05e3b2 Mon Sep 17 00:00:00 2001 From: charguer Date: Thu, 28 Mar 2019 15:39:04 +0100 Subject: additional details in the doc for -vos --- doc/sphinx/practical-tools/coq-commands.rst | 51 +++++++++++++++++++++++------ 1 file changed, 41 insertions(+), 10 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index be74b86b30..9da565aa3c 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -257,7 +257,6 @@ and ``coqtop``, unless stated otherwise: 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. @@ -269,20 +268,52 @@ the proofs that it contains. by producing standard ``.vo`` files. (Technically, when using ``-vos``, fewer universe constraints are collected.) - .. warning:: +**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``. - In the current implementation, the use of the command ``Include`` for - importing modules compiled using `-vos` might not work properly. +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 usage.** +**Typical compilation of a set of file using a build system.** -Assume a file ``foo.v`` that depends on two files ``bar1.v`` and ``bar2.v``. The -command ``make foo.requires_vos`` will compile ``bar1.v`` and ``bar2.v`` using -the option ``-vos`` to skip the proofs, producing ``bar1.vos`` and ``bar2.vos``. +Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The +command ``make foo.requires_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 ``bar*.v`` -files. +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 -- cgit v1.2.3 From fb6afb4a7256b33725660668738bc17c84ae94f5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 23 Oct 2019 15:10:14 +0200 Subject: Changelog entry --- doc/changelog/08-tools/08642-vos-files.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/08-tools/08642-vos-files.rst (limited to 'doc') 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..24a610c56b --- /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 enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 `_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). -- cgit v1.2.3 From 5efdfe979fd316372c59d9406fa7ade46aa6814a Mon Sep 17 00:00:00 2001 From: charguer Date: Fri, 25 Oct 2019 13:13:43 +0200 Subject: fix coq_makefile and doc for vos support. --- doc/sphinx/practical-tools/coq-commands.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9da565aa3c..d8325287cc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -309,7 +309,7 @@ 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.requires_vos`` will compile ``f1.v`` and ``f2.v`` using +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`` -- cgit v1.2.3 From c5ce7dfe595beaced11646e3aed7e3532a1353f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Nov 2019 12:19:57 +0100 Subject: Add warnings regarding the experimental nature of the vos feature in the doc. --- doc/changelog/08-tools/08642-vos-files.rst | 2 +- doc/sphinx/practical-tools/coq-commands.rst | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst index 24a610c56b..f612096880 100644 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -1,7 +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 enables working on a Coq file without the need to + This feature is experimental. It enables working on a Coq file without the need to first compile the proofs contained in its dependencies (`#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 d8325287cc..70259ff565 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -267,6 +267,8 @@ the proofs that it contains. 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.** -- cgit v1.2.3