diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 67 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 229 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 2 |
4 files changed, 300 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst new file mode 100644 index 0000000000..b0343a8f01 --- /dev/null +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -0,0 +1,67 @@ +.. include:: ../replaces.rst + +.. _miscellaneousextensions: + +Miscellaneous extensions +======================= + +:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html +:Converted by: Paul Steckler + +.. contents:: + :local: + :depth: 1 +---- + +Program derivation +----------------- + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.Derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident SuchThat @term As @ident + +The first `ident` can appear in `term`. This command opens a new proof +presenting the user with a goal for term in which the name `ident` is +bound to an existential variable `?x` (formally, there are other goals +standing for the existential variables but they are shelved, as +described in Section :ref:`TODO-8.17.4`). + +When the proof ends two constants are defined: + ++ The first one is named using the first `ident` and is defined as the proof of the + shelved goal (which is also the value of `?x`). It is always + transparent. ++ The second one is named using the second `ident`. It has type `term`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with ``Qed``, and transparent if the proof ends with ``Defined``. + +.. example:: + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +Any property can be used as `term`, not only an equation. In particular, +it could be an order relation specifying some form of program +refinement or a non-executable property from which deriving a program +is convenient. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst new file mode 100644 index 0000000000..8c1b9d152b --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,229 @@ +.. include:: ../replaces.rst + +.. _asynchronousandparallelproofprocessing: + +Asynchronous and Parallel Proof Processing +========================================== + +:Author: Enrico Tassi + +This chapter explains how proofs can be asynchronously processed by +|Coq|. This feature improves the reactivity of the system when used in +interactive mode via |CoqIDE|. In addition, it allows |Coq| to take +advantage of parallel hardware when used as a batch compiler by +decoupling the checking of statements and definitions from the +construction and checking of proofs objects. + +This feature is designed to help dealing with huge libraries of +theorems characterized by long proofs. In the current state, it may +not be beneficial on small sets of short files. + +This feature has some technical limitations that may make it +unsuitable for some use cases. + +For example, in interactive mode, some errors coming from the kernel +of |Coq| are signaled late. The type of errors belonging to this +category are universe inconsistencies. + +At the time of writing, only opaque proofs (ending with ``Qed`` or +``Admitted``) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running |CoqIDE| in +Windows. The current implementation of the feature is not stable on +Windows. It can be enabled, as described below at :ref:`interactive-mode`, +though doing so is not recommended. + +Proof annotations +---------------------- + +To process a proof asynchronously |Coq| needs to know the precise +statement of the theorem without looking at the proof. This requires +some annotations if the theorem is proved inside a Section (see +Section :ref:`TODO-2.4`). + +When a section ends, |Coq| looks at the proof object to decide which +section variables are actually used and hence have to be quantified in +the statement of the theorem. To avoid making the construction of +proofs mandatory when ending a section, one can start each proof with +the ``Proof using`` command (Section :ref:`TODO-7.1.5`) that declares which section +variables the theorem uses. + +The presence of ``Proof`` using is needed to process proofs asynchronously +in interactive mode. + +It is not strictly mandatory in batch mode if it is not the first time +the file is compiled and if the file itself did not change. When the +proof does not begin with Proof using, the system records in an +auxiliary file, produced along with the `.vo` file, the list of section +variables used. + +Automatic suggestion of proof annotations +````````````````````````````````````````` + +The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +command is processed, a correct proof annotation. It is up to the user +to modify the proof script accordingly. + + +Proof blocks and error resilience +-------------------------------------- + +|Coq| 8.6 introduced a mechanism for error resiliency: in interactive +mode |Coq| is able to completely check a document containing errors +instead of bailing out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular +commands and errors occurring in proofs. + +To properly recover from a failing tactic, |Coq| needs to recognize the +structure of the proof in order to confine the error to a sub proof. +Proof block detection is performed by looking at the syntax of the +proof script (i.e. also looking at indentation). |Coq| comes with four +kind of proof blocks, and an ML API to add new ones. + +:curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling` +:par: blocks are atomic, i.e. just one tactic introduced by the `par:` + goal selector +:indent: blocks end with a tactic indented less than the previous one +:bullet: blocks are delimited by two equal bullet signs at the same + indentation level + +Caveats +```````` + +When a vernacular command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resiliency for vernacular +commands can be switched off by passing ``-async-proofs-command-error-resilience off`` +to |CoqIDE|. + +An incorrect proof block detection can result into an incorrect error +recovery and hence in bogus errors. Proof block detection cannot be +precise for bullets or any other non well parenthesized proof +structure. Error resiliency can be turned off or selectively activated +for any set of block kind passing to |CoqIDE| one of the following +options: + +- ``-async-proofs-tactic-error-resilience off`` +- ``-async-proofs-tactic-error-resilience all`` +- ``-async-proofs-tactic-error-resilience`` :n:`{*, blocktype}` + +Valid proof block types are: “curly”, “par”, “indent”, and “bullet”. + +.. _interactive-mode: + +Interactive mode +--------------------- + +At the time of writing the only user interface supporting asynchronous +proof processing is |CoqIDE|. + +When |CoqIDE| is started, two |Coq| processes are created. The master one +follows the user, giving feedback as soon as possible by skipping +proofs, which are delegated to the worker process. The worker process, +whose state can be seen by clicking on the button in the lower right +corner of the main |CoqIDE| window, asynchronously processes the proofs. +If a proof contains an error, it is reported in red in the label of +the very same button, that can also be used to see the list of errors +and jump to the corresponding line. + +If a proof is processed asynchronously the corresponding Qed command +is colored using a lighter color that usual. This signals that the +proof has been delegated to a worker process (or will be processed +lazily if the ``-async-proofs lazy`` option is used). Once finished, the +worker process will provide the proof object, but this will not be +automatically checked by the kernel of the main process. To force the +kernel to check all the proof objects, one has to click the button +with the gears. Only then are all the universe constraints checked. + +Caveats +``````` + +The number of worker processes can be increased by passing |CoqIDE| +the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, +since each worker requires the same amount of memory as the master +process. Also note that increasing the number of workers may reduce +the reactivity of the master process to user commands. + +To disable this feature, one can pass the ``-async-proofs off`` flag to +|CoqIDE|. Conversely, on Windows, where the feature is disabled by +default, pass the ``-async-proofs on`` flag to enable it. + +Proofs that are known to take little time to process are not delegated +to a worker process. The threshold can be configure with +``-async-proofs-delegation-threshold``. Default is 0.03 seconds. + +Batch mode +--------------- + +When |Coq| is used as a batch compiler by running `coqc` or `coqtop` +-compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, +among other things, theorems statements and proofs. Hence to produce a +.vo |Coq| 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 +passed to `coqc` or `coqtop` 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. + +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). +Moreover, some universe constraints might be missing, so universes +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, +interactively, on any file without waiting for all the proofs to be +checked. + +When working interactively, one can fully check all the `.v` files by +running `coqc` as usual. + +Alternatively one can turn each `.vio` into the corresponding `.vo`. All +.vio files can be processed in parallel, hence this alternative might +be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and +`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target +can be used for that purpose. Variable `J` should be set to the number +of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the +.vo files obtained from `.vio` files are complete (they contain all proof +terms and universe constraints), the satisfiability of all universe +constraints has not been checked globally (they are checked to be +consistent for every single proof). Constraints will be checked when +these `.vo` files are (recursively) loaded with ``Require``. + +There is an extra, possibly even faster, alternative: just check the +proof tasks stored in `.vio` files without producing the `.vo` files. This +is possibly faster because all the proof tasks are independent, hence +one can further partition the job to be done between workers. The +``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +good scheduling for 6 workers to check all the proof tasks of `a.vio`, +`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof +task will take, assuming it will take the same amount of time it took +last time. When using a Makefile produced by coq_makefile, the +``checkproofs`` target can be used to check all `.vio` files. Variable `J` +should be set to the number of workers, e.g. ``make checkproofs J=6``. As +when converting `.vio` files to `.vo` files, universe constraints are not +checked to be globally consistent. Hence this compilation mode is only +useful for quick regression testing and on developments not making +heavy use of the `Type` hierarchy. + +Limiting the number of parallel workers +-------------------------------------------- + +Many |Coq| processes may run on the same computer, and each of them may +start many additional worker processes. The `coqworkmgr` utility lets +one limit the number of workers, globally. + +The utility accepts the ``-j`` argument to specify the maximum number of +workers (defaults to 2). `coqworkmgr` automatically starts in the +background and prints an environment variable assignment +like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable +in all the shells from which |Coq| processes will be started. If one +uses just one terminal running the bash shell, then +``export ‘coqworkmgr -j 4‘`` will do the job. + +After that, all |Coq| processes, e.g. `coqide` and `coqc`, will honor the +limit, globally. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index a60f326454..fac0d0a4f9 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -376,7 +376,7 @@ contributed by Jean Goubault was integrated in the basic theories. Pierre Courtieu developed a command and a tactic to reason on the inductive structure of recursively defined functions. -Jacek Chrzszcz designed and implemented the module system of |Coq| whose +Jacek Chrząszcz designed and implemented the module system of |Coq| whose foundations are in Judicaël Courant’s PhD thesis. The development was coordinated by C. Paulin. @@ -478,7 +478,7 @@ Marché and Bruno Barras. Claude Marché coordinated the edition of the Reference Manual for |Coq| V8.0. -Pierre Letouzey and Jacek Chrzszcz respectively maintained the +Pierre Letouzey and Jacek Chrząszcz respectively maintained the extraction tool and module system of |Coq|. Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 75e9551369..db03693ff9 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -54,6 +54,8 @@ Table of contents addendum/ring addendum/nsatz addendum/generalized-rewriting + addendum/parallel-proof-processing + addendum/miscellaneous-extensions .. toctree:: :caption: Reference |