diff options
| author | Théo Zimmermann | 2020-11-09 18:39:49 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-09 18:39:49 +0100 |
| commit | a3869e5371c89629ddfd8ccdd1bdc0de12efe806 (patch) | |
| tree | d2791aae79a76984f76989bd560989dd0faff8a2 /doc/sphinx | |
| parent | 87523f151484dcc4eff4f04535b9356036b51a3d (diff) | |
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
Diffstat (limited to 'doc/sphinx')
57 files changed, 981 insertions, 986 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4461ff9240..bfdbc4c4db 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -551,7 +551,7 @@ Add either ``abort`` to the first block or ``reset`` to the second block to avoi Abbreviations and macros ------------------------ -Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Ltac|`` and ``|Latex|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index b4e21aa14a..d4e297299e 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -290,7 +290,7 @@ Add either ``abort`` to the first block or ``reset`` to the second block to avoi Abbreviations and macros ------------------------ -Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Ltac|`` and ``|Latex|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 96e115fc3d..3662822a5e 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -5,10 +5,10 @@ Program extraction :Authors: Jean-Christophe Filliâtre and Pierre Letouzey -We present here the |Coq| extraction commands, used to build certified +We present here the Coq extraction commands, used to build certified and relatively efficient functional programs, extracting them from -either |Coq| functions or |Coq| proofs of specifications. The -functional languages available as output are currently |OCaml|, Haskell +either Coq functions or Coq proofs of specifications. The +functional languages available as output are currently OCaml, Haskell and Scheme. In the following, "ML" will be used (abusively) to refer to any of the three. @@ -16,7 +16,7 @@ Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly via ``Require Extraction``, or via the more robust ``From Coq Require Extraction``. -Note that in earlier versions of |Coq|, these commands and options were +Note that in earlier versions of Coq, these commands and options were directly available without any preliminary ``Require``. .. coqtop:: in @@ -29,23 +29,23 @@ Generating ML Code .. note:: In the following, a qualified identifier :token:`qualid` - can be used to refer to any kind of |Coq| global "object" : constant, + can be used to refer to any kind of Coq global "object" : constant, inductive type, inductive constructor or module name. The next two commands are meant to be used for rapid preview of -extraction. They both display extracted term(s) inside |Coq|. +extraction. They both display extracted term(s) inside Coq. .. cmd:: Extraction @qualid - Extraction of the mentioned object in the |Coq| toplevel. + Extraction of the mentioned object in the Coq toplevel. .. cmd:: Recursive Extraction {+ @qualid } Recursive extraction of all the mentioned objects and - all their dependencies in the |Coq| toplevel. + all their dependencies in the Coq toplevel. All the following commands produce real ML files. User can choose to -produce one monolithic file or one file per |Coq| library. +produce one monolithic file or one file per Coq library. .. cmd:: Extraction @string {+ @qualid } @@ -57,14 +57,14 @@ produce one monolithic file or one file per |Coq| library. .. cmd:: Extraction Library @ident - Extraction of the whole |Coq| library :n:`@ident.v` to an ML module + Extraction of the whole Coq library :n:`@ident.v` to an ML module :n:`@ident.ml`. In case of name clash, identifiers are here renamed using prefixes ``coq_`` or ``Coq_`` to ensure a session-independent renaming. .. cmd:: Recursive Extraction Library @ident - Extraction of the |Coq| library :n:`@ident.v` and all other modules + Extraction of the Coq library :n:`@ident.v` and all other modules :n:`@ident.v` depends on. .. cmd:: Separate Extraction {+ @qualid } @@ -72,26 +72,26 @@ produce one monolithic file or one file per |Coq| library. Recursive extraction of all the mentioned objects and all their dependencies, just as :n:`Extraction @string {+ @qualid }`, but instead of producing one monolithic file, this command splits - the produced code in separate ML files, one per corresponding |Coq| + the produced code in separate ML files, one per corresponding Coq ``.v`` file. This command is hence quite similar to :cmd:`Recursive Extraction Library`, except that only the needed - parts of |Coq| libraries are extracted instead of the whole. + parts of Coq libraries are extracted instead of the whole. The naming convention in case of name clash is the same one as :cmd:`Extraction Library`: identifiers are here renamed using prefixes ``coq_`` or ``Coq_``. The following command is meant to help automatic testing of the extraction, see for instance the ``test-suite`` directory -in the |Coq| sources. +in the Coq sources. .. cmd:: Extraction TestCompile {+ @qualid } All the mentioned objects and all their dependencies are extracted - to a temporary |OCaml| file, just as in ``Extraction "file"``. Then + to a temporary OCaml file, just as in ``Extraction "file"``. Then this temporary file and its signature are compiled with the same - |OCaml| compiler used to built |Coq|. This command succeeds only - if the extraction and the |OCaml| compilation succeed. It fails - if the current target language of the extraction is not |OCaml|. + OCaml compiler used to built Coq. This command succeeds only + if the extraction and the OCaml compilation succeed. It fails + if the current target language of the extraction is not OCaml. Extraction Options ------------------- @@ -120,17 +120,17 @@ Setting the target language Inlining and optimizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since |OCaml| is a strict language, the extracted code has to +Since OCaml is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -wants to generate an |OCaml| program. The optimizations can be split in two +wants to generate an OCaml program. The optimizations can be split in two groups: the type-preserving ones (essentially constant inlining and reductions) and the non type-preserving ones (some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types). Therefore some constants may not appear in the -resulting monolithic |OCaml| program. In the case of modular extraction, +resulting monolithic OCaml program. In the case of modular extraction, even if some inlining is done, the inlined constants are nevertheless printed, to ensure session-independent programs. @@ -138,7 +138,7 @@ Concerning Haskell, type-preserving optimizations are less useful because of laziness. We still make some optimizations, for example in order to produce more readable code. -The type-preserving optimizations are controlled by the following |Coq| flags +The type-preserving optimizations are controlled by the following Coq flags and commands: .. flag:: Extraction Optimize @@ -146,7 +146,7 @@ and commands: Default is on. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Turn this flag off if you want a - ML term as close as possible to the |Coq| term. + ML term as close as possible to the Coq term. .. flag:: Extraction Conservative Types @@ -199,7 +199,7 @@ The user can explicitly ask for a constant to be extracted by two means: * by mentioning it on the extraction command line - * by extracting the whole |Coq| module of this constant. + * by extracting the whole Coq module of this constant. In both cases, the declaration of this constant will be present in the produced file. But this same constant may or may not be inlined in @@ -321,7 +321,7 @@ Realizing inductive types The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML -native boolean type instead of the |Coq| one. The syntax is the following: +native boolean type instead of the Coq one. The syntax is the following: .. cmd:: Extract Inductive @qualid => {| @ident | @string } [ {* {| @ident | @string } } ] {? @string__match } @@ -350,7 +350,7 @@ native boolean type instead of the |Coq| one. The syntax is the following: arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional form ``(fun () -> bar)``. For instance, when extracting :g:`nat` - into |OCaml| ``int``, the code to be provided has type: + into OCaml ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. .. caution:: As for :cmd:`Extract Constant`, this command should be used with care: @@ -361,15 +361,15 @@ native boolean type instead of the |Coq| one. The syntax is the following: * Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern matching) will often **not** be fully rigorously - correct. For instance, when extracting ``nat`` to |OCaml| ``int``, + correct. For instance, when extracting ``nat`` to OCaml ``int``, it is theoretically possible to build ``nat`` values that are - larger than |OCaml| ``max_int``. It is the user's responsibility to + larger than OCaml ``max_int``. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. * Translating an inductive type to an arbitrary ML type does **not** magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting - ``nat`` to |OCaml| ``int``, the function ``Nat.mul`` stays quadratic. + ``nat`` to OCaml ``int``, the function ``Nat.mul`` stays quadratic. It might be interesting to associate this translation with some specific :cmd:`Extract Constant` when primitive counterparts exist. @@ -383,9 +383,9 @@ Typical examples are the following: .. note:: - When extracting to |OCaml|, if an inductive constructor or type has arity 2 and + When extracting to OCaml, if an inductive constructor or type has arity 2 and the corresponding string is enclosed by parentheses, and the string meets - |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is + OCaml's lexical criteria for an infix symbol, then the rest of the string is used as an infix constructor or type. .. coqtop:: in @@ -394,7 +394,7 @@ Typical examples are the following: Extract Inductive prod => "(*)" [ "(,)" ]. As an example of translation to a non-inductive datatype, let's turn -``nat`` into |OCaml| ``int`` (see caveat above): +``nat`` into OCaml ``int`` (see caveat above): .. coqtop:: in @@ -404,11 +404,11 @@ Avoiding conflicts with existing filenames ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When using :cmd:`Extraction Library`, the names of the extracted files -directly depend on the names of the |Coq| files. It may happen that +directly depend on the names of the Coq files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module ``List`` exists both in |Coq| and in |OCaml|. +For instance the module ``List`` exists both in Coq and in OCaml. It is possible to instruct the extraction not to use particular filenames. .. cmd:: Extraction Blacklist {+ @ident } @@ -424,7 +424,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. -For |OCaml|, a typical use of these commands is +For OCaml, a typical use of these commands is ``Extraction Blacklist String List``. Additional settings @@ -440,7 +440,7 @@ Additional settings Controls which optimizations are used during extraction, providing a finer-grained control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. - Keeping an option off keeps the extracted ML more similar to the |Coq| term. + Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: +-----+-------+----------------------------------------------------------------+ @@ -471,14 +471,14 @@ Additional settings .. flag:: Extraction TypeExpand - If set, fully expand |Coq| types in ML. See the |Coq| source code to learn more. + If set, fully expand Coq types in ML. See the Coq source code to learn more. -Differences between |Coq| and ML type systems +Differences between Coq and ML type systems ---------------------------------------------- -Due to differences between |Coq| and ML type systems, +Due to differences between Coq and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in |OCaml|) by adding +We now solve this problem (at least in OCaml) by adding when needed some unsafe casting ``Obj.magic``, which give a generic type ``'a`` to any term. @@ -492,7 +492,7 @@ function: Definition dp {A B:Type}(x:A)(y:B)(f:forall C:Type, C->C) := (f A x, f B y). -In |OCaml|, for instance, the direct extracted term would be:: +In OCaml, for instance, the direct extracted term would be:: let dp x y f = Pair((f () x),(f () y)) @@ -506,7 +506,7 @@ We now produce the following correct version:: let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) -Secondly, some |Coq| definitions may have no counterpart in ML. This +Secondly, some Coq definitions may have no counterpart in ML. This happens when there is a quantification over types inside the type of a constructor; for example: @@ -515,29 +515,29 @@ of a constructor; for example: Inductive anything : Type := dummy : forall A:Set, A -> anything. which corresponds to the definition of an ML dynamic type. -In |OCaml|, we must cast any argument of the constructor dummy +In OCaml, we must cast any argument of the constructor dummy (no GADT are produced yet by the extraction). Even with those unsafe castings, you should never get error like ``segmentation fault``. In fact even if your program may seem -ill-typed to the |OCaml| type checker, it can't go wrong : it comes -from a |Coq| well-typed terms, so for example inductive types will always +ill-typed to the OCaml type checker, it can't go wrong : it comes +from a Coq well-typed terms, so for example inductive types will always have the correct number of arguments, etc. Of course, when launching manually some extracted function, you should apply it to arguments -of the right shape (from the |Coq| point-of-view). +of the right shape (from the Coq point-of-view). More details about the correctness of the extracted programs can be found in :cite:`Let02`. We have to say, though, that in most "realistic" programs, these problems do not -occur. For example all the programs of |Coq| library are accepted by the |OCaml| +occur. For example all the programs of Coq library are accepted by the OCaml type checker without any ``Obj.magic`` (see examples below). Some examples ------------- We present here two examples of extraction, taken from the -|Coq| Standard Library. We choose |OCaml| as the target language, +Coq Standard Library. We choose OCaml as the target language, but everything, with slight modifications, can also be done in the other languages supported by extraction. We then indicate where to find other examples and tests of extraction. @@ -554,7 +554,7 @@ This module contains a theorem ``eucl_dev``, whose type is:: where ``diveucl`` is a type for the pair of the quotient and the modulo, plus some logical assertions that disappear during extraction. -We can now extract this program to |OCaml|: +We can now extract this program to OCaml: .. coqtop:: none @@ -570,11 +570,11 @@ We can now extract this program to |OCaml|: The inlining of ``gt_wf_rec`` and others is not mandatory. It only enhances readability of extracted code. You can then copy-paste the output to a file ``euclid.ml`` or let -|Coq| do it for you with the following command:: +Coq do it for you with the following command:: Extraction "euclid" eucl_dev. -Let us play the resulting program (in an |OCaml| toplevel):: +Let us play the resulting program (in an OCaml toplevel):: #use "euclid.ml";; type nat = O | S of nat @@ -588,7 +588,7 @@ Let us play the resulting program (in an |OCaml| toplevel):: # eucl_dev (S (S O)) (S (S (S (S (S O)))));; - : diveucl = Divex (S (S O), S O) -It is easier to test on |OCaml| integers:: +It is easier to test on OCaml integers:: # let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; val nat_of_int : int -> nat = <fun> @@ -614,12 +614,12 @@ Extraction's horror museum ~~~~~~~~~~~~~~~~~~~~~~~~~~ Some pathological examples of extraction are grouped in the file -``test-suite/success/extraction.v`` of the sources of |Coq|. +``test-suite/success/extraction.v`` of the sources of Coq. Users' Contributions ~~~~~~~~~~~~~~~~~~~~ -Several of the |Coq| Users' Contributions use extraction to produce +Several of the Coq Users' Contributions use extraction to produce certified programs. In particular the following ones have an automatic extraction test: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 407a38378f..27ae7cea3a 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -35,7 +35,7 @@ the previous implementation in several ways: the new implementation, if one provides the proper morphisms. Again, most of the work is handled in the tactics. + First-class morphisms and signatures. Signatures and morphisms are - ordinary |Coq| terms, hence they can be manipulated inside |Coq|, put + ordinary Coq terms, hence they can be manipulated inside Coq, put inside structures and lemmas about them can be proved inside the system. Higher-order morphisms are also allowed. + Performance. The implementation is based on a depth-first search for @@ -103,7 +103,7 @@ argument. Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation instance :math:`R` if it is covariant on the same argument when the inverse -relation :math:`R^{−1}` (``inverse R`` in |Coq|) is considered. The special arrow ``-->`` +relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. Functions having arguments related by symmetric relations instances @@ -144,7 +144,7 @@ always the intended equality for a given structure. In the next section we will describe the commands to register terms as parametric relations and morphisms. Several tactics that deal with -equality in |Coq| can also work with the registered relations. The exact +equality in Coq can also work with the registered relations. The exact list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R`` is an instance of a registered reflexive relation. However, the diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index b81212ad0d..0f0ccd6a20 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -8,7 +8,7 @@ Implicit Coercions General Presentation --------------------- -This section describes the inheritance mechanism of |Coq|. In |Coq| with +This section describes the inheritance mechanism of Coq. In Coq with inheritance, we are not interested in adding any expressive power to our theory, but only convenience. Given a term, possibly not typable, we are interested in the problem of determining if it can be well diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 2c7b637a42..fb9965e43a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -260,7 +260,7 @@ proof by abstracting monomials by variables. that might miss a refutation. To illustrate the working of the tactic, consider we wish to prove the - following |Coq| goal: + following Coq goal: .. needs csdp .. coqdoc:: diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 3944a34cdc..7d30cae525 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,7 +1,7 @@ Program derivation ================== -|Coq| comes with an extension called ``Derive``, which supports program +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, diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 5c08bc44df..2b10f5671d 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -9,7 +9,7 @@ Omega: a (deprecated) solver for arithmetic The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` tactic. The goal is to consolidate the arithmetic solving - capabilities of |Coq| into a single engine; moreover, :tacn:`lia` is + capabilities of Coq into a single engine; moreover, :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a complete Presburger arithmetic solver while :tacn:`omega` was known to be incomplete). @@ -143,7 +143,7 @@ Options .. deprecated:: 8.5 - This deprecated flag (on by default) is for compatibility with |Coq| pre 8.5. It + This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It resets internal name counters to make executions of :tacn:`omega` independent. .. flag:: Omega UseLocalDefs diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 7a50748c51..e824ae152d 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -6,8 +6,8 @@ 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 +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. @@ -20,13 +20,13 @@ 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 +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 +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. @@ -34,12 +34,12 @@ though doing so is not recommended. Proof annotations ---------------------- -To process a proof asynchronously |Coq| needs to know the precise +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:`section-mechanism`). -When a section ends, |Coq| looks at the proof object to decide which +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 @@ -58,7 +58,7 @@ variables used. Automatic suggestion of proof annotations ````````````````````````````````````````` -The :flag:`Suggest Proof Using` flag makes |Coq| suggest, when a ``Qed`` +The :flag:`Suggest Proof Using` flag 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. @@ -66,17 +66,17 @@ to modify the proof script accordingly. Proof blocks and error resilience -------------------------------------- -|Coq| 8.6 introduced a mechanism for error resilience: in interactive -mode |Coq| is able to completely check a document containing errors +Coq 8.6 introduced a mechanism for error resilience: 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 +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 +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` @@ -92,13 +92,13 @@ Caveats When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by the first error. Error resilience for vernacular commands can be switched off by passing ``-async-proofs-command-error-resilience off`` -to |CoqIDE|. +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 resilience can be turned off or selectively activated -for any set of block kind passing to |CoqIDE| one of the following +for any set of block kind passing to CoqIDE one of the following options: - ``-async-proofs-tactic-error-resilience off`` @@ -113,13 +113,13 @@ Interactive mode --------------------- At the time of writing the only user interface supporting asynchronous -proof processing is |CoqIDE|. +proof processing is CoqIDE. -When |CoqIDE| is started, two |Coq| processes are created. The master one +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. +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. @@ -137,14 +137,14 @@ Only then all the universe constraints are checked. Caveats ``````` -The number of worker processes can be increased by passing |CoqIDE| +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 +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 @@ -166,9 +166,9 @@ Batch mode a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is assigned higher priority than the loading of a ``.vio`` file. -When |Coq| is used as a batch compiler by running ``coqc``, it produces +When Coq is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other -things, theorem statements and proofs. Hence to produce a .vo |Coq| +things, theorem 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 @@ -224,7 +224,7 @@ 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 +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. @@ -232,9 +232,9 @@ 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 +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 respect the +After that, all Coq processes, e.g. ``coqide`` and ``coqc``, will respect the limit, globally. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 5da1ac3f46..298ea4b4ab 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -8,25 +8,25 @@ Program :Author: Matthieu Sozeau We present here the |Program| tactic commands, used to build -certified |Coq| programs, elaborating them from their algorithmic +certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification :cite:`sozeau06`. It can be thought of as a dual of :ref:`Extraction <extraction>`. The goal of |Program| is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the -specification using the whole |Coq| proof apparatus. This is done using +specification using the whole Coq proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of PVS :cite:`Rushby98`, which generates type checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a -complete |Coq| term. |Program| replaces the |Program| tactic by Catherine +complete Coq term. |Program| replaces the |Program| tactic by Catherine Parent :cite:`Parent95b` which had a similar goal but is no longer maintained. -The languages available as input are currently restricted to |Coq|’s -term language, but may be extended to |OCaml|, Haskell and -others in the future. We use the same syntax as |Coq| and permit to use +The languages available as input are currently restricted to Coq’s +term language, but may be extended to OCaml, Haskell and +others in the future. We use the same syntax as Coq and permit to use implicit arguments and the existing coercion mechanism. Input terms and types are typed in an extended system (Russell) and interpreted -into |Coq| terms. The interpretation process may produce some proof +into Coq terms. The interpretation process may produce some proof obligations which need to be resolved to create the final term. @@ -35,7 +35,7 @@ obligations which need to be resolved to create the final term. Elaborating programs -------------------- -The main difference from |Coq| is that an object in a type :g:`T : Set` can +The main difference from Coq is that an object in a type :g:`T : Set` can be considered as an object of type :g:`{x : T | P}` for any well-formed :g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property :g:`P`, we must prove that the object under consideration verifies it. Russell @@ -86,7 +86,7 @@ coercions. Controls the special treatment of pattern matching generating equalities and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm - of |Coq| (see :ref:`extendedpatternmatching`) when this flag is + of Coq (see :ref:`extendedpatternmatching`) when this flag is deactivated. .. flag:: Program Generalized Coercion @@ -116,7 +116,7 @@ Syntactic control over equalities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To give more control over the generation of equalities, the -type checker will fall back directly to |Coq|’s usual typing of dependent +type checker will fall back directly to Coq’s usual typing of dependent pattern matching if a ``return`` or ``in`` clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can @@ -161,13 +161,13 @@ Program Definition A :cmd:`Definition` command with the :attr:`program` attribute types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the -final |Coq| term to the name :n:`@ident` in the environment. +final Coq term to the name :n:`@ident` in the environment. :n:`Program Definition @ident : @type := @term` Interprets the type :n:`@type`, potentially generating proof -obligations to be resolved. Once done with them, we have a |Coq| -type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq| +obligations to be resolved. Once done with them, we have a Coq +type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a Coq term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the set of obligations generated during the interpretation of :n:`@term__0` @@ -342,7 +342,7 @@ Frequently Asked Questions .. exn:: Ill-formed recursive definition. This error can happen when one tries to define a function by structural - recursion on a subset object, which means the |Coq| function looks like: + recursion on a subset object, which means the Coq function looks like: :: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index abfffa0035..d46dea1f5d 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -99,7 +99,7 @@ Yes, building the variables map and doing the substitution after normalizing is automatically done by the tactic. So you can just forget this paragraph and use the tactic according to your intuition. -Concrete usage in |Coq| +Concrete usage in Coq -------------------------- .. tacn:: ring {? [ {+ @one_term } ] } @@ -429,10 +429,10 @@ How does it work? The code of ``ring`` is a good example of a tactic written using *reflection*. What is reflection? Basically, using it means that a part of a tactic is written -in Gallina, |Coq|'s language of terms, rather than |Ltac| or |OCaml|. From the +in Gallina, Coq's language of terms, rather than |Ltac| or OCaml. From the philosophical point of view, reflection is using the ability of the Calculus of Constructions to speak and reason about itself. For the ``ring`` tactic we used -|Coq| as a programming language and also as a proof environment to build a tactic +Coq as a programming language and also as a proof environment to build a tactic and to prove its correctness. The interested reader is strongly advised to have a look at the @@ -491,7 +491,7 @@ its correctness w.r.t interpretation, that is: So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little -piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an +piece of ML code guesses the type of `p`, the ring theory `T` to use, an abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|- equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`, using the main correctness theorem and we reduce it to a @@ -677,7 +677,7 @@ History of ring First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big -for |Coq|’s type checker. Let us see why: +for Coq’s type checker. Let us see why: .. coqtop:: all @@ -697,7 +697,7 @@ was rewritten by Patrick Loiseleur: the new tactic does not any more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote -some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. +some ML code for the ``Add Ring`` command that allows registering new rings dynamically. Proofs terms generated by ring are quite small, they are linear in the number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking @@ -740,12 +740,12 @@ tactics using reflection. Another idea suggested by Benjamin Werner: reflection could be used to couple an external tool (a rewriting program or a model checker) -with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and +with Coq. We define (in Coq) a type of terms, a type of *traces*, and prove a correctness theorem that states that *replaying traces* is safe with respect to some interpretation. Then we let the external tool do every computation (using side-effects, backtracking, exception, or others features that are not available in pure lambda calculus) to produce -the trace. Now we can check in |Coq| that the trace has the expected +the trace. Now we can check in Coq that the trace has the expected semantics by applying the correctness theorem. diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 6c62ff3116..2b1f343e14 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -10,13 +10,13 @@ SProp (proof irrelevant propositions) In particular, conversion checking through bytecode or native code compilation currently does not understand proof irrelevance. -This section describes the extension of |Coq| with definitionally +This section describes the extension of Coq with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also known as strict propositions) as described in :cite:`Gilbert:POPL2019`. Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the -|Coq| program or by turning the :flag:`Allow StrictProp` flag off. +Coq program or by turning the :flag:`Allow StrictProp` flag off. .. flag:: Allow StrictProp :name: Allow StrictProp diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7638fce010..cdd31fcb86 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -13,7 +13,7 @@ Class and Instance declarations ------------------------------- The syntax for class and instance declarations is the same as the record -syntax of |Coq|: +syntax of Coq: .. coqdoc:: @@ -61,7 +61,7 @@ Note that if you finish the proof with :cmd:`Qed` the entire instance will be opaque, including the fields given in the initial term. Alternatively, in :flag:`Program Mode` if one does not give all the -members in the Instance declaration, |Coq| generates obligations for the +members in the Instance declaration, Coq generates obligations for the remaining fields, e.g.: .. coqtop:: in @@ -242,7 +242,7 @@ binders. For example: Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). The ``!`` modifier switches the way a binder is parsed back to the usual -interpretation of |Coq|. In particular, it uses the implicit arguments +interpretation of Coq. In particular, it uses the implicit arguments mechanism if available, as shown in the example. Substructures @@ -513,7 +513,7 @@ Settings This flag (off by default) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before - the dependent ones previously (|Coq| 8.5 and below). This can result in + the dependent ones previously (Coq 8.5 and below). This can result in quite different performance behaviors of proof search. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index dd26534ec7..1fb337b30a 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -12,7 +12,7 @@ General Presentation The status of Universe Polymorphism is experimental. -This section describes the universe polymorphic extension of |Coq|. +This section describes the universe polymorphic extension of Coq. Universe polymorphism makes it possible to write generic definitions making use of universes and reuse them at different and sometimes incompatible universe levels. @@ -231,7 +231,7 @@ constraints by prefixing the level names with symbols. Because inductive subtypings are only produced by comparing inductives to themselves with universes changed, they amount to variance information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in |Coq|), +irrelevant (there are no contravariant subtypings in Coq), respectively represented by the symbols `=`, `+` and `*`. Here we see that :g:`list` binds an irrelevant universe, so any two @@ -474,7 +474,7 @@ mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one can use :cmd:`Show Universes` to display the current context of universes. -It is possible to provide only some universe levels and let |Coq| infer the others +It is possible to provide only some universe levels and let Coq infer the others by adding a :g:`+` in the list of bound universe levels: .. coqtop:: all diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst index b00a7cdb08..50ffec8e3f 100644 --- a/doc/sphinx/appendix/history-and-changes/index.rst +++ b/doc/sphinx/appendix/history-and-changes/index.rst @@ -5,10 +5,10 @@ History and recent changes ========================== This chapter is divided in two parts. The first one is about the -:ref:`early history of |Coq| <history>` and is presented in +:ref:`early history of Coq <history>` and is presented in chronological order. The second one provides :ref:`release notes -about recent versions of |Coq| <changes>` and is presented in reverse -chronological order. When updating your copy of |Coq| to a new version +about recent versions of Coq <changes>` and is presented in reverse +chronological order. When updating your copy of Coq to a new version (especially a new major version), it is strongly recommended that you read the corresponding release notes. They may contain advice that will help you understand the differences with the previous version and diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 79f00a4a5a..8da5014125 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -14,7 +14,7 @@ Version 8.12 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.12 integrates many usability improvements, +Coq version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. The main changes include: @@ -34,10 +34,10 @@ The main changes include: this takes precedence over the now deprecated :ref:`ssreflect search<812SSRSearch>`. - Many additions and improvements of the :ref:`standard library<812Stdlib>`. - Improvements to the :ref:`reference manual<812Refman>` include a more logical organization - of chapters along with updated syntax descriptions that match |Coq|'s grammar + of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. -Additionally, the :tacn:`omega` tactic is deprecated in this version of |Coq|, +Additionally, the :tacn:`omega` tactic is deprecated in this version of Coq, and we recommend users to switch to :tacn:`lia` in new proof scripts (see also the warning message in the :ref:`corresponding chapter <omega_chapter>`). @@ -46,7 +46,7 @@ See the `Changes in 8.12+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked with **Changed**. -|Coq|'s documentation is available at https://coq.github.io/doc/v8.12/refman (reference +Coq's documentation is available at https://coq.github.io/doc/v8.12/refman (reference manual), and https://coq.github.io/doc/v8.12/stdlib (documentation of the standard library). Developer documentation of the ML API is available at https://coq.github.io/doc/v8.12/api. @@ -55,16 +55,16 @@ Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -Erik Martin-Dorel has maintained the `|Coq| Docker images -<https://hub.docker.com/r/coqorg/coq>`_ that are used in many |Coq| +Erik Martin-Dorel has maintained the `Coq Docker images +<https://hub.docker.com/r/coqorg/coq>`_ that are used in many Coq projects for continuous integration. -The OPAM repository for |Coq| packages has been maintained by +The OPAM repository for Coq packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. -Previously, most components of |Coq| had a single principal maintainer. +Previously, most components of Coq had a single principal maintainer. This was changed in 8.12 (`#11295 <https://github.com/coq/coq/pull/11295>`_) so that every component now has a team of maintainers, who are in charge of reviewing and @@ -97,18 +97,18 @@ Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia, Nickolai Zeldovich and Théo Zimmermann. Many power users helped to improve the design of this new version via -the GitHub issue and pull request system, the |Coq| development mailing list +the GitHub issue and pull request system, the Coq development mailing list coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum -<https://coq.discourse.group/>`_ and the new `|Coq| Zulip chat <http://coq.zulipchat.com>`_ +<https://coq.discourse.group/>`_ and the new `Coq Zulip chat <http://coq.zulipchat.com>`_ (thanks to Cyril Cohen for organizing the move from Gitter). Version 8.12's development spanned 6 months from the release of -|Coq| 8.11.0. Emilio Jesus Gallego Arias and Théo Zimmermann are -the release managers of |Coq| 8.12. This release is the result of +Coq 8.11.0. Emilio Jesus Gallego Arias and Théo Zimmermann are +the release managers of Coq 8.12. This release is the result of ~500 PRs merged, closing ~100 issues. | Nantes, June 2020, -| Matthieu Sozeau for the |Coq| development team +| Matthieu Sozeau for the Coq development team | Changes in 8.12+beta1 @@ -131,7 +131,7 @@ Specification language, type inference ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - **Changed:** - The deprecation warning raised since |Coq| 8.10 when a trailing + The deprecation warning raised since Coq 8.10 when a trailing implicit is declared to be non-maximally inserted (with the command :cmd:`Arguments`) has been turned into an error (`#11368 <https://github.com/coq/coq/pull/11368>`_, @@ -432,7 +432,7 @@ Tactics fixes `#12210 <https://github.com/coq/coq/issues/12210>`_). - **Fixed:** :tacn:`zify` now handles :g:`Z.pow_pos` by default. - In |Coq| 8.11, this was the case only when loading module + In Coq 8.11, this was the case only when loading module :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. The regression is now fixed, and the module kept only for compatibility (`#11362 <https://github.com/coq/coq/pull/11362>`_, @@ -532,7 +532,7 @@ Flags, options and attributes by Emilio Jesus Gallego Arias). - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, - ``notemplate`` attributes (they were deprecated since |Coq| 8.10). + ``notemplate`` attributes (they were deprecated since Coq 8.10). Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)` and :attr:`universes(notemplate)` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). @@ -676,7 +676,7 @@ Tools involving ``%``) (`#12126 <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). - **Changed:** - When passing ``TIMED=1`` to ``make`` with either |Coq|'s own makefile + When passing ``TIMED=1`` to ``make`` with either Coq's own makefile or a ``coq_makefile``\-made makefile, timing information is now printed for OCaml files as well (`#12211 <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). @@ -701,7 +701,7 @@ Tools <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert). - **Added:** A new documentation environment ``details`` to make certain portion - of a |Coq| document foldable. See :ref:`coqdoc-hide-show` + of a Coq document foldable. See :ref:`coqdoc-hide-show` (`#10592 <https://github.com/coq/coq/pull/10592>`_, by Thomas Letan). - **Added:** @@ -726,7 +726,7 @@ Tools ``--user``) to ``make`` (`#11302 <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). - **Added:** - |Coq|'s build system now supports both ``TIMING_FUZZ``, + Coq's build system now supports both ``TIMING_FUZZ``, ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` made by ``coq_makefile`` (`#11302 <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). @@ -742,7 +742,7 @@ Tools ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make`` (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). - **Added:** - |Coq|'s build system now supports both ``TIMING_INCLUDE_MEM`` and + Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). @@ -765,7 +765,7 @@ Tools (`#12091 <https://github.com/coq/coq/pull/12091>`_, by Hugo Herbelin). - **Fixed:** - The various timing targets for |Coq|'s standard library now correctly + The various timing targets for Coq's standard library now correctly display and label the "before" and "after" columns, rather than mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason @@ -799,15 +799,15 @@ Tools <https://github.com/coq/coq/pull/12388>`_, fixes `#12387 <https://github.com/coq/coq/pull/12387>`_, by Jason Gross). -|CoqIDE| +CoqIDE ^^^^^^^^ - **Removed:** - "Tactic" menu from |CoqIDE| which had been unmaintained for a number of years + "Tactic" menu from CoqIDE which had been unmaintained for a number of years (`#11414 <https://github.com/coq/coq/pull/11414>`_, by Pierre-Marie Pédrot). - **Removed:** - "Revert all buffers" command from |CoqIDE| which had been broken for a long time + "Revert all buffers" command from CoqIDE which had been broken for a long time (`#11415 <https://github.com/coq/coq/pull/11415>`_, by Pierre-Marie Pédrot). @@ -1038,7 +1038,7 @@ Extraction - **Added:** Support for better extraction of strings in OCaml and Haskell: - `ExtOcamlNativeString` provides bindings from the |Coq| `String` type to + `ExtOcamlNativeString` provides bindings from the Coq `String` type to the OCaml `string` type, and string literals can be extracted to literals, both in OCaml and Haskell (`#10486 <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from @@ -1063,7 +1063,7 @@ Reference manual organization. In the new version, there are fewer top-level chapters, and, in the HTML format, chapters are split into smaller pages. This is still a work in progress and further restructuring - is expected in the next versions of |Coq| + is expected in the next versions of Coq (`CEP#43 <https://github.com/coq/ceps/pull/43>`_, implemented in `#11601 <https://github.com/coq/coq/pull/11601>`_, `#11871 <https://github.com/coq/coq/pull/11871>`_, @@ -1076,7 +1076,7 @@ Reference manual help and reviews of Jim Fehrle, Clément Pit-Claudel and others). - **Changed:** Most of the grammar is now presented using the notation mechanism - that has been used to present commands and tactics since |Coq| 8.8 and + that has been used to present commands and tactics since Coq 8.8 and which is documented in :ref:`syntax-conventions` (`#11183 <https://github.com/coq/coq/pull/11183>`_, `#11314 <https://github.com/coq/coq/pull/11314>`_, @@ -1198,9 +1198,9 @@ Changes in 8.12.0 fixes `#11970 <https://github.com/coq/coq/issues/11970>`_, by Pierre-Marie Pédrot). -**|CoqIDE|** +**CoqIDE** -- **Fixed:** |CoqIDE| no longer exits when trying to open a file whose name is not a valid identifier +- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier (`#12562 <https://github.com/coq/coq/pull/12562>`_, fixes `#10988 <https://github.com/coq/coq/issues/10988>`_, by Vincent Laporte). @@ -1329,7 +1329,7 @@ Version 8.11 Summary of changes ~~~~~~~~~~~~~~~~~~ -The main changes brought by |Coq| version 8.11 are: +The main changes brought by Coq version 8.11 are: - :ref:`Ltac2<811Ltac2>`, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. @@ -1357,17 +1357,17 @@ The main changes brought by |Coq| version 8.11 are: instances of the constructive and classical real numbers. Additionally, while the :tacn:`omega` tactic is not yet deprecated in -this version of |Coq|, it should soon be the case and we already +this version of Coq, it should soon be the case and we already recommend users to switch to :tacn:`lia` in new proof scripts (see also the warning message in the :ref:`corresponding chapter <omega_chapter>`). The ``dev/doc/critical-bugs`` file documents the known critical bugs -of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +of Coq and affected releases. See the `Changes in 8.11+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked with **Changed**. -|Coq|'s documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of the ML API), https://coq.github.io/doc/v8.11/refman (reference manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of the standard library). @@ -1376,7 +1376,7 @@ Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -The OPAM repository for |Coq| packages has been maintained by +The OPAM repository for Coq packages has been maintained by Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. @@ -1399,20 +1399,20 @@ Matthieu Sozeau, spanjel, Claude Stolze, Enrico Tassi, Laurent Théry, James R. Wilcox, Xia Li-yao, Théo Zimmermann Many power users helped to improve the design of the new features via -the issue and pull request system, the |Coq| development mailing list, +the issue and pull request system, the Coq development mailing list, the coq-club@inria.fr mailing list or the `Discourse forum <https://coq.discourse.group/>`_. It would be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -Version 8.11 is the sixth release of |Coq| developed on a time-based +Version 8.11 is the sixth release of Coq developed on a time-based development cycle. Its development spanned 3 months from the release of -|Coq| 8.10. Pierre-Marie Pédrot is the release manager and maintainer of this +Coq 8.10. Pierre-Marie Pédrot is the release manager and maintainer of this release, assisted by Matthieu Sozeau. This release is the result of 2000+ commits and 300+ PRs merged, closing 75+ issues. | Paris, November 2019, -| Matthieu Sozeau for the |Coq| development team +| Matthieu Sozeau for the Coq development team | @@ -1429,7 +1429,7 @@ Changes in 8.11+beta1 computation. Primitive floats are added in the language of terms, following the binary64 format of the IEEE 754 standard, and the related operations are implemented for the different reduction - engines of |Coq| by using the corresponding processor operators in + engines of Coq by using the corresponding processor operators in rounding-to-nearest-even. The properties of these operators are axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part of the library :g:`Coq.Floats.Floats`. @@ -1522,7 +1522,7 @@ Changes in 8.11+beta1 Output of the :cmd:`Print` and :cmd:`About` commands. Arguments meta-data is now displayed as the corresponding :cmd:`Arguments` command instead of the - human-targeted prose used in previous |Coq| versions. (`#10985 + human-targeted prose used in previous Coq versions. (`#10985 <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). .. _811RefineInstance: @@ -1621,7 +1621,7 @@ Changes in 8.11+beta1 - **Added:** Ltac2, a new version of the tactic language Ltac, that doesn't - preserve backward compatibility, has been integrated in the main |Coq| + preserve backward compatibility, has been integrated in the main Coq distribution. It is still experimental, but we already recommend users of advanced Ltac to start using it and report bugs or request enhancements. See its documentation in the :ref:`dedicated chapter @@ -1650,14 +1650,14 @@ Changes in 8.11+beta1 Generalize tactics :tacn:`under` and :tacn:`over` for any registered relation. More precisely, assume the given context lemma has type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The - first step performed by :tacn:`under` (since |Coq| 8.10) amounts to + first step performed by :tacn:`under` (since Coq 8.10) amounts to calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which itself relies on :tacn:`setoid_rewrite` if need be. So this step was already compatible with a double implication or setoid equality for the conclusion head symbol `R2`. But a further step consists in tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` - that is displayed as ``'Under[ f1 i ]``. In |Coq| 8.10, this second + that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second (convenience) step was only performed when `R1` was Leibniz' `eq` or `iff`. Now, it is also performed for any relation `R1` which has a ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance @@ -1719,7 +1719,7 @@ Changes in 8.11+beta1 .. warning:: This is a common source of incompatibilities in projects - migrating to |Coq| 8.11. + migrating to Coq 8.11. - **Changed:** Output generated by :flag:`Printing Dependent Evars Line` flag @@ -1750,7 +1750,7 @@ Changes in 8.11+beta1 `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 + 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). @@ -1822,7 +1822,7 @@ Changes in 8.11+beta1 **Infrastructure and dependencies** - **Changed:** - |Coq| now officially supports OCaml 4.08. + Coq now officially supports OCaml 4.08. See `INSTALL` file for details (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). @@ -1900,7 +1900,7 @@ Changes in 8.11.0 **Tactic language** - **Fixed:** - Syntax of tactic `cofix ... with ...` was broken since |Coq| 8.10 + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 (`#11241 <https://github.com/coq/coq/pull/11241>`_, by Hugo Herbelin). @@ -1933,9 +1933,9 @@ Changes in 8.11.0 fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, by Karl Palmskog). -**|CoqIDE|** +**CoqIDE** -- **Changed:** |CoqIDE| now uses the GtkSourceView native implementation +- **Changed:** CoqIDE now uses the GtkSourceView native implementation of the autocomplete mechanism (`#11400 <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). @@ -1981,7 +1981,7 @@ Changes in 8.11.1 (`#11859 <https://github.com/coq/coq/pull/11859>`_, by Pierre Roux). -**|CoqIDE|** +**CoqIDE** - **Fixed:** Compiling file paths containing spaces @@ -2039,21 +2039,21 @@ Changes in 8.11.2 (`#12070 <https://github.com/coq/coq/pull/12070>`_, by Pierre Roux). -**|CoqIDE|** +**CoqIDE** - **Changed:** - |CoqIDE| now uses native window frames by default on Windows. + CoqIDE now uses native window frames by default on Windows. The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1` (`#12060 <https://github.com/coq/coq/pull/12060>`_, fixes `#11080 <https://github.com/coq/coq/issues/11080>`_, by Attila Gáspár). - **Fixed:** - New patch presumably fixing the random |Coq| 8.11 segfault issue with |CoqIDE| completion + New patch presumably fixing the random Coq 8.11 segfault issue with CoqIDE completion (`#12068 <https://github.com/coq/coq/pull/12068>`_, by Hugo Herbelin, presumably fixing `#11943 <https://github.com/coq/coq/pull/11943>`_). - **Fixed:** - Highlighting style consistently applied to all three buffers of |CoqIDE| + Highlighting style consistently applied to all three buffers of CoqIDE (`#12106 <https://github.com/coq/coq/pull/12106>`_, by Hugo Herbelin; fixes `#11506 <https://github.com/coq/coq/pull/11506>`_). @@ -2064,7 +2064,7 @@ Version 8.10 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.10 contains two major new features: support for a native +Coq version 8.10 contains two major new features: support for a native fixed-precision integer type and a new sort :math:`\SProp` of strict propositions. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, @@ -2165,15 +2165,15 @@ reference manual. Here are the most important user-visible changes: :math:`\Type`. It used to be limited to sort `Prop` (`#7634 <https://github.com/coq/coq/pull/7634>`_, by Théo Winterhalter). -- A new registration mechanism for reference from ML code to |Coq| +- A new registration mechanism for reference from ML code to Coq constructs has been added (`#186 <https://github.com/coq/coq/pull/186>`_, by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte). -- |CoqIDE|: +- CoqIDE: - - |CoqIDE| now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2. - The INSTALL file available in the |Coq| sources has been updated to list + - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2. + The INSTALL file available in the Coq sources has been updated to list the new dependencies (`#9279 <https://github.com/coq/coq/pull/9279>`_, by Hugo Herbelin, with help from Jacques Garrigue, @@ -2188,15 +2188,15 @@ reference manual. Here are the most important user-visible changes: - Infrastructure and dependencies: - - |Coq| 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the + - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the `INSTALL` file for more information on dependencies (`#7522 <https://github.com/coq/coq/pull/7522>`_, by Emilio Jesús Gallego Arías). - - |Coq| 8.10 doesn't need Camlp5 to build anymore. It now includes a - fork of the core parsing library that |Coq| uses, which is a small + - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a + fork of the core parsing library that Coq uses, which is a small subset of the whole Camlp5 distribution. In particular, this subset doesn't depend on the OCaml AST, allowing easier compilation and - testing on experimental OCaml versions. |Coq| also ships a new parser + testing on experimental OCaml versions. Coq also ships a new parser `coqpp` that plugin authors must switch to (`#7902 <https://github.com/coq/coq/pull/7902>`_, `#7979 <https://github.com/coq/coq/pull/7979>`_, @@ -2205,19 +2205,19 @@ reference manual. Here are the most important user-visible changes: and `#8945 <https://github.com/coq/coq/pull/8945>`_, by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias). - The |Coq| developers would like to thank Daniel de Rauglaudre for many + The Coq developers would like to thank Daniel de Rauglaudre for many years of continued support. - - |Coq| now supports building with Dune, in addition to the traditional + - Coq now supports building with Dune, in addition to the traditional Makefile which is scheduled for deprecation (`#6857 <https://github.com/coq/coq/pull/6857>`_, by Emilio Jesús Gallego Arias, with help from Rudi Grinberg). - Experimental support for building |Coq| projects has been integrated + Experimental support for building Coq projects has been integrated in Dune at the same time, providing an `improved experience <https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/>`_ for plugin developers. We thank the Dune team for their work - supporting |Coq|. + supporting Coq. Version 8.10 also comes with a bunch of smaller-scale changes and improvements regarding the different components of the system, including @@ -2228,7 +2228,7 @@ the numerous changes to the implementation and improvements of interfaces. The file provides guidelines on porting a plugin to the new version and a plugin development tutorial originally made by Yves Bertot is now in `doc/plugin_tutorial`. The ``dev/doc/critical-bugs`` file -documents the known critical bugs of |Coq| and affected releases. +documents the known critical bugs of Coq and affected releases. The efficiency of the whole system has seen improvements thanks to contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès. @@ -2236,16 +2236,16 @@ contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès. Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop, Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -|Coq| is now continuously tested against the |OCaml| trunk, in addition to the +Coq is now continuously tested against the OCaml trunk, in addition to the oldest supported and latest OCaml releases. -|Coq|'s documentation for the development branch is now deployed +Coq's documentation for the development branch is now deployed continuously at https://coq.github.io/doc/master/api (documentation of the ML API), https://coq.github.io/doc/master/refman (reference manual), and https://coq.github.io/doc/master/stdlib (documentation of the standard library). Similar links exist for the `v8.10` branch. -The OPAM repository for |Coq| packages has been maintained by Guillaume +The OPAM repository for Coq packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. @@ -2267,19 +2267,19 @@ Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter, Xia Li-yao, Beta Ziliani and Théo Zimmermann. Many power users helped to improve the design of the new features via -the issue and pull request system, the |Coq| development mailing list, +the issue and pull request system, the Coq development mailing list, the coq-club@inria.fr mailing list or the new Discourse forum. It would be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -Version 8.10 is the fifth release of |Coq| developed on a time-based +Version 8.10 is the fifth release of Coq developed on a time-based development cycle. Its development spanned 6 months from the release of -|Coq| 8.9. Vincent Laporte is the release manager and maintainer of this +Coq 8.9. Vincent Laporte is the release manager and maintainer of this release. This release is the result of ~2500 commits and ~650 PRs merged, closing 150+ issues. | Santiago de Chile, April 2019, -| Matthieu Sozeau for the |Coq| development team +| Matthieu Sozeau for the Coq development team | Other changes in 8.10+beta1 @@ -2298,13 +2298,13 @@ Other changes in 8.10+beta1 (*à la* ``-top``) based on the filename passed, taking into account the proper ``-R``/``-Q`` options. For example, given ``-R Foo foolib`` using ``-topfile foolib/bar.v`` will set the module name to ``Foo.Bar``. - |CoqIDE| now properly sets the module name for a given file based on + CoqIDE now properly sets the module name for a given file based on its path (`#8991 <https://github.com/coq/coq/pull/8991>`_, closes `#8989 <https://github.com/coq/coq/issues/8989>`_, by Gaëtan Gilbert). - - Experimental: |Coq| flags and options can now be set on the + - Experimental: Coq flags and options can now be set on the command-line, e.g. ``-set "Universe Polymorphism=true"`` (`#9876 <https://github.com/coq/coq/pull/9876>`_, by Gaëtan Gilbert). @@ -2402,7 +2402,7 @@ Other changes in 8.10+beta1 - Deprecated compatibility notations have actually been removed. Uses of these notations are generally easy to fix thanks - to the hint contained in the deprecation warning emitted by |Coq| + to the hint contained in the deprecation warning emitted by Coq 8.8 and 8.9. For projects that require more than a handful of such fixes, there is `a script <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_ @@ -2417,7 +2417,7 @@ Other changes in 8.10+beta1 - The `quote plugin <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_ was removed. If some users are interested in maintaining this plugin - externally, the |Coq| development team can provide assistance for + externally, the Coq development team can provide assistance for extracting the plugin and setting up a new repository (`#7894 <https://github.com/coq/coq/pull/7894>`_, by Maxime Dénès). @@ -2644,7 +2644,7 @@ Other changes in 8.10+beta1 - Changelog has been moved from a specific file `CHANGES.md` to the reference manual; former Credits chapter of the reference manual has been split in two parts: a History chapter which was enriched with - additional historical information about |Coq| versions 1 to 5, and a + additional historical information about Coq versions 1 to 5, and a Changes chapter which was enriched with the content formerly in `CHANGES.md` and `COMPATIBILITY` (`#9133 <https://github.com/coq/coq/pull/9133>`_, @@ -2687,15 +2687,15 @@ Many bug fixes and documentation improvements, in particular: fixes `#9336 <https://github.com/coq/coq/issues/9336>`_, by Andreas Lynge, review by Enrico Tassi) -**|CoqIDE|** +**CoqIDE** -- Fix |CoqIDE| instability on Windows after the update to gtk3 +- Fix CoqIDE instability on Windows after the update to gtk3 (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop, closes `#9885 <https://github.com/coq/coq/issues/9885>`_). **Miscellaneous** -- Proof General can now display |Coq|-generated diffs between proof steps +- Proof General can now display Coq-generated diffs between proof steps in color (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, @@ -2803,7 +2803,7 @@ A few bug fixes and documentation improvements, in particular: fixes `#10894 <https://github.com/coq/coq/issues/10894>`_, by Hugo Herbelin). -**|CoqIDE|** +**CoqIDE** - Fix handling of unicode input before space (`#10852 <https://github.com/coq/coq/pull/10852>`_, @@ -2843,9 +2843,9 @@ Changes in 8.10.2 (`#11090 <https://github.com/coq/coq/pull/11090>`_, fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). -**|CoqIDE|** +**CoqIDE** -- Fixed uneven dimensions of |CoqIDE| panels when window has been resized +- Fixed uneven dimensions of CoqIDE panels when window has been resized (`#11070 <https://github.com/coq/coq/pull/11070>`_, fixes 8.10-regression `#10956 <https://github.com/coq/coq/issues/10956>`_, by Guillaume Melquiond). @@ -2868,7 +2868,7 @@ Version 8.9 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.9 contains the result of refinements and stabilization +Coq version 8.9 contains the result of refinements and stabilization of features and deprecations or removals of deprecated features, cleanups of the internals of the system and API along with a few new features. This release includes many user-visible changes, including @@ -2886,7 +2886,7 @@ changes: manual). - Deprecated notations of the standard library will be removed in the - next version of |Coq|, see the next subsection for a script to + next version of Coq, see the next subsection for a script to ease porting, by Jason Gross and Jean-Christophe Léchenet. - Added the :cmd:`Number Notation` command for registering decimal @@ -2949,7 +2949,7 @@ changes: - Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode. -- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many +- Packaging: as in Coq 8.8.2, the Windows installer now includes many more external packages that can be individually selected for installation, by Michael Soegtrop. @@ -2960,10 +2960,10 @@ important ones are documented in the next subsection file. On the implementation side, the ``dev/doc/changes.md`` file documents the numerous changes to the implementation and improvements of interfaces. The file provides guidelines on porting a plugin to the new -version and a plugin development tutorial kept in sync with |Coq| was +version and a plugin development tutorial kept in sync with Coq was introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials. The new ``dev/doc/critical-bugs`` file documents the known critical bugs -of |Coq| and affected releases. +of Coq and affected releases. The efficiency of the whole system has seen improvements thanks to contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès. @@ -2972,7 +2972,7 @@ Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael Soegtrop, Théo Zimmermann worked on maintaining and improving the continuous integration system. -The OPAM repository for |Coq| packages has been maintained by Guillaume +The OPAM repository for Coq packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. @@ -2992,23 +2992,23 @@ Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter, Zeimer, Beta Ziliani, Théo Zimmermann. Many power users helped to improve the design of the new features via -the issue and pull request system, the |Coq| development mailing list or +the issue and pull request system, the Coq development mailing list or the coq-club@inria.fr mailing list. It would be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -Version 8.9 is the fourth release of |Coq| developed on a time-based +Version 8.9 is the fourth release of Coq developed on a time-based development cycle. Its development spanned 7 months from the release of -|Coq| 8.8. The development moved to a decentralized merging process +Coq 8.8. The development moved to a decentralized merging process during this cycle. Guillaume Melquiond was in charge of the release process and is the maintainer of this release. This release is the result of ~2,000 commits and ~500 PRs merged, closing 75+ issues. -The |Coq| development team welcomed Vincent Laporte, a new |Coq| -engineer working with Maxime Dénès in the |Coq| consortium. +The Coq development team welcomed Vincent Laporte, a new Coq +engineer working with Maxime Dénès in the Coq consortium. | Paris, November 2018, -| Matthieu Sozeau for the |Coq| development team +| Matthieu Sozeau for the Coq development team | Details of changes in 8.9+beta1 @@ -3024,7 +3024,7 @@ Notations entries" (see chapter "Syntax extensions" of the reference manual). - Deprecated compatibility notations will actually be removed in the - next version of |Coq|. Uses of these notations are generally easy to + next version of Coq. Uses of these notations are generally easy to fix thanks to the hint contained in the deprecation warnings. For projects that require more than a handful of such fixes, there is `a script @@ -3125,7 +3125,7 @@ Standard Library - Numeral syntax for `nat` is no longer available without loading the entire prelude (`Require Import Coq.Init.Prelude`). This only - impacts users running |Coq| without the init library (`-nois` or + impacts users running Coq without the init library (`-nois` or `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. Tools @@ -3135,10 +3135,10 @@ Tools `COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles `$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`. -- Removed the `gallina` utility (extracts specification from |Coq| vernacular files). +- Removed the `gallina` utility (extracts specification from Coq vernacular files). If you would like to maintain this tool externally, please contact us. -- Removed the Emacs modes distributed with |Coq|. You are advised to +- Removed the Emacs modes distributed with Coq. You are advised to use `Proof-General <https://proofgeneral.github.io/>`_ (and optionally `Company-Coq <https://github.com/cpitclaudel/company-coq>`_) instead. If your use case is not covered by these alternative Emacs modes, @@ -3167,15 +3167,15 @@ Vernacular Commands NoTCResolution`. - Multiple sections with the same name are allowed. -|Coq| binaries and process model +Coq binaries and process model -- Before 8.9, |Coq| distributed a single `coqtop` binary and a set of +- Before 8.9, Coq distributed a single `coqtop` binary and a set of dynamically loadable plugins that used to take over the main loop for tasks such as IDE language server or parallel proof checking. These plugins have been turned into full-fledged binaries so each different process has associated a particular binary now, in - particular `coqidetop` is the |CoqIDE| language server, and + particular `coqidetop` is the CoqIDE language server, and `coq{proof,tactic,query}worker` are in charge of task-specific and parallel proof checking. @@ -3233,7 +3233,7 @@ Changes in 8.8.1 - Some quality-of-life fixes. - Numerous improvements to the documentation. - Fix a critical bug related to primitive projections and :tacn:`native_compute`. -- Ship several additional |Coq| libraries with the Windows installer. +- Ship several additional Coq libraries with the Windows installer. Version 8.8 ----------- @@ -3241,7 +3241,7 @@ Version 8.8 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.8 contains the result of refinements and stabilization of +Coq version 8.8 contains the result of refinements and stabilization of features and deprecations, cleanups of the internals of the system along with a few new features. The main user visible changes are: @@ -3303,12 +3303,12 @@ contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and Matthieu Sozeau and performance issue tracking by Jason Gross and Paul Steckler. -The official wiki and the bugtracker of |Coq| migrated to the GitHub +The official wiki and the bugtracker of Coq migrated to the GitHub platform, thanks to the work of Pierre Letouzey and Théo Zimmermann. Gaëtan Gilbert, Emilio Jesús Gallego Arias worked on maintaining and improving the continuous integration system. -The OPAM repository for |Coq| packages has been maintained by Guillaume +The OPAM repository for Coq packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. @@ -3323,26 +3323,26 @@ Clément Pit-Claudel, Matthew Ryan, Matt Quinn, Sigurd Schneider, Bernhard Schommer, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Anton Trunov, Martin Vassor, Vadim Zaliva and Théo Zimmermann. -Version 8.8 is the third release of |Coq| developed on a time-based +Version 8.8 is the third release of Coq developed on a time-based development cycle. Its development spanned 6 months from the release of -|Coq| 8.7 and was based on a public roadmap. The development process +Coq 8.7 and was based on a public roadmap. The development process was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the release process. Théo Zimmermann is the maintainer of this release. Many power users helped to improve the design of the new features via -the bug tracker, the pull request system, the |Coq| development mailing +the bug tracker, the pull request system, the Coq development mailing list or the coq-club@inria.fr mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Jason Gross, Ralf Jung, Robbert Krebbers and Amin Timany. It would however be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -The |Coq| consortium, an organization directed towards users and +The Coq consortium, an organization directed towards users and supporters of the system, is now running and employs Maxime Dénès. -The contacts of the |Coq| Consortium are Yves Bertot and Maxime Dénès. +The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Santiago de Chile, March 2018, -| Matthieu Sozeau for the |Coq| development team +| Matthieu Sozeau for the Coq development team | Details of changes in 8.8+beta1 @@ -3461,7 +3461,7 @@ Universes Tools -- |Coq| can now be run with the option -mangle-names to change the auto-generated +- Coq can now be run with the option -mangle-names to change the auto-generated name scheme. This is intended to function as a linter for developments that want to be robust to changes in auto-generated names. This feature is experimental, and may change or disappear without warning. @@ -3471,7 +3471,7 @@ Checker - The checker now accepts filenames in addition to logical paths. -|CoqIDE| +CoqIDE - Find and Replace All report the number of occurrences found; Find indicates when it wraps. @@ -3484,7 +3484,7 @@ coqdep Documentation -- The |Coq| FAQ, formerly located at https://coq.inria.fr/faq, has been +- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been moved to the GitHub wiki section of this repository; the main entry page is https://github.com/coq/coq/wiki/The-Coq-FAQ. - Documentation: a large community effort resulted in the migration @@ -3534,7 +3534,7 @@ Details of changes in 8.8.0 Tools - Asynchronous proof delegation policy was fixed. Since version 8.7 - |Coq| was ignoring previous runs and the `-async-proofs-delegation-threshold` + Coq was ignoring previous runs and the `-async-proofs-delegation-threshold` option did not have the expected behavior. Tactic language @@ -3608,7 +3608,7 @@ Version 8.7 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.7 contains the result of refinements, stabilization of features +Coq version 8.7 contains the result of refinements, stabilization of features and cleanups of the internals of the system along with a few new features. The main user visible changes are: @@ -3627,7 +3627,7 @@ main user visible changes are: and the extensibility of generated Makefiles, and to make ``_CoqProject`` files more palatable to IDEs by Enrico Tassi. -|Coq| 8.7 involved a large amount of work on cleaning and speeding up the code +Coq 8.7 involved a large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust. The ``dev/doc/changes.txt`` file @@ -3647,7 +3647,7 @@ Thomas Sibut-Pinote and Hugo Herbelin added support for side effect hooks in cbv, cbn and simpl. The side effects are provided via a plugin available at https://github.com/herbelin/reduction-effects/. -The BigN, BigZ, BigQ libraries are no longer part of the |Coq| standard library, +The BigN, BigZ, BigQ libraries are no longer part of the Coq standard library, they are now provided by a separate repository https://github.com/coq/bignums, maintained by Pierre Letouzey. @@ -3661,7 +3661,7 @@ others, documented in the next subsection file. The mathematical proof language/declarative mode plugin was removed from the archive. -The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, +The OPAM repository for Coq packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. @@ -3686,29 +3686,29 @@ Maxime Dénès, who was also in charge of the release process. Théo Zimmermann the maintainer of this release. Many power users helped to improve the design of the new features via the bug -tracker, the pull request system, the |Coq| development mailing list or the +tracker, the pull request system, the Coq development mailing list or the Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy, Clément Pit–Claudel and Gabriel Scherer. It would however be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -Version 8.7 is the second release of |Coq| developed on a time-based development -cycle. Its development spanned 9 months from the release of |Coq| 8.6 and was +Version 8.7 is the second release of Coq developed on a time-based development +cycle. Its development spanned 9 months from the release of Coq 8.6 and was based on a public road-map. It attracted many external contributions. Code reviews and continuous integration testing were systematically used before integration of new features, with an important focus given to compatibility and -performance issues, resulting in a hopefully more robust release than |Coq| 8.6 +performance issues, resulting in a hopefully more robust release than Coq 8.6 while maintaining compatibility. -|Coq| Enhancement Proposals (CEPs for short) and open pull request discussions +Coq Enhancement Proposals (CEPs for short) and open pull request discussions were used to discuss publicly the new features. -The |Coq| consortium, an organization directed towards users and supporters of the +The Coq consortium, an organization directed towards users and supporters of the system, is now upcoming and will rely on Inria’s newly created Foundation. | Paris, August 2017, -| Matthieu Sozeau and the |Coq| development team +| Matthieu Sozeau and the Coq development team | Potential compatibility issues @@ -3807,7 +3807,7 @@ Vernacular Commands - Possibility to unset the printing of notations in a more fine grained fashion than `Unset Printing Notations` is provided without any user-syntax. The goal is that someone creates a plugin to experiment - such a user-syntax, to be later integrated in |Coq| when stabilized. + such a user-syntax, to be later integrated in Coq when stabilized. - `About` now tells if a reference is a coercion. - The deprecated `Save` vernacular and its form `Save Theorem id` to close proofs have been removed from the syntax. Please use `Qed`. @@ -3825,7 +3825,7 @@ Standard Library - New lemmas about iff and about orders on positive and Z. - New lemmas on powerRZ. - Strengthened statement of JMeq_eq_dep (closes bug #4912). -- The BigN, BigZ, BigZ libraries are no longer part of the |Coq| standard +- The BigN, BigZ, BigZ libraries are no longer part of the Coq standard library, they are now provided by a separate repository https://github.com/coq/bignums The split has been done just after the Int31 library. @@ -3839,12 +3839,12 @@ Standard Library Plugins -- The Ssreflect plugin is now distributed with |Coq|. Its documentation has +- The Ssreflect plugin is now distributed with Coq. Its documentation has been integrated as a chapter of the reference manual. This chapter is work in progress so feedback is welcome. - The mathematical proof language (also known as declarative mode) was removed. - A new command Extraction TestCompile has been introduced, not meant - for the general user but instead for |Coq|'s test-suite. + for the general user but instead for Coq's test-suite. - The extraction plugin is no longer loaded by default. It must be explicitly loaded with [Require Extraction], which is backwards compatible. @@ -3863,7 +3863,7 @@ Tools the extensibility of generated Makefiles, and to make _CoqProject files more palatable to IDEs. Overview: - * _CoqProject files contain only |Coq| specific data (i.e. the list of + * _CoqProject files contain only Coq specific data (i.e. the list of files, -R options, ...) * coq_makefile translates _CoqProject to Makefile.conf and copies in the desired location a standard Makefile (that reads Makefile.conf) @@ -3921,15 +3921,15 @@ Details of changes in 8.7+beta2 Tools -- In |CoqIDE|, the "Compile Buffer" command takes account of flags in +- In CoqIDE, the "Compile Buffer" command takes account of flags in _CoqProject or other project file. Improvements around some error messages. Many bug fixes including two important ones: -- Bug #5730: |CoqIDE| becomes unresponsive on file open. -- coq_makefile: make sure compile flags for |Coq| and coq_makefile are in sync +- Bug #5730: CoqIDE becomes unresponsive on file open. +- coq_makefile: make sure compile flags for Coq and coq_makefile are in sync (in particular, make sure the `-safe-string` option is used to compile plugins). Details of changes in 8.7.0 @@ -3940,7 +3940,7 @@ OCaml - Users can pass specific flags to the OCaml optimizing compiler by -using the flambda-opts configure-time option. - Beware that compiling |Coq| with a flambda-enabled compiler is + Beware that compiling Coq with a flambda-enabled compiler is experimental and may require large amounts of RAM and CPU, see INSTALL for more details. @@ -3970,7 +3970,7 @@ Version 8.6 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.6 contains the result of refinements, stabilization of +Coq version 8.6 contains the result of refinements, stabilization of 8.5’s features and cleanups of the internals of the system. Over the year of (now time-based) development, about 450 bugs were resolved and over 100 contributions integrated. The main user visible changes are: @@ -3978,9 +3978,9 @@ over 100 contributions integrated. The main user visible changes are: - A new, faster state-of-the-art universe constraint checker, by Jacques-Henri Jourdan. -- In |CoqIDE| and other asynchronous interfaces, more fine-grained +- In CoqIDE and other asynchronous interfaces, more fine-grained asynchronous processing and error reporting by Enrico Tassi, making - |Coq| capable of recovering from errors and continue processing the + Coq capable of recovering from errors and continue processing the document. - More access to the proof engine features from Ltac: goal management @@ -4004,7 +4004,7 @@ over 100 contributions integrated. The main user visible changes are: - Integration of LtacProf, a profiler for Ltac by Jason Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi. -|Coq| 8.6 also comes with a bunch of smaller-scale changes and +Coq 8.6 also comes with a bunch of smaller-scale changes and improvements regarding the different components of the system. We shall only list a few of them. @@ -4027,7 +4027,7 @@ Matthieu Sozeau. The minimization algorithm has been improved by Matthieu Sozeau. The unifier has been improved by Hugo Herbelin and Matthieu Sozeau, -fixing some incompatibilities introduced in |Coq| 8.5. Unification +fixing some incompatibilities introduced in Coq 8.5. Unification constraints can now be left floating around and be seen by the user thanks to a new option. The Keyed Unification mode has been improved by Matthieu Sozeau. @@ -4050,19 +4050,19 @@ the pretty-printing and user interface communication components. Frédéric Besson maintained the micromega tactic. -The OPAM repository for |Coq| packages has been maintained by Guillaume +The OPAM repository for Coq packages has been maintained by Guillaume Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A list of packages is now available at https://coq.inria.fr/opam/www/. Packaging tools and software development kits were prepared by Michael Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly -built on the continuous integration server. |Coq| now comes with a META +built on the continuous integration server. Coq now comes with a META file usable with ocamlfind, contributed by Emilio Jesús Gallego Arias, Gregory Malecha, and Matthieu Sozeau. Matej Košík maintained and greatly improved the continuous integration -setup and the testing of |Coq| contributions. He also contributed many API +setup and the testing of Coq contributions. He also contributed many API improvements and code cleanups throughout the system. The contributors for this version are Bruno Barras, C.J. Bell, Yves @@ -4079,7 +4079,7 @@ coordinated by Hugo Herbelin and Matthieu Sozeau with the help of Maxime Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via -the bug tracker, the pull request system, the |Coq| development mailing +the bug tracker, the pull request system, the Coq development mailing list or the Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan @@ -4088,23 +4088,23 @@ Scherer and Beta Ziliani. It would however be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -Version 8.6 is the first release of |Coq| developed on a time-based +Version 8.6 is the first release of Coq developed on a time-based development cycle. Its development spanned 10 months from the release of -|Coq| 8.5 and was based on a public roadmap. To date, it contains more -external contributions than any previous |Coq| system. Code reviews were +Coq 8.5 and was based on a public roadmap. To date, it contains more +external contributions than any previous Coq system. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues, resulting -in a hopefully more robust release than |Coq| 8.5. +in a hopefully more robust release than Coq 8.5. -|Coq| Enhancement Proposals (CEPs for short) were introduced by Enrico +Coq Enhancement Proposals (CEPs for short) were introduced by Enrico Tassi to provide more visibility and a discussion period on new features, they are publicly available https://github.com/coq/ceps. Started during this period, an effort is led by Yves Bertot and Maxime -Dénès to put together a |Coq| consortium. +Dénès to put together a Coq consortium. | Paris, November 2016, -| Matthieu Sozeau and the |Coq| development team +| Matthieu Sozeau and the Coq development team | Potential sources of incompatibilities @@ -4241,13 +4241,13 @@ General infrastructure - New configurable warning system which can be controlled with the vernacular command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In particular, the default is now that warnings are printed by coqc. -- In asynchronous mode, |Coq| is now capable of recovering from errors and +- In asynchronous mode, Coq is now capable of recovering from errors and continue processing the document. Tools - coqc accepts a -o option to specify the output file name -- coqtop accepts --print-version to print |Coq| and |OCaml| versions in +- coqtop accepts --print-version to print Coq and OCaml versions in easy to parse format - Setting [Printing Dependent Evars Line] can be unset to disable the computation associated with printing the "dependent evars: " line in @@ -4276,7 +4276,7 @@ Other bug fixes in universes, type class shelving,... Details of changes in 8.6.1 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- Fix #5380: Default colors for |CoqIDE| are actually applied. +- Fix #5380: Default colors for CoqIDE are actually applied. - Fix plugin warnings - Document named evars (including Show ident) - Fix Bug #5574, document function scope @@ -4328,7 +4328,7 @@ Version 8.5 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.5 contains the result of five specific long-term projects: +Coq version 8.5 contains the result of five specific long-term projects: - A new asynchronous evaluation and compilation mode by Enrico Tassi with help from Bruno Barras and Carst Tankink. @@ -4359,7 +4359,7 @@ the backtracking behavior of tactics. Multiple goal handling paves the way for smarter automation tactics. It is currently used for simple goal manipulation such as goal reordering. -The way |Coq| processes a document in batch and interactive mode has been +The way Coq processes a document in batch and interactive mode has been redesigned by Enrico Tassi with help from Bruno Barras. Opaque proofs, the text between Proof and Qed, can be processed asynchronously, decoupling the checking of definitions and statements from the checking @@ -4372,12 +4372,12 @@ already Required. All .vio files can be turned into complete .vo files in parallel. The same infrastructure also allows terminating tactics to be run in parallel on a set of goals via the ``par:`` goal selector. -|CoqIDE| was modified to cope with asynchronous checking of the document. -Its source code was also made separate from that of |Coq|, so that |CoqIDE| +CoqIDE was modified to cope with asynchronous checking of the document. +Its source code was also made separate from that of Coq, so that CoqIDE no longer has a special status among user interfaces, paving the way for -decoupling its release cycle from that of |Coq| in the future. +decoupling its release cycle from that of Coq in the future. -Carst Tankink developed a |Coq| back-end for user interfaces built on +Carst Tankink developed a Coq back-end for user interfaces built on Makarius Wenzel’s Prover IDE framework (PIDE), like PIDE/jEdit (with help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander Faithfull and Jesper Bengtson). The development of such features was @@ -4411,7 +4411,7 @@ principles such as propositional extensionality and univalence, thanks to Maxime Dénès and Bruno Barras. To ensure compatibility with the univalence axiom, a new flag ``-indices-matter`` has been implemented, taking into account the universe levels of indices when computing the -levels of inductive types. This supports using |Coq| as a tool to explore +levels of inductive types. This supports using Coq as a tool to explore the relations between homotopy theory and type theory. Maxime Dénès and Benjamin Grégoire developed an implementation of @@ -4419,7 +4419,7 @@ conversion test and normal form computation using the OCaml native compiler. It complements the virtual machine conversion offering much faster computation for expensive functions. -|Coq| 8.5 also comes with a bunch of many various smaller-scale changes +Coq 8.5 also comes with a bunch of many various smaller-scale changes and improvements regarding the different components of the system. We shall only list a few of them. @@ -4441,13 +4441,13 @@ Matthieu Sozeau. Error messages for unification and type inference failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and Arnaud Spiwack. -Pierre Courtieu contributed new features for using |Coq| through Proof +Pierre Courtieu contributed new features for using Coq through Proof General and for better interactive experience (bullets, Search, etc). The efficiency of the whole system has been significantly improved thanks to contributions from Pierre-Marie Pédrot. -A distribution channel for |Coq| packages using the OPAM tool has been +A distribution channel for Coq packages using the OPAM tool has been initiated by Thomas Braibant and developed by Guillaume Claret, with contributions by Enrico Tassi and feedback from Hugo Herbelin. @@ -4464,7 +4464,7 @@ Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson, Lionel Rieg. It would however be impossible to mention with precision all names of people who to some extent influenced the development. -Version 8.5 is one of the most important releases of |Coq|. Its development +Version 8.5 is one of the most important releases of Coq. Its development spanned over about 3 years and a half with about one year of beta-testing. General maintenance during part or whole of this period has been done by Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo @@ -4476,14 +4476,14 @@ Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François Ripault, Carst Tankink. Maxime Dénès coordinated the release process. | Paris, January 2015, revised December 2015, -| Hugo Herbelin, Matthieu Sozeau and the |Coq| development team +| Hugo Herbelin, Matthieu Sozeau and the Coq development team | Potential sources of incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -List of typical changes to be done to adapt files from |Coq| 8.4 -to |Coq| 8.5 when not using compatibility option ``-compat 8.4``. +List of typical changes to be done to adapt files from Coq 8.4 +to Coq 8.5 when not using compatibility option ``-compat 8.4``. - Symptom: "The reference omega was not found in the current environment". @@ -4618,7 +4618,7 @@ Logic logic inconsistent). - The guard condition for fixpoints is now a bit stricter. Propagation of subterm value through pattern matching is restricted according to - the return predicate. Restores compatibility of |Coq|'s logic with the + the return predicate. Restores compatibility of Coq's logic with the propositional extensionality axiom. May create incompatibilities in recursive programs heavily using dependent types. - Trivial inductive types are no longer defined in Type but in Prop, which @@ -4658,7 +4658,7 @@ Vernacular commands - A new Print Strategies command allows visualizing the opacity status of the whole engine. - The "Locate" command now searches through all sorts of qualified namespaces of - |Coq|: terms, modules, tactics, etc. The old behavior of the command can be + Coq: terms, modules, tactics, etc. The old behavior of the command can be retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. - New "Refine Instance Mode" option that allows to deactivate the generation of @@ -4986,24 +4986,24 @@ Tools files from the quickly generated proofs. - The XML plugin was discontinued and removed from the source. - A new utility called coqworkmgr can be used to limit the number of - concurrent workers started by independent processes, like make and |CoqIDE|. + concurrent workers started by independent processes, like make and CoqIDE. This is of interest for users of the par: goal selector. Interfaces -- |CoqIDE| supports asynchronous edition of the document, ongoing tasks and +- CoqIDE supports asynchronous edition of the document, ongoing tasks and errors are reported in the bottom right window. The number of workers taking care of processing proofs can be selected with -async-proofs-j. -- |CoqIDE| highlights in yellow "unsafe" commands such as axiom +- CoqIDE highlights in yellow "unsafe" commands such as axiom declarations, and tactics like "give_up". -- |CoqIDE| supports Proof General like key bindings; +- CoqIDE supports Proof General like key bindings; to activate the PG mode go to Edit -> Preferences -> Editor. For the documentation see Help -> Help for PG mode. -- |CoqIDE| automatically retracts the locked area when one edits the +- CoqIDE automatically retracts the locked area when one edits the locked text. -- |CoqIDE| search and replace got regular expressions power. See the +- CoqIDE search and replace got regular expressions power. See the documentation of OCaml's Str module for the supported syntax. -- Many |CoqIDE| windows, including the query one, are now detachable to +- Many CoqIDE windows, including the query one, are now detachable to improve usability on multi screen work stations. - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks to the COQ_COLORS environment variable, and their current state can @@ -5014,7 +5014,7 @@ Interfaces Internal Infrastructure - Many reorganizations in the ocaml source files. For instance, - many internal a.s.t. of |Coq| are now placed in mli files in + many internal a.s.t. of Coq are now placed in mli files in a new directory intf/, for instance constrexpr.mli or glob_term.mli. More details in dev/doc/changes. @@ -5066,7 +5066,7 @@ Tactics Extraction - Definitions extracted to Haskell GHC should no longer randomly - segfault when some |Coq| types cannot be represented by Haskell types. + segfault when some Coq types cannot be represented by Haskell types. - Definitions can now be extracted to Json for post-processing. Tools @@ -5164,8 +5164,8 @@ Tools Standard Library - There is now a Coq.Compat.Coq84 library, which sets the various compatibility - options and does a few redefinitions to make |Coq| behave more like |Coq| v8.4. - The standard way of putting |Coq| in v8.4 compatibility mode is to pass the command + options and does a few redefinitions to make Coq behave more like Coq v8.4. + The standard way of putting Coq in v8.4 compatibility mode is to pass the command line flags "-require Coq.Compat.Coq84 -compat 8.4". Details of changes in 8.5 @@ -5174,7 +5174,7 @@ Details of changes in 8.5 Tools - Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of - putting |Coq| in v8.4 compatibility mode is to pass the command line flag + putting Coq in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom" if the 8.4 behavior of admit is needed, in which case it uses an axiom. @@ -5215,7 +5215,7 @@ Various performance improvements (time, space used by .vo files) Other bugfixes - Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v -- Added compatibility coercions from Specif.v which were present in |Coq| 8.4. +- Added compatibility coercions from Specif.v which were present in Coq 8.4. - Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic. - Allow to unset the refinement mode of Instance in ML - Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite. @@ -5230,7 +5230,7 @@ Other bugfixes - #4623: set tactic too weak with universes (regression) - Fix incorrect behavior of CS resolution - #4591: Uncaught exception in directory browsing. -- |CoqIDE| is more resilient to initialization errors. +- CoqIDE is more resilient to initialization errors. - #4614: "Fully check the document" is uninterruptible. - Try eta-expansion of records only on non-recursive ones - Fix bug when a sort is ascribed to a Record @@ -5240,23 +5240,23 @@ Other bugfixes - Fix strategy of Keyed Unification - #4608: Anomaly "output_value: abstract value (outside heap)". - #4607: do not read native code files if native compiler was disabled. -- #4105: poor escaping in the protocol between |CoqIDE| and coqtop. +- #4105: poor escaping in the protocol between CoqIDE and coqtop. - #4596: [rewrite] broke in the past few weeks. - #4533 (partial): respect declared global transparency of projections in unification.ml - #4544: Backtrack on using full betaiota reduction during keyed unification. -- #4540: |CoqIDE| bottom progress bar does not update. +- #4540: CoqIDE bottom progress bar does not update. - Fix regression from 8.4 in reflexivity - #4580: [Set Refine Instance Mode] also used for Program Instance. - #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683. - STM: Print/Extraction have to be skipped if -quick -- #4542: |CoqIDE|: STOP button also stops workers +- #4542: CoqIDE: STOP button also stops workers - STM: classify some variants of Instance as regular `` `Fork `` nodes. - #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). - Do not give a name to anonymous evars anymore. See bug #4547. - STM: always stock in vio files the first node (state) of a proof - STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 - Don't fail fatally if PATH is not set. -- #4537: |Coq| 8.5 is slower in typeclass resolution. +- #4537: Coq 8.5 is slower in typeclass resolution. - #4522: Incorrect "Warning..." on windows. - #4373: coqdep does not know about .vio files. - #3826: "Incompatible module types" is uninformative. @@ -5265,7 +5265,7 @@ Other bugfixes - #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported. - #4519: oops, global shadowed local universe level bindings. - #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed. -- #4548: |CoqIDE| crashes when going back one command +- #4548: CoqIDE crashes when going back one command Details of changes in 8.5pl2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -5286,8 +5286,8 @@ Other bugfixes - #4644: a regression in unification. - #4725: Function (Error: Conversion test raised an anomaly) and Program (Error: Cannot infer this placeholder of type) -- #4747: Problem building |Coq| 8.5pl1 with OCaml 4.03.0: Fatal warnings -- #4752: |CoqIDE| crash on files not ended by ".v". +- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings +- #4752: CoqIDE crash on files not ended by ".v". - #4777: printing inefficiency with implicit arguments - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" @@ -5301,7 +5301,7 @@ Other bugfixes - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. - triggered by |CoqIDE| + triggered by CoqIDE - #4069, #4718: congruence fails when universes are involved. Universes @@ -5364,7 +5364,7 @@ Other bugfixes - #5097: status of evars refined by "clear" in ltac: closed wrt evars. - #5150: Missing dependency of the test-suite subsystems in prerequisite. - Fix a bug in error printing of unif constraints -- #3941: Do not stop propagation of signals when |Coq| is busy. +- #3941: Do not stop propagation of signals when Coq is busy. - #4822: Incorrect assertion in cbn. - #3479 parsing of "{" and "}" when a keyword starts with "{" or "}". - #5127: Memory corruption with the VM. @@ -5378,9 +5378,9 @@ Version 8.4 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.4 contains the result of three long-term projects: a new +Coq version 8.4 contains the result of three long-term projects: a new modular library of arithmetic by Pierre Letouzey, a new proof engine by -Arnaud Spiwack and a new communication protocol for |CoqIDE| by Vincent +Arnaud Spiwack and a new communication protocol for CoqIDE by Vincent Gross. The new modular library of arithmetic extends, generalizes and unifies @@ -5402,16 +5402,16 @@ goals simultaneously, for reordering goals, all features which are planned for the next release. The new proof engine forced Pierre Letouzey to reimplement info and Show Script differently. -Before version 8.4, |CoqIDE| was linked to |Coq| with the graphical -interface living in a separate thread. From version 8.4, |CoqIDE| is a -separate process communicating with |Coq| through a textual channel. This -allows for a more robust interfacing, the ability to interrupt |Coq| +Before version 8.4, CoqIDE was linked to Coq with the graphical +interface living in a separate thread. From version 8.4, CoqIDE is a +separate process communicating with Coq through a textual channel. This +allows for a more robust interfacing, the ability to interrupt Coq without interrupting the interface, and the ability to manage several sessions in parallel. Relying on the infrastructure work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and Pierre-Marie Pédrot -contributed many various refinements of |CoqIDE|. +contributed many various refinements of CoqIDE. -|Coq| 8.4 also comes with a bunch of various smaller-scale changes +Coq 8.4 also comes with a bunch of various smaller-scale changes and improvements regarding the different components of the system. The underlying logic has been extended with :math:`\eta`-conversion @@ -5420,7 +5420,7 @@ addition of :math:`\eta`-conversion is justified by the confidence that the formulation of the Calculus of Inductive Constructions based on typed equality (such as the one considered in Lee and Werner to build a set-theoretic model of CIC :cite:`LeeWerner11`) is -applicable to the concrete implementation of |Coq|. +applicable to the concrete implementation of Coq. The underlying logic benefited also from a refinement of the guard condition for fixpoints by Pierre Boutillier, the point being that it is @@ -5489,19 +5489,19 @@ Julien Forest maintained the Function command. Matthieu Sozeau maintained the setoid rewriting mechanism. -|Coq| related tools have been upgraded too. In particular, coq\_makefile +Coq related tools have been upgraded too. In particular, coq\_makefile has been largely revised by Pierre Boutillier. Also, patches from Adam Chlipala for coqdoc have been integrated by Pierre Boutillier. Bruno Barras and Pierre Letouzey maintained the `coqchk` checker. Pierre Courtieu and Arnaud Spiwack contributed new features for using -|Coq| through Proof General. +Coq through Proof General. The Dp plugin has been removed. Use the plugin provided with Why 3 instead (http://why3.lri.fr/). -Under the hood, the |Coq| architecture benefited from improvements in +Under the hood, the Coq architecture benefited from improvements in terms of efficiency and robustness, especially regarding universes management and existential variables management, thanks to Pierre Letouzey and Yann Régis-Gianas with contributions from Stéphane Glondu @@ -5748,7 +5748,7 @@ Libraries * "<?" "<=?" "=?" for boolean tests such as Z.ltb Z.leb Z.eqb. * "÷" for the alternative integer division Z.quot implementing the Truncate - convention (former ZOdiv), while the notation for the |Coq| usual division + convention (former ZOdiv), while the notation for the Coq usual division Z.div implementing the Flooring convention remains "/". Their corresponding modulo functions are Z.rem (no notations) for Z.quot and Z.modulo (infix "mod" notation) for Z.div. @@ -5808,31 +5808,31 @@ Extraction universe polymorphism it cannot handle yet (the pair (I,I) being Prop). - Support of anonymous fields in record (#2555). -|CoqIDE| +CoqIDE -- |CoqIDE| now runs coqtop as separated process, making it more robust: +- CoqIDE now runs coqtop as separated process, making it more robust: coqtop subprocess can be interrupted, or even killed and relaunched (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts, the Windows version of coqide now requires Windows >= XP SP1. -- The communication between |CoqIDE| and coqtop is now done via a dialect +- The communication between CoqIDE and coqtop is now done via a dialect of XML (DOC TODO). -- The backtrack engine of |CoqIDE| has been reworked, it now uses the +- The backtrack engine of CoqIDE has been reworked, it now uses the "Backtrack" command similarly to Proof General. -- The |CoqIDE| parsing of sentences has be reworked and now supports +- The CoqIDE parsing of sentences has be reworked and now supports tactic delimitation via { }. -- |CoqIDE| now accepts the Abort command (wish #2357). -- |CoqIDE| can read coq_makefile files as "project file" and use it to +- CoqIDE now accepts the Abort command (wish #2357). +- CoqIDE can read coq_makefile files as "project file" and use it to set automatically options to send to coqtop. - Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators are not stored as a list anymore. Tools -- |Coq| now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, +- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, $XDG_DATA_DIRS/coq, and user-contribs before the standard library. -- |Coq| rc file has moved to $XDG_CONFIG_HOME/coq. +- Coq rc file has moved to $XDG_CONFIG_HOME/coq. - Major changes to coq_makefile: @@ -5890,9 +5890,9 @@ Module System namespace from ordinary definitions: "Definition E:=0. Module E. End E." is now accepted. -|CoqIDE| +CoqIDE -- |CoqIDE| now supports the "Restart" command, and "Undo" (with a warning). +- CoqIDE now supports the "Restart" command, and "Undo" (with a warning). Better support for "Abort". Details of changes in 8.4 @@ -5909,9 +5909,9 @@ Vernacular commands Notations - Most compatibility notations of the standard library are now tagged as - (compat xyz), where xyz is a former |Coq| version, for instance "8.3". + (compat xyz), where xyz is a former Coq version, for instance "8.3". These notations behave as (only parsing) notations, except that they may - triggers warnings (or errors) when used while |Coq| is not in a corresponding + triggers warnings (or errors) when used while Coq is not in a corresponding -compat mode. - To activate these compatibility warnings, use "Set Verbose Compat Notations" or the command-line flag -verbose-compat-notations. @@ -5941,7 +5941,7 @@ Version 8.3 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.3 is before all a transition version with refinements or +Coq version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic nsatz based on Hilbert’s Nullstellensatz for deciding systems of equations over rings. @@ -5980,7 +5980,7 @@ been done by Matthieu Sozeau, Hugo Herbelin and Pierre Letouzey. Matthieu Sozeau extended and refined the typeclasses and Program features (the Russell language). Pierre Letouzey maintained and improved the extraction mechanism. Bruno Barras and Élie Soubiran maintained the -|Coq| checker, Julien Forest maintained the Function mechanism for +Coq checker, Julien Forest maintained the Function mechanism for reasoning over recursively defined functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson maintained the Micromega platform for deciding systems of inequalities. @@ -5994,8 +5994,8 @@ more robust basis. Though invisible from outside, Arnaud Spiwack improved the general process of management of existential variables. Pierre Letouzey and -Stéphane Glondu improved the compilation scheme of the |Coq| archive. -Vincent Gross provided support to |CoqIDE|. Jean-Marc Notin provided +Stéphane Glondu improved the compilation scheme of the Coq archive. +Vincent Gross provided support to CoqIDE. Jean-Marc Notin provided support for benchmarking and archiving. Many users helped by reporting problems, providing patches, suggesting @@ -6144,12 +6144,12 @@ Module system "Inline" annotation in the type of its argument(s) (for examples of use of the new features, see libraries Structures and Numbers). - Coercions are now active only when modules are imported (use "Set Automatic - Coercions Import" to get the behavior of the previous versions of |Coq|). + Coercions Import" to get the behavior of the previous versions of Coq). Extraction - When using (Recursive) Extraction Library, the filenames are directly the - |Coq| ones with new appropriate extensions : we do not force anymore + Coq ones with new appropriate extensions : we do not force anymore uncapital first letters for Ocaml and capital ones for Haskell. - The extraction now tries harder to avoid code transformations that can be dangerous for the complexity. In particular many eta-expansions at the top @@ -6232,7 +6232,7 @@ Vernacular commands Library -- Use "standard" |Coq| names for the properties of eq and identity +- Use "standard" Coq names for the properties of eq and identity (e.g. refl_equal is now eq_refl). Support for compatibility is provided. - The function Compare_dec.nat_compare is now defined directly, @@ -6283,7 +6283,7 @@ Library - MSets library: an important evolution of the FSets library. "MSets" stands for Modular (Finite) Sets, by contrast with a forthcoming library of Class (Finite) Sets contributed by S. Lescuyer which will be - integrated with the next release of |Coq|. The main features of MSets are: + integrated with the next release of Coq. The main features of MSets are: + The use of Equivalence, Proper and other Type Classes features easing the handling of setoid equalities. @@ -6298,7 +6298,7 @@ Library Note: No Maps yet in MSets. The FSets library is still provided for compatibility, but will probably be considered as deprecated in the - next release of |Coq|. + next release of Coq. - Numbers library: @@ -6314,12 +6314,12 @@ Library Tools -- Option -R now supports binding |Coq| root read-only. +- Option -R now supports binding Coq root read-only. - New coqtop/coqc option -beautify to reformat .v files (usable e.g. to globally update notations). - New tool beautify-archive to beautify a full archive of developments. - New coqtop/coqc option -compat X.Y to simulate the general behavior - of previous versions of |Coq| (provides e.g. support for 8.2 compatibility). + of previous versions of Coq (provides e.g. support for 8.2 compatibility). Coqdoc @@ -6335,7 +6335,7 @@ Coqdoc - New option "--parse-comments" to allow parsing of regular ``(* *)`` comments. - New option "--plain-comments" to disable interpretation inside comments. -- New option "--interpolate" to try and typeset identifiers in |Coq| escapings +- New option "--interpolate" to try and typeset identifiers in Coq escapings using the available globalization information. - New option "--external url root" to refer to external libraries. - Links to section variables and notations now supported. @@ -6349,7 +6349,7 @@ Internal infrastructure - An experimental build mechanism via ocamlbuild is provided. From the top of the archive, run ./configure as usual, and then ./build. Feedback about this build mechanism is most welcome. - Compiling |Coq| on platforms such as Windows might be simpler + Compiling Coq on platforms such as Windows might be simpler this way, but this remains to be tested. - The Makefile system has been simplified and factorized with the ocamlbuild system. In particular "make" takes advantage @@ -6362,19 +6362,19 @@ Version 8.2 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.2 adds new features, new libraries and improves on many +Coq version 8.2 adds new features, new libraries and improves on many various aspects. -Regarding the language of |Coq|, the main novelty is the introduction by +Regarding the language of Coq, the main novelty is the introduction by Matthieu Sozeau of a package of commands providing Haskell-style typeclasses. Typeclasses, which come with a few convenient features such as type-based resolution of implicit arguments, play a new landmark role -in the architecture of |Coq| with respect to automation. For +in the architecture of Coq with respect to automation. For instance, thanks to typeclass support, Matthieu Sozeau could implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. -Another major improvement of |Coq| 8.2 is the evolution of the arithmetic +Another major improvement of Coq 8.2 is the evolution of the arithmetic libraries and of the tools associated to them. Benjamin Grégoire and Laurent Théry contributed a modular library for building arbitrarily large integers from bounded integers while Evgeny Makarov contributed a @@ -6398,7 +6398,7 @@ Arnaud Spiwack developed a library of 31-bits machine integers and, relying on Benjamin Grégoire and Laurent Théry’s library, delivered a library of unbounded integers in base :math:`2^{31}`. As importantly, he developed a notion of “retro-knowledge” so as to safely extend the -kernel-located bytecode-based efficient evaluation algorithm of |Coq| +kernel-located bytecode-based efficient evaluation algorithm of Coq version 8.1 to use 31-bits machine arithmetic for efficiently computing with the library of integers he developed. @@ -6430,16 +6430,16 @@ the Scheme command and of injection. Bruno Barras implemented the ``coqchk`` tool: this is a stand-alone type checker that can be used to certify .vo files. Especially, as this verifier runs in a separate process, it is granted not to be “hijacked” -by virtually malicious extensions added to |Coq|. +by virtually malicious extensions added to Coq. Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and Julien Forest acted as maintainers of features they implemented in previous -versions of |Coq|. +versions of Coq. -Julien Narboux contributed to |CoqIDE|. Nicolas Tabareau made the +Julien Narboux contributed to CoqIDE. Nicolas Tabareau made the adaptation of the interface of the old “setoid rewrite” tactic to the -new version. Lionel Mamane worked on the interaction between |Coq| and its -external interfaces. With Samuel Mimram, he also helped making |Coq| +new version. Lionel Mamane worked on the interaction between Coq and its +external interfaces. With Samuel Mimram, he also helped making Coq compatible with recent software tools. Russell O’Connor, Cezary Kaliszyk, Milad Niqui contributed to improve the libraries of integers, rational, and real numbers. We also thank many users and partners for @@ -6517,7 +6517,7 @@ Vernacular commands qualified names (this holds also for coqtop/coqc option -R). - SearchAbout supports negated search criteria, reference to logical objects by their notation, and more generally search of subterms. -- "Declare ML Module" now allows to import .cmxs files when |Coq| is +- "Declare ML Module" now allows to import .cmxs files when Coq is compiled in native code with a version of OCaml that supports native Dynlink (>= 3.11). - Specific sort constraints on Record now taken into account. @@ -6558,7 +6558,7 @@ Libraries version should be fairly good, but some adaptations may be required. * Interfaces of unordered ("weak") and ordered sets have been factorized - thanks to new features of |Coq| modules (in particular Include), see + thanks to new features of Coq modules (in particular Include), see FSetInterface. Same for maps. Hints in these interfaces have been reworked (they are now placed in a "set" database). * To allow full subtyping between weak and ordered sets, a field @@ -6589,7 +6589,7 @@ Libraries initial Ocaml code and written via the Function framework. - Library IntMap, subsumed by FSets/FMaps, has been removed from - |Coq| Standard Library and moved into a user contribution Cachan/IntMap + Coq Standard Library and moved into a user contribution Cachan/IntMap - Better computational behavior of some constants (eq_nat_dec and le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare @@ -6794,7 +6794,7 @@ Tactics - New tactic "specialize H with a" or "specialize (H a)" allows to transform in-place a universally-quantified hypothesis (H : forall x, T x) into its instantiated form (H : T a). Nota: "specialize" was in fact there in earlier - versions of |Coq|, but was undocumented, and had a slightly different behavior. + versions of Coq, but was undocumented, and had a slightly different behavior. - New tactic "contradict H" can be used to solve any kind of goal as long as the user can provide afterwards a proof of the negation of the hypothesis H. @@ -6838,7 +6838,7 @@ Program - Program Lemma, Axiom etc... now permit to have obligations in the statement iff they can be automatically solved by the default tactic. - Renamed "Obligations Tactic" command to "Obligation Tactic". -- New command "Preterm [ of id ]" to see the actual term fed to |Coq| for +- New command "Preterm [ of id ]" to see the actual term fed to Coq for debugging purposes. - New option "Transparent Obligations" to control the declaration of obligations as transparent or opaque. All obligations are now transparent @@ -6930,7 +6930,7 @@ Extraction not happen anymore. - The command Extract Inductive has now a syntax for infix notations. This - allows in particular to map |Coq| lists and pairs onto |OCaml| ones: + allows in particular to map Coq lists and pairs onto OCaml ones: + Extract Inductive list => list [ "[]" "(::)" ]. + Extract Inductive prod => "(*)" [ "(,)" ]. @@ -6944,16 +6944,16 @@ Extraction conflits with existing code, for instance when extracting module List to Ocaml. -|CoqIDE| +CoqIDE -- |CoqIDE| font defaults to monospace so as indentation to be meaningful. -- |CoqIDE| supports nested goals and any other kind of declaration in the middle +- CoqIDE font defaults to monospace so as indentation to be meaningful. +- CoqIDE supports nested goals and any other kind of declaration in the middle of a proof. -- Undoing non-tactic commands in |CoqIDE| works faster. -- New |CoqIDE| menu for activating display of various implicit informations. +- Undoing non-tactic commands in CoqIDE works faster. +- New CoqIDE menu for activating display of various implicit informations. - Added the possibility to choose the location of tabs in coqide: (in Edit->Preferences->Misc) -- New Open and Save As dialogs in |CoqIDE| which filter ``*.v`` files. +- New Open and Save As dialogs in CoqIDE which filter ``*.v`` files. Tools @@ -6962,22 +6962,22 @@ Tools - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. - The binary "parser" has been renamed to "coq-parser". - Improved coqdoc and dump of globalization information to give more - meta-information on identifiers. All categories of |Coq| definitions are + meta-information on identifiers. All categories of Coq definitions are supported, which makes typesetting trivial in the generated documentation. Support for hyperlinking and indexing developments in the tex output has been implemented as well. Miscellaneous -- |Coq| installation provides enough files so that Ocaml's extensions need not - the |Coq| sources to be compiled (this assumes O'Caml 3.10 and Camlp5). +- Coq installation provides enough files so that Ocaml's extensions need not + the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5). - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the Whelp search tool. - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into "Test Printing Let for ref" and "Test Printing If for ref". - An overhauled build system (new Makefiles); see dev/doc/build-system.txt. - Add -browser option to configure script. -- Build a shared library for the C part of |Coq|, and use it by default on +- Build a shared library for the C part of Coq, and use it by default on non-(Windows or MacOS) systems. Bytecode executables are now pure. The behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and -custom configure options. @@ -6990,10 +6990,10 @@ Version 8.1 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.1 adds various new functionalities. +Coq version 8.1 adds various new functionalities. Benjamin Grégoire implemented an alternative algorithm to check the -convertibility of terms in the |Coq| type checker. This alternative +convertibility of terms in the Coq type checker. This alternative algorithm works by compilation to an efficient bytecode that is interpreted in an abstract machine similar to Xavier Leroy’s ZINC machine. Convertibility is performed by comparing the normal forms. This @@ -7023,7 +7023,7 @@ Claudio Sacerdoti Coen added new tactic features. Hugo Herbelin implemented matching on disjunctive patterns. -New mechanisms made easier the communication between |Coq| and external +New mechanisms made easier the communication between Coq and external provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented connections with the provers cvcl, Simplify and zenon. Hugo Herbelin implemented an experimental protocol for calling external tools from the @@ -7037,7 +7037,7 @@ unresolved implicit has been implemented by Hugo Herbelin. Laurent Théry’s contribution on strings and Pierre Letouzey and Jean-Christophe Filliâtre’s contribution on finite maps have been -integrated to the |Coq| standard library. Pierre Letouzey developed a +integrated to the Coq standard library. Pierre Letouzey developed a library about finite sets “à la Objective Caml”. With Jean-Marc Notin, he extended the library on lists. Pierre Letouzey’s contribution on rational numbers has been integrated and extended. @@ -7098,7 +7098,7 @@ Vernacular commands Ltac and tactic syntactic extensions -- New primitive "external" for communication with tool external to |Coq| +- New primitive "external" for communication with tool external to Coq - New semantics for "match t with": if a clause returns a tactic, it is now applied to the current goal. If it fails, the next clause or next matching subterm is tried (i.e. it behaves as "match @@ -7123,7 +7123,7 @@ Tactics - New conversion tactic "vm_compute": evaluates the goal (or an hypothesis) with a call-by-value strategy, using the compiled version of terms. -- When rewriting H where H is not directly a |Coq| equality, search first H for +- When rewriting H where H is not directly a Coq equality, search first H for a registered setoid equality before starting to reduce in H. This is unlikely to break any script. Should this happen nonetheless, one can insert manually some "unfold ... in H" before rewriting. @@ -7168,7 +7168,7 @@ Tactics - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns. -- New introduction pattern "?" for letting |Coq| choose a name. +- New introduction pattern "?" for letting Coq choose a name. - Introduction patterns now support side hypotheses (e.g. intros [|] on "(nat -> nat) -> nat" works). @@ -7254,7 +7254,7 @@ Libraries Zlt_square_simpl removed; fixed names mentioning letter O instead of digit 0; weaken premises in Z_lt_induction). - Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type. -- Znumtheory now contains a gcd function that can compute within |Coq|. +- Znumtheory now contains a gcd function that can compute within Coq. - More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and Acc_iter2. - Change of the internal names of lemmas in OmegaLemmas. @@ -7287,7 +7287,7 @@ Tools - Tool coq_makefile now removes custom targets that are file names in "make clean" - New environment variable COQREMOTEBROWSER to set the command invoked - to start the remote browser both in |Coq| and |CoqIDE|. Standard syntax: + to start the remote browser both in Coq and CoqIDE. Standard syntax: "%s" is the placeholder for the URL. Details of changes in 8.1gamma @@ -7363,7 +7363,7 @@ Version 8.0 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8 is a major revision of the |Coq| proof assistant. First, the +Coq version 8 is a major revision of the Coq proof assistant. First, the underlying logic is slightly different. The so-called *impredicativity* of the sort Set has been dropped. The main reason is that it is inconsistent with the principle of description which is quite a useful @@ -7392,7 +7392,7 @@ main motivations were Together with the revision of the concrete syntax, a new mechanism of *notation scopes* permits to reuse the same symbols (typically +, -, \*, /, <, <=) in various mathematical theories without any -ambiguities for |Coq|, leading to a largely improved readability of |Coq| +ambiguities for Coq, leading to a largely improved readability of Coq scripts. New commands to easily add new symbols are also provided. Coming with the new syntax of terms, a slight reform of the tactic @@ -7401,30 +7401,30 @@ purpose here is a better uniformity making the tactics and commands easier to use and to remember. Thirdly, a restructuring and uniformization of the standard library of -|Coq| has been performed. There is now just one Leibniz equality usable -for all the different kinds of |Coq| objects. Also, the set of real +Coq has been performed. There is now just one Leibniz equality usable +for all the different kinds of Coq objects. Also, the set of real numbers now lies at the same level as the sets of natural and integer numbers. Finally, the names of the standard properties of numbers now follow a standard pattern and the symbolic notations for the standard definitions as well. -The fourth point is the release of |CoqIDE|, a new graphical gtk2-based -interface fully integrated with |Coq|. Close in style to the Proof General -Emacs interface, it is faster and its integration with |Coq| makes +The fourth point is the release of CoqIDE, a new graphical gtk2-based +interface fully integrated with Coq. Close in style to the Proof General +Emacs interface, it is faster and its integration with Coq makes interactive developments more friendly. All mathematical Unicode symbols -are usable within |CoqIDE|. +are usable within CoqIDE. -Finally, the module system of |Coq| completes the picture of |Coq| version +Finally, the module system of Coq completes the picture of Coq version 8.0. Though released with an experimental status in the previous version 7.4, it should be considered as a salient feature of the new version. -Besides, |Coq| comes with its load of novelties and improvements: new or +Besides, Coq comes with its load of novelties and improvements: new or improved tactics (including a new tactic for solving first-order statements), new management commands, extended libraries. Bruno Barras and Hugo Herbelin have been the main contributors of the reflection and the implementation of the new syntax. The smart automatic -translator from old to new syntax released with |Coq| is also their work +translator from old to new syntax released with Coq is also their work with contributions by Olivier Desmettre. Hugo Herbelin is the main designer and implementer of the notion of @@ -7437,21 +7437,21 @@ Pierre Corbineau is the main designer and implementer of the new tactic for solving first-order statements in presence of inductive types. He is also the maintainer of the non-domain specific automation tactics. -Benjamin Monate is the developer of the |CoqIDE| graphical interface with +Benjamin Monate is the developer of the CoqIDE graphical interface with contributions by Jean-Christophe Filliâtre, Pierre Letouzey, Claude Marché and Bruno Barras. -Claude Marché coordinated the edition of the Reference Manual for |Coq| +Claude Marché coordinated the edition of the Reference Manual for Coq V8.0. Pierre Letouzey and Jacek Chrząszcz respectively maintained the -extraction tool and module system of |Coq|. +extraction tool and module system of Coq. Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other contributors from Sophia-Antipolis and Nijmegen participated in extending the library. -Julien Narboux built a NSIS-based automatic |Coq| installation tool for +Julien Narboux built a NSIS-based automatic Coq installation tool for the Windows platform. Hugo Herbelin and Christine Paulin coordinated the development which was @@ -7618,19 +7618,19 @@ Miscellaneous Incompatibilities -- Persistence of true_sub (4 incompatibilities in |Coq| user contributions) +- Persistence of true_sub (4 incompatibilities in Coq user contributions) - Variable names of some constants changed for a better uniformity (2 changes - in |Coq| user contributions) + in Coq user contributions) - Naming of quantified names in goal now avoid global names (2 occurrences) - NewInduction naming for inductive types with functional arguments - (no incompatibility in |Coq| user contributions) + (no incompatibility in Coq user contributions) - Contradiction now solve more goals (source of 2 incompatibilities) - Merge of eq and eqT may exceptionally result in subgoals now solved automatically - Redundant pairs of ZArith lemmas may have different names: it may cause "Apply/Rewrite with" to fail if using the first name of a pair of redundant lemmas (this is solved by renaming the variables bound by - "with"; 3 incompatibilities in |Coq| user contribs) + "with"; 3 incompatibilities in Coq user contribs) - ML programs referring to constants from fast_integer.v must use "Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead @@ -7666,7 +7666,7 @@ Revision of the standard library "Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0") - Order and names of arguments of basic lemmas on nat, Z, positive and R have been made uniform. -- Notions of |Coq| initial state are declared with (strict) implicit arguments +- Notions of Coq initial state are declared with (strict) implicit arguments - eq merged with eqT: old eq disappear, new eq (written =) is old eqT and new eqT is syntactic sugar for new eq (notation == is an alias for = and is written as it, exceptional source of incompatibilities) @@ -7697,7 +7697,7 @@ Known problems of the automatic translation - iso-latin-1 characters are no longer supported: move your files to 7-bits ASCII or unicode before translation (switch to unicode is automatically done if a file is loaded and saved again by coqide) -- Renaming in ZArith: incompatibilities in |Coq| user contribs due to +- Renaming in ZArith: incompatibilities in Coq user contribs due to merging names INZ, from Reals, and inject_nat. - Renaming and new lemmas in ZArith: may clash with names used by users - Restructuration of ZArith: replace requirement of specific modules @@ -7747,7 +7747,7 @@ Tactics and the tactic Language Executables and tools - Added option -top to change the name of the toplevel module "Top" -- Coqdoc updated to new syntax and now part of |Coq| sources +- Coqdoc updated to new syntax and now part of Coq sources - XML exportation tool now exports the structure of vernacular files (cf chapter 13 in the reference manual) diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index bab9bfcadb..c5ef92a1bf 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -1,23 +1,23 @@ .. _history: ---------------------- -Early history of |Coq| +Early history of Coq ---------------------- Historical roots ---------------- -|Coq| is a proof assistant for higher-order logic, allowing the +Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal specification. It is the result of about ten years [#years]_ of research -of the |Coq| project. We shall briefly survey here three main aspects: the +of the Coq project. We shall briefly survey here three main aspects: the *logical language* in which we write our axiomatizations and specifications, the *proof assistant* which allows the development of verified mathematical proofs, and the *program extractor* which synthesizes computer programs obeying their formal specifications, written as logical assertions in the language. -The logical language used by |Coq| is a variety of type theory, called the +The logical language used by Coq is a variety of type theory, called the *Calculus of Inductive Constructions*. Without going back to Leibniz and Boole, we can date the creation of what is now called mathematical logic to the work of Frege and Peano at the turn of the century. The discovery @@ -108,7 +108,7 @@ modules, automatically generated from a consistency proof of their formal specifications. We are however still far from being able to use this methodology in a smooth interaction with the standard tools from software engineering, i.e. compilers, linkers, run-time systems taking -advantage of special hardware, debuggers, and the like. We hope that |Coq| +advantage of special hardware, debuggers, and the like. We hope that Coq can be of use to researchers interested in experimenting with this new methodology. @@ -153,8 +153,8 @@ by A. Felty. It allowed operation of the theorem-prover through the manipulation of windows, menus, mouse-sensitive buttons, and other widgets. This system (Version 5.6) was released in 1991. -|Coq| was ported to the new implementation Caml-light of X. Leroy and D. -Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version of |Coq| +Coq was ported to the new implementation Caml-light of X. Leroy and D. +Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version of Coq was then coordinated by C. Murthy, with new tools designed by C. Parent to prove properties of ML programs (this methodology is dual to program extraction) and a new user-interaction loop. This system (Version 5.8) @@ -163,9 +163,9 @@ by Y. Bertot from the Croap project from INRIA-Sophia-Antipolis. In parallel, G. Dowek and H. Herbelin developed a new proof engine, allowing the general manipulation of existential variables consistently -with dependent types in an experimental version of |Coq| (V5.9). +with dependent types in an experimental version of Coq (V5.9). -The version V5.10 of |Coq| is based on a generic system for manipulating +The version V5.10 of Coq is based on a generic system for manipulating terms with binding operators due to Chet Murthy. A new proof engine allows the parallel development of partial proofs for independent subgoals. The structure of these proof trees is a mixed representation @@ -477,7 +477,7 @@ C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`. This led to the Calculus of Inductive Constructions, logical formalism implemented in Versions 5 upward of the system, and documented in: -C. Paulin-Mohring. *Inductive Definitions in the System |Coq| - Rules +C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules and Properties* :cite:`P93`. The last version of CONSTR is Version 4.11, which was last distributed @@ -489,7 +489,7 @@ Version 5 ~~~~~~~~~ At the end of 1989, Version 5.1 was started, and renamed as the system -|Coq| for the Calculus of Inductive Constructions. It was then ported to +Coq for the Calculus of Inductive Constructions. It was then ported to the new stand-alone implementation of ML called Caml-light. In 1990 many changes occurred. Thierry Coquand left for Chalmers @@ -497,7 +497,7 @@ University in Göteborg. Christine Paulin-Mohring took a CNRS researcher position at the LIP laboratory of École Normale Supérieure de Lyon. Project Formel was terminated, and gave rise to two teams: Cristal at INRIA-Roquencourt, that continued developments in -functional programming with Caml-light then OCaml, and |Coq|, continuing +functional programming with Caml-light then OCaml, and Coq, continuing the type theory research, with a joint team headed by Gérard Huet at INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory of CNRS-ENS Lyon. @@ -519,14 +519,14 @@ Versions 6 Version 6.1 ~~~~~~~~~~~ -The present version 6.1 of |Coq| is based on the V5.10 architecture. It +The present version 6.1 of Coq is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The underlying framework has slightly changed and allows more conversions between sorts. The new version provides powerful tools for easier developments. -Cristina Cornes designed an extension of the |Coq| syntax to allow +Cristina Cornes designed an extension of the Coq syntax to allow definition of terms using a powerful pattern matching analysis in the style of ML programs. @@ -539,13 +539,13 @@ written. Yann Coscoy designed a command which explains a proof term using natural language. Pierre Crégut built a new tactic which solves problems in quantifier-free Presburger Arithmetic. Both functionalities have been -integrated to the |Coq| system by Hugo Herbelin. +integrated to the Coq system by Hugo Herbelin. Samuel Boutin designed a tactic for simplification of commutative rings using a canonical set of rewriting rules and equality modulo associativity and commutativity. -Finally the organisation of the |Coq| distribution has been supervised by +Finally the organisation of the Coq distribution has been supervised by Jean-Christophe Filliâtre with the help of Judicaël Courant and Bruno Barras. @@ -556,21 +556,21 @@ Barras. Version 6.2 ~~~~~~~~~~~ -In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor +In version 6.2 of Coq, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. -Daniel de Rauglaudre made the first adaptation of |Coq| for camlp4, this -work was continued by Bruno Barras who also changed the structure of |Coq| +Daniel de Rauglaudre made the first adaptation of Coq for camlp4, this +work was continued by Bruno Barras who also changed the structure of Coq abstract syntax trees and the primitives to manipulate them. The result of these changes is a faster parsing procedure with greatly improved syntax-error messages. The user-interface to introduce grammar or pretty-printing rules has also changed. Eduardo Giménez redesigned the internal tactic libraries, giving uniform -names to Caml functions corresponding to |Coq| tactic names. +names to Caml functions corresponding to Coq tactic names. Bruno Barras wrote new, more efficient reduction functions. -Hugo Herbelin introduced more uniform notations in the |Coq| specification +Hugo Herbelin introduced more uniform notations in the Coq specification language: the definitions by fixpoints and pattern matching have a more readable syntax. Patrick Loiseleur introduced user-friendly notations for arithmetic expressions. @@ -586,10 +586,10 @@ a proof term with holes as a proof scheme. David Delahaye designed the tool to search an object in the library given its type (up to isomorphism). -Henri Laulhère produced the |Coq| distribution for the Windows +Henri Laulhère produced the Coq distribution for the Windows environment. -Finally, Hugo Herbelin was the main coordinator of the |Coq| documentation +Finally, Hugo Herbelin was the main coordinator of the Coq documentation with principal contributions by Bruno Barras, David Delahaye, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin and Patrick Loiseleur. @@ -639,7 +639,7 @@ Summary of changes The version V7 is a new implementation started in September 1999 by Jean-Christophe Filliâtre. This is a major revision with respect to the -internal architecture of the system. The |Coq| version 7.0 was distributed +internal architecture of the system. The Coq version 7.0 was distributed in March 2001, version 7.1 in September 2001, version 7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in February 2003. @@ -653,13 +653,13 @@ Hugo Herbelin introduced a new structure of terms with local definitions. He introduced “qualified” names, wrote a new pattern matching compilation algorithm and designed a more compact algorithm for checking the logical consistency of universes. He -contributed to the simplification of |Coq| internal structures and the +contributed to the simplification of Coq internal structures and the optimisation of the system. He added basic tactics for forward reasoning and coercions in patterns. David Delahaye introduced a new language for tactics. General tactics using pattern matching on goals and context can directly be written from -the |Coq| toplevel. He also provided primitives for the design of +the Coq toplevel. He also provided primitives for the design of user-defined tactics in Caml. Micaela Mayero contributed the library on real numbers. Olivier @@ -668,16 +668,16 @@ square, square roots, finite sums, Chasles property and basic plane geometry. Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new -extraction procedure from |Coq| terms to Caml or Haskell programs. This +extraction procedure from Coq terms to Caml or Haskell programs. This new extraction procedure, unlike the one implemented in previous version -of |Coq| is able to handle all terms in the Calculus of Inductive +of Coq is able to handle all terms in the Calculus of Inductive Constructions, even involving universes and strong elimination. P. Letouzey adapted user contributions to extract ML programs when it was sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation -tool for |Coq| libraries usable from version 7.2. +tool for Coq libraries usable from version 7.2. Bruno Barras improved the efficiency of the reduction algorithm and the -confidence level in the correctness of |Coq| critical type checking +confidence level in the correctness of Coq critical type checking algorithm. Yves Bertot designed the ``SearchPattern`` and ``SearchRewrite`` tools @@ -696,7 +696,7 @@ real numbers. Pierre Crégut developed a new, reflection-based version of the Omega decision procedure. -Claudio Sacerdoti Coen designed an XML output for the |Coq| modules to be +Claudio Sacerdoti Coen designed an XML output for the Coq modules to be used in the Hypertextual Electronic Library of Mathematics (HELM cf http://www.cs.unibo.it/helm). @@ -706,13 +706,13 @@ 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 Chrząszcz 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. Many discussions within the Démons team and the LogiCal project -influenced significantly the design of |Coq| especially with J. Courant, +influenced significantly the design of Coq especially with J. Courant, J. Duprat, J. Goubault, A. Miquel, C. Marché, B. Monate and B. Werner. Intensive users suggested improvements of the system : Y. Bertot, L. @@ -736,7 +736,7 @@ Notes: Main novelties ^^^^^^^^^^^^^^ -References are to |Coq| 7.1 reference manual +References are to Coq 7.1 reference manual - New primitive let-in construct (see sections 1.2.8 and ) - Long names (see sections 2.6 and 2.7) @@ -770,7 +770,7 @@ Language: long names name, the name of the module in which they are defined (Top if in coqtop), and possibly an arbitrary long sequence of directory (e.g. "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part - of |Coq| standard library, "Lists" means it is defined in the Lists + of Coq standard library, "Lists" means it is defined in the Lists library and "PolyList" means it is in the file Polylist) (+) - Constructions can be referred by their base name, or, in case of @@ -829,7 +829,7 @@ Reduction - Constants declared as opaque (using Qed) can no longer become transparent (a constant intended to be alternatively opaque and transparent must be declared as transparent (using Defined)); a risk - exists (until next |Coq| version) that Simpl and Hnf reduces opaque + exists (until next Coq version) that Simpl and Hnf reduces opaque constants (*) @@ -1171,7 +1171,7 @@ Incompatibilities - New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility - Extra parentheses may exceptionally be needed in tactic definitions. -- |Coq| extensions written in |OCaml| need to be updated (see dev/changements.txt +- Coq extensions written in OCaml need to be updated (see dev/changements.txt for a description of the main changes in the interface files of V7.2) - New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities @@ -1205,7 +1205,7 @@ Tactics product if needed (source of incompatibilities) - "Match Context" now matching more recent hypotheses first and failing only on user errors and Fail tactic (possible source of incompatibilities) -- Tactic Definition's without arguments now allowed in |Coq| states +- Tactic Definition's without arguments now allowed in Coq states - Better simplification and discrimination made by Inversion (source of incompatibilities) @@ -1239,7 +1239,7 @@ User Contributions - CongruenceClosure (congruence closure decision procedure) [Pierre Corbineau, ENS Cachan] - MapleMode (an interface to embed Maple simplification procedures over - rational fractions in |Coq|) + rational fractions in Coq) [David Delahaye, Micaela Mayero, Chalmers University] - Presburger: A formalization of Presburger's algorithm [Laurent Thery, INRIA Sophia Antipolis] @@ -1283,7 +1283,7 @@ Bug fixes Misc - - Ocaml version >= 3.06 is needed to compile |Coq| from sources + - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and LetTac (#1402) @@ -1398,7 +1398,7 @@ Extraction (See details in plugins/extraction/CHANGES and README): - An experimental Scheme extraction is provided. - Concerning OCaml, extracted code is now ensured to always type check, thanks to automatic inserting of Obj.magic. -- Experimental extraction of |Coq| new modules to Ocaml modules. +- Experimental extraction of Coq new modules to Ocaml modules. Proof rendering in natural language diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index dc16897d42..06a677d837 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,8 +1,8 @@ -This is the reference manual of |Coq|. |Coq| is an interactive theorem +This is the reference manual of Coq. Coq is an interactive theorem prover. It lets you formalize mathematical concepts and then helps you interactively generate machine-checked proofs of theorems. Machine checking gives users much more confidence that the proofs are -correct compared to human-generated and -checked proofs. |Coq| has been +correct compared to human-generated and -checked proofs. Coq has been used in a number of flagship verification projects, including the `CompCert verified C compiler <http://compcert.inria.fr/>`_, and has served to verify the proof of the `four color theorem @@ -18,49 +18,49 @@ arithmetic). :ref:`Ltac <ltac>` and its planned replacement, combining existing tactics with looping and conditional constructs. These permit automation of large parts of proofs and sometimes entire proofs. Furthermore, users can add novel tactics or functionality by -creating |Coq| plugins using |OCaml|. +creating Coq plugins using OCaml. -The |Coq| kernel, a small part of |Coq|, does the final verification that +The Coq kernel, a small part of Coq, does the final verification that the tactic-generated proof is valid. Usually the tactic-generated proof is indeed correct, but delegating proof verification to the kernel means that even if a tactic is buggy, it won't be able to introduce an incorrect proof into the system. -Finally, |Coq| also supports extraction of verified programs to -programming languages such as |OCaml| and Haskell. This provides a way -of executing |Coq| code efficiently and can be used to create verified +Finally, Coq also supports extraction of verified programs to +programming languages such as OCaml and Haskell. This provides a way +of executing Coq code efficiently and can be used to create verified software libraries. -To learn |Coq|, beginners are advised to first start with a tutorial / +To learn Coq, beginners are advised to first start with a tutorial / book. Several such tutorials / books are listed at https://coq.inria.fr/documentation. This manual is organized in three main parts, plus an appendix: -- **The first part presents the specification language of |Coq|**, that +- **The first part presents the specification language of Coq**, that allows to define programs and state mathematical theorems. - :ref:`core-language` presents the language that the kernel of |Coq| + :ref:`core-language` presents the language that the kernel of Coq understands. :ref:`extensions` presents the richer language, with notations, implicits, etc. that a user can use and which is translated down to the language of the kernel by means of an "elaboration process". - **The second part presents the interactive proof mode**, the central - feature of |Coq|. :ref:`writing-proofs` introduces this interactive + feature of Coq. :ref:`writing-proofs` introduces this interactive proof mode and the available proof languages. :ref:`automatic-tactics` presents some more advanced tactics, while :ref:`writing-tactics` is about the languages that allow a user to combine tactics together and develop new ones. -- **The third part shows how to use |Coq| in practice.** +- **The third part shows how to use Coq in practice.** :ref:`libraries` presents some of the essential reusable blocks from the ecosystem and some particularly important extensions such as the program extraction mechanism. :ref:`tools` documents important - tools that a user needs to build a |Coq| project. + tools that a user needs to build a Coq project. - In the appendix, :ref:`history-and-changes` presents the history of - |Coq| and changes in recent releases. This is an important reference - if you upgrade the version of |Coq| that you use. The various + Coq and changes in recent releases. This is an important reference + if you upgrade the version of Coq that you use. The various :ref:`indexes <indexes>` are very useful to **quickly browse the manual and find what you are looking for.** They are often the main entry point to the manual. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index f1ed64e52a..85b04f6df0 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1,7 +1,7 @@ Typing rules ==================================== -The underlying formal language of |Coq| is a *Calculus of Inductive +The underlying formal language of Coq is a *Calculus of Inductive Constructions* (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related work are provided in a separate chapter; see *Credits*. @@ -33,7 +33,7 @@ the following rules. #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms. #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then - :math:`∀ x:T,~U` (:g:`forall x:T, U` in |Coq| concrete syntax) is a term. + :math:`∀ x:T,~U` (:g:`forall x:T, U` in Coq concrete syntax) is a term. If :math:`x` occurs in :math:`U`, :math:`∀ x:T,~U` reads as “for all :math:`x` of type :math:`T`, :math:`U`”. As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,~U` is @@ -43,11 +43,11 @@ the following rules. written: :math:`T \rightarrow U`. #. if :math:`x` is a variable and :math:`T`, :math:`u` are terms then :math:`λ x:T .~u` (:g:`fun x:T => u` - in |Coq| concrete syntax) is a term. This is a notation for the + in Coq concrete syntax) is a term. This is a notation for the λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T .~u` is a function which maps elements of :math:`T` to the expression :math:`u`. #. if :math:`t` and :math:`u` are terms then :math:`(t~u)` is a term - (:g:`t u` in |Coq| concrete + (:g:`t u` in Coq concrete syntax). The term :math:`(t~u)` reads as “:math:`t` applied to :math:`u`”. #. if :math:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are terms then :math:`\letin{x}{t:T}{u}` is @@ -91,10 +91,10 @@ Let us assume that ``mult`` is a function of type :math:`\nat→\nat→\nat` and predicate of type :math:`\nat→\nat→ \Prop`. The λ-abstraction can serve to build “ordinary” functions as in :math:`λ x:\nat.~(\kw{mult}~x~x)` (i.e. :g:`fun x:nat => mult x x` -in |Coq| notation) but may build also predicates over the natural +in Coq notation) but may build also predicates over the natural numbers. For instance :math:`λ x:\nat.~(\kw{eqnat}~x~0)` (i.e. :g:`fun x:nat => eqnat x 0` -in |Coq| notation) will represent the predicate of one variable :math:`x` which +in Coq notation) will represent the predicate of one variable :math:`x` which asserts the equality of :math:`x` with :math:`0`. This predicate has type :math:`\nat → \Prop` and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to give an @@ -524,7 +524,7 @@ One can consequently derive the following property. The Calculus of Inductive Constructions with impredicative Set ----------------------------------------------------------------- -|Coq| can be used as a type checker for the Calculus of Inductive +Coq can be used as a type checker for the Calculus of Inductive Constructions with an impredicative sort :math:`\Set` by using the compiler option ``-impredicative-set``. For example, using the ordinary `coqtop` command, the following is rejected, diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 485dfd964d..d061ed41f1 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1,28 +1,28 @@ .. _thecoqlibrary: -The |Coq| library +The Coq library ================= .. index:: single: Theories -The |Coq| library has two parts: +The Coq library has two parts: * The :gdef:`prelude`: definitions and theorems for the most commonly used elementary logical notions and - data types. |Coq| normally loads these files automatically when it starts. + data types. Coq normally loads these files automatically when it starts. * The :gdef:`standard library`: general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the ``Require`` command (see :ref:`compiled-files`) -There are also many libraries provided by |Coq| users' community. +There are also many libraries provided by Coq users' community. These libraries and developments are available for download at http://coq.inria.fr (see :ref:`userscontributions`). -This chapter briefly reviews the |Coq| libraries whose contents can +This chapter briefly reviews the Coq libraries whose contents can also be browsed at http://coq.inria.fr/stdlib/. @@ -32,9 +32,9 @@ The prelude ----------- This section lists the basic notions and results which are directly -available in the standard |Coq| system. Most of these constructions +available in the standard Coq system. Most of these constructions are defined in the ``Prelude`` module in directory ``theories/Init`` -in the |Coq| root directory; this includes the modules +in the Coq root directory; this includes the modules ``Notations``, ``Logic``, ``Datatypes``, @@ -92,7 +92,7 @@ Notation Precedence Associativity Logic ~~~~~ -The basic library of |Coq| comes with the definitions of standard +The basic library of Coq comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the subclass :token:`form` of the syntactic class :token:`term`. The constructs @@ -767,7 +767,7 @@ the modules they provide are compiled at installation time. So they are directly accessible with the command ``Require`` (see Section :ref:`compiled-files`). -The different modules of the |Coq| standard library are documented +The different modules of the Coq standard library are documented online at https://coq.inria.fr/stdlib. Peano’s arithmetic (nat) diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index a38282d41a..e029068630 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -117,7 +117,7 @@ Assumptions Assumptions extend the environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by |Coq| if and only if this :n:`@type` is a correct type in the environment +by Coq if and only if this :n:`@type` is a correct type in the environment preexisting the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index dfa2aaf8ff..5406da38a1 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -10,7 +10,7 @@ manual. Then, we present the essential vocabulary necessary to read the rest of the manual. Other terms are defined throughout the manual. The reader may refer to the :ref:`glossary index <glossary_index>` for a complete list of defined terms. Finally, we describe the various types of -settings that |Coq| provides. +settings that Coq provides. Syntax and lexical conventions ------------------------------ @@ -21,7 +21,7 @@ Syntax conventions ~~~~~~~~~~~~~~~~~~ The syntax described in this documentation is equivalent to that -accepted by the |Coq| parser, but the grammar has been edited +accepted by the Coq parser, but the grammar has been edited to improve readability and presentation. In the grammar presented in this manual, the terminal symbols are @@ -49,13 +49,13 @@ graphically using the following kinds of blocks: `Precedence levels <https://en.wikipedia.org/wiki/Order_of_operations>`_ that are -implemented in the |Coq| parser are shown in the documentation by +implemented in the Coq parser are shown in the documentation by appending the level to the nonterminal name (as in :n:`@term100` or :n:`@ltac_expr3`). .. note:: - |Coq| uses an extensible parser. Plugins and the :ref:`notation + Coq uses an extensible parser. Plugins and the :ref:`notation system <syntax-extensions-and-notation-scopes>` can extend the syntax at run time. Some notations are defined in the :term:`prelude`, which is loaded by default. The documented grammar doesn't include @@ -71,8 +71,8 @@ appending the level to the nonterminal name (as in :n:`@term100` or Given the complexity of these parsing rules, it would be extremely difficult to create an external program that can properly parse a - |Coq| document. Therefore, tool writers are advised to delegate - parsing to |Coq|, by communicating with it, for instance through + Coq document. Therefore, tool writers are advised to delegate + parsing to Coq, by communicating with it, for instance through `SerAPI <https://github.com/ejgallego/coq-serapi>`_. .. seealso:: :cmd:`Print Grammar` @@ -134,7 +134,7 @@ Numbers hexdigit ::= {| 0 .. 9 | a .. f | A .. F } :n:`@integer` and :n:`@natural` are limited to the range that fits - into an |OCaml| integer (63-bit integers on most architectures). + into an OCaml integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. The :ref:`standard library <thecoqlibrary>` provides some @@ -152,8 +152,8 @@ Strings :token:`string`. Keywords - The following character sequences are keywords defined in the main |Coq| grammar - that cannot be used as identifiers (even when starting |Coq| with the `-noinit` + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop @@ -168,8 +168,8 @@ Keywords keywords. Other tokens - The following character sequences are tokens defined in the main |Coq| grammar - (even when starting |Coq| with the `-noinit` command-line flag):: + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> ; < <+ <- <: @@ -195,7 +195,7 @@ Essential vocabulary -------------------- This section presents the most essential notions to understand the -rest of the |Coq| manual: :term:`terms <term>` and :term:`types +rest of the Coq manual: :term:`terms <term>` and :term:`types <type>` on the one hand, :term:`commands <command>` and :term:`tactics <tactic>` on the other hand. @@ -203,14 +203,14 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types term - Terms are the basic expressions of |Coq|. Terms can represent + Terms are the basic expressions of Coq. Terms can represent mathematical expressions, propositions and proofs, but also executable programs and program types. Here is the top-level syntax of terms. Each of the listed constructs is presented in a dedicated section. Some of these constructs (like :n:`@term_forall_or_fun`) are part of the core - language that the kernel of |Coq| understands and are therefore + language that the kernel of Coq understands and are therefore described in :ref:`this chapter <core-language>`, while others (like :n:`@term_if`) are language extensions that are presented in :ref:`the next chapter <extensions>`. @@ -256,18 +256,18 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types type - To be valid and accepted by the |Coq| kernel, a term needs an + To be valid and accepted by the Coq kernel, a term needs an associated type. We express this relationship by “:math:`x` *of type* :math:`T`”, which we write as “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as “:math:`x` *belongs to* :math:`T`”. - The |Coq| kernel is a type checker: it verifies that a term has + The Coq kernel is a type checker: it verifies that a term has the expected type by applying a set of typing rules (see :ref:`Typing-rules`). If that's indeed the case, we say that the term is :gdef:`well-typed`. - A special feature of the |Coq| language is that types can depend + A special feature of the Coq language is that types can depend on terms (we say that the language is `dependently-typed <https://en.wikipedia.org/wiki/Dependent_type>`_). Because of this, types and terms share a common syntax. All types are terms, @@ -289,13 +289,13 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types mathematics alternative to the standard `"set theory" <https://en.wikipedia.org/wiki/Set_theory>`_: we call such logical foundations `"type theories" - <https://en.wikipedia.org/wiki/Type_theory>`_. |Coq| is based on + <https://en.wikipedia.org/wiki/Type_theory>`_. Coq is based on the Calculus of Inductive Constructions, which is a particular instance of type theory. sentence - |Coq| documents are made of a series of sentences that contain + Coq documents are made of a series of sentences that contain :term:`commands <command>` or :term:`tactics <tactic>`, generally terminated with a period and optionally decorated with :term:`attributes <attribute>`. @@ -315,7 +315,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types command - A :production:`command` can be used to modify the state of a |Coq| + A :production:`command` can be used to modify the state of a Coq document, for instance by declaring a new object, or to get information about the current state. @@ -334,7 +334,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types Tactics specify how to transform the current proof state as a step in creating a proof. They are syntactically valid only when - |Coq| is in proof mode, such as after a :cmd:`Theorem` command + Coq is in proof mode, such as after a :cmd:`Theorem` command and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more on proof mode. @@ -346,10 +346,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types Settings -------- -There are several mechanisms for changing the behavior of |Coq|. The +There are several mechanisms for changing the behavior of Coq. The :term:`attribute` mechanism is used to modify the behavior of a single :term:`sentence`. The :term:`flag`, :term:`option` and :term:`table` -mechanisms are used to modify the behavior of |Coq| more globally in a +mechanisms are used to modify the behavior of Coq more globally in a document or project. .. _attributes: @@ -420,7 +420,7 @@ boldface label "Attribute:". Attributes are listed in the Flags, Options and Tables ~~~~~~~~~~~~~~~~~~~~~~~~~ -The following types of settings can be used to change the behavior of |Coq| in +The following types of settings can be used to change the behavior of Coq in subsequent commands and tactics (see :ref:`set_unset_scope_qualifiers` for a more precise description of the scope of these settings): @@ -463,10 +463,10 @@ they appear after a boldface label. They are listed in the This warning message can be raised by :cmd:`Set` and :cmd:`Unset` when :n:`@setting_name` is unknown. It is a warning rather than an error because this helps library authors - produce |Coq| code that is compatible with several |Coq| versions. + produce Coq code that is compatible with several Coq versions. To preserve the same behavior, they may need to set some compatibility flags or options that did not exist in previous - |Coq| versions. + Coq versions. .. cmd:: Unset @setting_name :name: Unset diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 2e5dff42ac..3e2ecdc0f0 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -76,7 +76,7 @@ propositional η-equality, which itself would require full η-conversion for subject reduction to hold, but full η-conversion is not acceptable as it would make type checking undecidable. -Since the introduction of primitive records in |Coq| 8.5, an alternative +Since the introduction of primitive records in Coq 8.5, an alternative presentation is available, called *negative co-inductive types*. This consists in defining a co-inductive type as a primitive record type through its projections. Such a technique is akin to the *co-pattern* style that can be @@ -115,7 +115,7 @@ equality: Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. -As of |Coq| 8.9, it is now advised to use negative co-inductive types rather than +As of Coq 8.9, it is now advised to use negative co-inductive types rather than their positive counterparts. .. seealso:: @@ -195,7 +195,7 @@ Top-level definitions of co-recursive functions As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously defining several mutual cofixpoints. - If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 6b031cfea3..7395b12339 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -85,7 +85,7 @@ reduction is called δ-reduction and shows as follows. ζ-reduction ~~~~~~~~~~~ -|Coq| allows also to remove local definitions occurring in terms by +Coq allows also to remove local definitions occurring in terms by replacing the defined variable by its value. The declaration being destroyed, this reduction differs from δ-reduction. It is called ζ-reduction and shows as follows. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 1681eee6e7..4ea3ea5e6d 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -135,7 +135,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: | Proposition | Property - After the statement is asserted, |Coq| needs a proof. Once a proof of + After the statement is asserted, Coq needs a proof. Once a proof of :n:`@type` under the assumptions represented by :n:`@binder`\s is given and validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and the theorem is bound to the name :n:`@ident` in the environment. @@ -176,7 +176,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn the :flag:`Nested Proofs Allowed` flag on. -Proofs start with the keyword :cmd:`Proof`. Then |Coq| enters the proof editing mode +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode until the proof is completed. In proof editing mode, the user primarily enters tactics, which are described in chapter :ref:`Tactics`. The user may also enter commands to manage the proof editing mode. They are described in Chapter diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index c7b1df28db..de780db267 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -4,7 +4,7 @@ Core language ============= -At the heart of the |Coq| proof assistant is the |Coq| kernel. While +At the heart of the Coq proof assistant is the Coq kernel. While users have access to a language with many convenient features such as :ref:`notations <syntax-extensions-and-notation-scopes>`, :ref:`implicit arguments <ImplicitArguments>`, etc. (presented in the diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 1642482bb1..d3bd787587 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -17,7 +17,7 @@ Inductive types constructor ::= @ident {* @binder } {? @of_type } This command defines one or more - inductive types and its constructors. |Coq| generates destructors + inductive types and its constructors. Coq generates destructors depending on the universe that the inductive type belongs to. The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, @@ -411,7 +411,7 @@ constructions. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -552,7 +552,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \end{array} \right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in reset @@ -573,7 +573,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \consf &:& \tree → \forest → \forest\\ \end{array}\right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in @@ -596,7 +596,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \oddS &:& ∀ n,~\even~n → \odd~(\nS~n) \end{array}\right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in @@ -1099,7 +1099,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or template polymorphic, even if the :flag:`Auto Template Polymorphism` flag is on. -In practice, the rule **Ind-Family** is used by |Coq| only when all the +In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over the parameters whose type is an arity of sort in the Type hierarchy. @@ -1237,7 +1237,7 @@ at the computational level it implements a generic operator for doing primitive recursion over the structure. But this operator is rather tedious to implement and use. We choose in -this version of |Coq| to factorize the operator for primitive recursion +this version of Coq to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. Coquand in :cite:`Coq92`. One is the definition by pattern matching. The second one is a definition by guarded fixpoints. @@ -1252,7 +1252,7 @@ The basic idea of this operator is that we have an object :math:`m` in an inductive type :math:`I` and we want to prove a property which possibly depends on :math:`m`. For this, it is enough to prove the property for :math:`m = (c_i~u_1 … u_{p_i} )` for each constructor of :math:`I`. -The |Coq| term for this proof +The Coq term for this proof will be written: .. math:: @@ -1267,7 +1267,7 @@ Actually, for type checking a :math:`\Match…\with…\kwend` expression we also to know the predicate :math:`P` to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` -(parameters excluded), and the last one corresponds to object :math:`m`. |Coq| +(parameters excluded), and the last one corresponds to object :math:`m`. Coq can sometimes infer this predicate but sometimes not. The concrete syntax for describing this predicate uses the :math:`\as…\In…\return` construction. For instance, let us assume that :math:`I` is an unary predicate diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 1309a47ff4..54252689e1 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -864,17 +864,17 @@ Libraries and qualified names Names of libraries ~~~~~~~~~~~~~~~~~~ -The theories developed in |Coq| are stored in *library files* which are +The theories developed in Coq are stored in *library files* which are hierarchically classified into *libraries* and *sublibraries*. To express this hierarchy, library names are represented by qualified identifiers qualid, i.e. as list of identifiers separated by dots (see :ref:`qualified-names`). For instance, the library file ``Mult`` of the standard -|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts +Coq library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts the name of a library is called a *library root*. All library files of -the standard library of |Coq| have the reserved root |Coq| but library -filenames based on other roots can be obtained by using |Coq| commands +the standard library of Coq have the reserved root Coq but library +filenames based on other roots can be obtained by using Coq commands (coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`). -Also, when an interactive |Coq| session starts, a library of root ``Top`` is +Also, when an interactive Coq session starts, a library of root ``Top`` is started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`). .. _qualified-names: @@ -897,7 +897,7 @@ followed by the sequence of submodules names encapsulating the construction and ended by the proper name of the construction. Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’ equality defined in the module Logic in the sublibrary ``Init`` of the -standard library of |Coq|. +standard library of Coq. The proper name that ends the name of a construction is the short name (or sometimes base name) of the construction (for instance, the short @@ -906,7 +906,7 @@ name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a construction is its shortest partially qualified name. -|Coq| does not accept two constructions (definition, theorem, …) with +Coq does not accept two constructions (definition, theorem, …) with the same absolute name but different constructions can have the same short name (or even same partially qualified names as soon as the full names are different). @@ -916,14 +916,14 @@ names also applies to library filenames. **Visibility** -|Coq| maintains a table called the name table which maps partially qualified +Coq maintains a table called the name table which maps partially qualified names of constructions to absolute names. This table is updated by the commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and also each time a new declaration is added to the context. An absolute name is called visible from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in -|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with +Coq name table. Definitions with the :attr:`local` attribute are only accessible with their fully qualified name (see :ref:`gallina-definitions`). It may happen that a visible name is hidden by the short name or a @@ -953,13 +953,13 @@ accessible, absolute names can never be hidden. Libraries and filesystem ~~~~~~~~~~~~~~~~~~~~~~~~ -.. note:: The questions described here have been subject to redesign in |Coq| 8.5. - Former versions of |Coq| use the same terminology to describe slightly different things. +.. note:: The questions described here have been subject to redesign in Coq 8.5. + Former versions of Coq use the same terminology to describe slightly different things. Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer -to them inside |Coq|, a translation from file-system names to |Coq| names +to them inside Coq, a translation from file-system names to Coq names is needed. In this translation, names in the file system are called -*physical* paths while |Coq| names are contrastingly called *logical* +*physical* paths while Coq names are contrastingly called *logical* names. A logical prefix Lib can be associated with a physical path using @@ -967,7 +967,7 @@ the command line option ``-Q`` `path` ``Lib``. All subfolders of path are recursively associated to the logical path ``Lib`` extended with the corresponding suffix coming from the physical path. For instance, the folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding -to invalid |Coq| identifiers are skipped, and, by convention, +to invalid Coq identifiers are skipped, and, by convention, subdirectories named ``CVS`` or ``_darcs`` are skipped too. Thanks to this mechanism, ``.vo`` files are made available through the @@ -979,7 +979,7 @@ its logical name, so that an error is issued if it is loaded with the wrong loadpath afterwards. Some folders have a special status and are automatically put in the -path. |Coq| commands associate automatically a logical path to files in +path. Coq commands associate automatically a logical path to files in the repository trees rooted at the directory from where the command is launched, ``coqlib/user-contrib/``, the directories listed in the ``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/`` @@ -1001,12 +1001,12 @@ of the ``Require`` command can be used to bypass the implicit shortening by providing an absolute root to the required file (see :ref:`compiled-files`). There also exists another independent loadpath mechanism attached to -|OCaml| object files (``.cmo`` or ``.cmxs``) rather than |Coq| object -files as described above. The |OCaml| loadpath is managed using -the option ``-I`` `path` (in the |OCaml| world, there is neither a +OCaml object files (``.cmo`` or ``.cmxs``) rather than Coq object +files as described above. The OCaml loadpath is managed using +the option ``-I`` `path` (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in subdirectories of path). See the command :cmd:`Declare ML Module` in -:ref:`compiled-files` to understand the need of the |OCaml| loadpath. +:ref:`compiled-files` to understand the need of the OCaml loadpath. -See :ref:`command-line-options` for a more general view over the |Coq| command +See :ref:`command-line-options` for a more general view over the Coq command line options. diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 17f569ca2a..4505fc4b4d 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -45,13 +45,13 @@ applications of these primitive operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` -module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types -and functions of a :g:`Uint63` module. That |OCaml| module is not produced by +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. That OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of |Coq|. +can be taken from the kernel of Coq. -Literal values (at type :g:`Int63.int`) are extracted to literal |OCaml| values +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function :g:`Uint63.compile` from the kernel). @@ -94,13 +94,13 @@ to comply with the IEEE 754 standard for floating-point arithmetic. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` -module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types -and functions of a :g:`Float64` module. Said |OCaml| module is not produced by +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Float64` module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of |Coq|. +can be taken from the kernel of Coq. -Literal values (of type :g:`Float64.t`) are extracted to literal |OCaml| +Literal values (of type :g:`Float64.t`) are extracted to literal OCaml values (of type :g:`float`) written in hexadecimal notation and wrapped into the :g:`Float64.of_float` constructor, e.g.: :g:`Float64.of_float (0x1p+0)`. @@ -144,19 +144,19 @@ operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray` -module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types -and functions of a :g:`Parray` module. Said |OCaml| module is not produced by +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Parray` module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of |Coq| (see ``kernel/parray.ml``). +can be taken from the kernel of Coq (see ``kernel/parray.ml``). -|Coq|'s primitive arrays are persistent data structures. Semantically, a set operation +Coq's primitive arrays are persistent data structures. Semantically, a set operation ``t.[i <- a]`` represents a new array that has the same values as ``t``, except at position ``i`` where its value is ``a``. The array ``t`` still exists, can still be used and its values were not modified. Operationally, the implementation -of |Coq|'s primitive arrays is optimized so that the new array ``t.[i <- a]`` does not +of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`. -In short, the implementation keeps one version of ``t`` as an |OCaml| native array and +In short, the implementation keeps one version of ``t`` as an OCaml native array and other versions as lists of modifications to ``t``. Accesses to the native array version are constant time operations. However, accesses to versions where all the cells of the array are modified have O(n) access time, the same as a list. The version that is kept as the native array diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index c70f7a347b..df50dbafe3 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -84,7 +84,7 @@ Sections create local contexts which can be shared across multiple definitions. will be wrapped with a :n:`@term_let` with the same declaration. As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. + if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index f8c0e23696..2460461ede 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -182,7 +182,7 @@ Manual declaration of implicit arguments Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - The ":n:`default implicits`" :token:`args_modifier` clause tells |Coq| to automatically determine the + The ":n:`default implicits`" :token:`args_modifier` clause tells Coq to automatically determine the implicit arguments of the object. Auto-detection is governed by flags specifying whether strict, @@ -378,7 +378,7 @@ Effects of :cmd:`Arguments` on unfolding Bidirectionality hints ~~~~~~~~~~~~~~~~~~~~~~ -When type-checking an application, |Coq| normally does not use information from +When type-checking an application, Coq normally does not use information from the context to infer the types of the arguments. It only checks after the fact that the type inferred for the application is coherent with the expected type. Bidirectionality hints make it possible to specify that after type-checking the @@ -395,7 +395,7 @@ the context to help inferring the types of the remaining arguments. * *type inference*, with is inferring the type of a construct by analyzing the construct. Methods that combine these approaches are known as *bidirectional typing*. - |Coq| normally uses only the first approach to infer the types of arguments, + Coq normally uses only the first approach to infer the types of arguments, then later verifies that the inferred type is consistent with the expected type. *Bidirectionality hints* specify to use both methods: after type checking the first arguments of an application (appearing before the `&` in :cmd:`Arguments`), @@ -417,7 +417,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Definition b2n (b : bool) := if b then 1 else 0. Coercion b2n : bool >-> nat. - |Coq| cannot automatically coerce existential statements over ``bool`` to + Coq cannot automatically coerce existential statements over ``bool`` to statements over ``nat``, because the need for inserting a coercion is known only from the expected type of a subterm: @@ -432,7 +432,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). -|Coq| will attempt to produce a term which uses the arguments you +Coq will attempt to produce a term which uses the arguments you provided, but in some cases involving Program mode the arguments after the bidirectionality starts may be replaced by convertible but syntactically different terms. diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index 38c9fa336d..48120503af 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -159,7 +159,7 @@ of the terms that are compared. End theory. End EQ. -We use |Coq| modules as namespaces. This allows us to follow the same +We use Coq modules as namespaces. This allows us to follow the same pattern and naming convention for the rest of the chapter. The base namespace contains the definitions of the algebraic structure. To keep the example small, the algebraic structure ``EQ.type`` we are @@ -196,7 +196,7 @@ We amend that by equipping ``nat`` with a comparison relation. Check 3 == 3. Eval compute in 3 == 4. -This last test shows that |Coq| is now not only able to type check ``3 == 3``, +This last test shows that Coq is now not only able to type check ``3 == 3``, but also that the infix relation was bound to the ``nat_eq`` relation. This relation is selected whenever ``==`` is used on terms of type nat. This can be read in the line declaring the canonical structure @@ -223,8 +223,8 @@ example work: Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). -The error message is telling that |Coq| has no idea on how to compare -pairs of objects. The following construction is telling |Coq| exactly +The error message is telling that Coq has no idea on how to compare +pairs of objects. The following construction is telling Coq exactly how to do that. .. coqtop:: all @@ -241,7 +241,7 @@ how to do that. Check forall n m : nat, (3, 4) == (n, m). -Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison +Thanks to the ``pair_EQty`` declaration, Coq is able to build a comparison relation for pairs whenever it is able to build a comparison relation for each component of the pair. The declaration associates to the key ``*`` (the type constructor of pairs) the canonical comparison @@ -290,7 +290,7 @@ As before we register a canonical ``LE`` class for ``nat``. Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. -And we enable |Coq| to relate pair of terms with ``<=``. +And we enable Coq to relate pair of terms with ``<=``. .. coqtop:: all @@ -355,10 +355,10 @@ theory of this new class. The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by -a subclass relation. In other words |Coq| does not see that an object of +a subclass relation. In other words Coq does not see that an object of the ``LEQ`` class is also an object of the ``LE`` class. -The following two constructions tell |Coq| how to canonically build the +The following two constructions tell Coq how to canonically build the ``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same type. @@ -413,7 +413,7 @@ setting to any concrete instate of the algebraic structure. Abort. -Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and +Again one has to tell Coq that the type ``nat`` is in the ``LEQ`` class, and how the type constructor ``*`` interacts with the ``LEQ`` class. In the following proofs are omitted for brevity. @@ -468,7 +468,7 @@ Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by the user for ``n`` and m of type ``nat * nat``. What the user provides is a proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the pair constructor preserves this property. The combination of these two -facts is a simple form of proof search that |Coq| performs automatically +facts is a simple form of proof search that Coq performs automatically while inferring canonical structures. Compact declaration of Canonical Structures @@ -507,7 +507,7 @@ instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be read as: “find a class e such that its objects have type T or fail with message "T is not an EQ.type"”. -The other utilities are used to ask |Coq| to solve a specific unification +The other utilities are used to ask Coq to solve a specific unification problem, that will in turn require the inference of some canonical structures. They are explained in more details in :cite:`CSwcu`. @@ -532,7 +532,7 @@ The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers al the other pieces of the class ``LEQ`` and declares them as canonical values associated to the ``T`` key. All in all, the only new piece of information we add in the ``LEQ`` class is the mixin, all the rest is -already canonical for ``T`` and hence can be inferred by |Coq|. +already canonical for ``T`` and hence can be inferred by Coq. ``Pack`` is a notation, hence it is not type checked at the time of its declaration. It will be type checked when it is used, an in that case ``T`` is diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index dc208a63a0..fd9695e270 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -13,7 +13,7 @@ Existential variables | ?[ ?@ident ] | ?@ident {? @%{ {+; @ident := @term } %} } -|Coq| terms can include existential variables that represent unknown +Coq terms can include existential variables that represent unknown subterms that are eventually replaced with actual subterms. Existential variables are generated in place of unsolved implicit @@ -68,7 +68,7 @@ Inferable subterms ~~~~~~~~~~~~~~~~~~ Expressions often contain redundant pieces of information. Subterms that can be -automatically inferred by |Coq| can be replaced by the symbol ``_`` and |Coq| will +automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will guess the missing piece of information. .. extracted from Gallina extensions chapter diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 9457505feb..23ba5f703a 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -115,7 +115,7 @@ application will include that argument. Otherwise, the argument is *non-maximally inserted* and the partial application will not include that argument. Each implicit argument can be declared to be inserted maximally or non -maximally. In |Coq|, maximally inserted implicit arguments are written between curly braces +maximally. In Coq, maximally inserted implicit arguments are written between curly braces "{ }" and non-maximally inserted implicit arguments are written in square brackets "[ ]". .. seealso:: :flag:`Maximal Implicit Insertion` @@ -146,7 +146,7 @@ by replacing it with `_`. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) - |Coq| was not able to deduce an instantiation of a “_”. + Coq was not able to deduce an instantiation of a “_”. .. _declare-implicit-args: @@ -290,8 +290,8 @@ Controlling contextual implicit arguments .. flag:: Contextual Implicit - By default, |Coq| does not automatically set implicit the contextual - implicit arguments. You can turn this flag on to tell |Coq| to also + By default, Coq does not automatically set implicit the contextual + implicit arguments. You can turn this flag on to tell Coq to also infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: @@ -301,8 +301,8 @@ Controlling reversible-pattern implicit arguments .. flag:: Reversible Pattern Implicit - By default, |Coq| does not automatically set implicit the reversible-pattern - implicit arguments. You can turn this flag on to tell |Coq| to also infer + By default, Coq does not automatically set implicit the reversible-pattern + implicit arguments. You can turn this flag on to tell Coq to also infer reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index ea7271179e..ed207ca743 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -4,7 +4,7 @@ Language extensions =================== -Elaboration extends the language accepted by the |Coq| kernel to make it +Elaboration extends the language accepted by the Coq kernel to make it easier to use. For example, this lets the user omit most type annotations because they can be inferred, call functions with implicit arguments which will be inferred as well, extend the syntax with diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 3c1983ee97..23389eba3b 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -5,7 +5,7 @@ Extended pattern matching :Authors: Cristina Cornes and Hugo Herbelin -This section describes the full form of pattern matching in |Coq| terms. +This section describes the full form of pattern matching in Coq terms. .. |rhs| replace:: right hand sides @@ -187,10 +187,10 @@ Printing nested patterns pattern matching into a single pattern matching over a nested pattern. - When this flag is on (default), |Coq|’s printer tries to do such + When this flag is on (default), Coq’s printer tries to do such limited re-factorization. - Turning it off tells |Coq| to print only simple pattern matching problems - in the same way as the |Coq| kernel handles them. + Turning it off tells Coq to print only simple pattern matching problems + in the same way as the Coq kernel handles them. Factorization of clauses with same right-hand side @@ -200,7 +200,7 @@ Factorization of clauses with same right-hand side When several patterns share the same right-hand side, it is additionally possible to share the clauses using disjunctive patterns. Assuming that the - printing matching mode is on, this flag (on by default) tells |Coq|'s + printing matching mode is on, this flag (on by default) tells Coq's printer to try to do this kind of factorization. Use of a default clause @@ -212,7 +212,7 @@ Use of a default clause arguments of the patterns, yet an extra factorization is possible: the disjunction of patterns can be replaced with a `_` default clause. Assuming that the printing matching mode and the factorization mode are on, this flag (on by - default) tells |Coq|'s printer to use a default clause when relevant. + default) tells Coq's printer to use a default clause when relevant. Printing of wildcard patterns ++++++++++++++++++++++++++++++ @@ -234,7 +234,7 @@ Printing of the elimination predicate In most of the cases, the type of the result of a matched term is mechanically synthesizable. Especially, if the result type does not depend of the matched term. When this flag is on (default), - the result type is not printed when |Coq| knows that it can re- + the result type is not printed when Coq knows that it can re- synthesize it. @@ -676,7 +676,7 @@ Dependent pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~ The examples given so far do not need an explicit elimination -predicate because all the |rhs| have the same type and |Coq| +predicate because all the |rhs| have the same type and Coq succeeds to synthesize it. Unfortunately when dealing with dependent patterns it often happens that we need to write cases where the types of the |rhs| are different instances of the elimination predicate. The diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 59e1c65a49..d20a82e6c0 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -1,13 +1,13 @@ .. _thecoqcommands: -The |Coq| commands +The Coq commands ==================== -There are three |Coq| commands: +There are three Coq commands: -+ ``coqtop``: the |Coq| toplevel (interactive mode); -+ ``coqc``: the |Coq| compiler (batch compilation); -+ ``coqchk``: the |Coq| checker (validation of compiled libraries). ++ ``coqtop``: the Coq toplevel (interactive mode); ++ ``coqc``: the Coq compiler (batch compilation); ++ ``coqchk``: the Coq checker (validation of compiled libraries). The options are (basically) the same for the first two commands, and @@ -19,19 +19,19 @@ roughly described below. You can also look at the ``man`` pages of Interactive use (coqtop) ------------------------ -In the interactive mode, also known as the |Coq| toplevel, the user can -develop his theories and proofs step by step. The |Coq| toplevel is run +In the interactive mode, also known as the Coq toplevel, the user can +develop his theories and proofs step by step. The Coq toplevel is run by the command ``coqtop``. -There are two different binary images of |Coq|: the byte-code one and the -native-code one (if |OCaml| provides a native-code compiler for +There are two different binary images of Coq: the byte-code one and the +native-code one (if OCaml provides a native-code compiler for your platform, which is supposed in the following). By default, ``coqtop`` executes the native-code version; run ``coqtop.byte`` to get the byte-code version. -The byte-code toplevel is based on an |OCaml| toplevel (to -allow dynamic linking of tactics). You can switch to the |OCaml| toplevel -with the command ``Drop.``, and come back to the |Coq| +The byte-code toplevel is based on an OCaml toplevel (to +allow dynamic linking of tactics). You can switch to the OCaml toplevel +with the command ``Drop.``, and come back to the Coq toplevel with the command ``Coqloop.loop();;``. .. flag:: Coqtop Exit On Error @@ -48,7 +48,7 @@ vernacular file named *file*.v, and tries to compile it into a .. caution:: - The name *file* should be a regular |Coq| identifier as defined in Section :ref:`lexical-conventions`. + The name *file* should be a regular Coq identifier as defined in Section :ref:`lexical-conventions`. It should contain only letters, digits or underscores (_). For example ``/bar/foo/toto.v`` is valid, but ``/bar/foo/to-to.v`` is not. @@ -59,9 +59,9 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +When Coq is launched, with either ``coqtop`` or ``coqc``, the resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will -be implicitly prepended to any document read by |Coq|, whether it is an +be implicitly prepended to any document read by Coq, whether it is an interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default it's ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If @@ -73,7 +73,7 @@ You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). The resource file may contain, for instance, ``Add LoadPath`` commands to add -directories to the load path of |Coq|. It is possible to skip the +directories to the load path of Coq. It is possible to skip the loading of the resource file with the option ``-q``. .. _customization-by-environment-variables: @@ -82,10 +82,10 @@ By environment variables ~~~~~~~~~~~~~~~~~~~~~~~~~ ``$COQPATH`` can be used to specify the load path. It is a list of directories separated by -``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and +``:`` (``;`` on Windows). Coq will also honor ``$XDG_DATA_HOME`` and ``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`). -Some |Coq| commands call other |Coq| commands. In this case, they look for +Some Coq commands call other Coq commands. In this case, they look for the commands in directory specified by ``$COQBIN``. If this variable is not set, they look for the commands in the executable path. @@ -115,7 +115,7 @@ can be used to specify certain runtime and memory usage parameters. In most cas experimenting with these settings will likely not cause a significant performance difference and should be harmless. -If the variable is not set, |Coq| uses the +If the variable is not set, Coq uses the `default values <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEcontrol>`_, except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 32Mwords (256MB with 64-bit executables or 128MB with 32-bit executables). @@ -133,21 +133,21 @@ The following command-line options are recognized by the commands ``coqc`` and ``coqtop``, unless stated otherwise: :-I *directory*, -include *directory*: Add physical path *directory* - to the |OCaml| loadpath. + to the OCaml loadpath. .. seealso:: :ref:`names-of-libraries` and the command Declare ML Module Section :ref:`compiled-files`. :-Q *directory* *dirpath*: Add physical path *directory* to the list of - directories where |Coq| looks for a file and bind it to the logical + directories where Coq looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is - recursively available from |Coq| using absolute names (extending the + recursively available from Coq using absolute names (extending the :n:`@dirpath` prefix) (see Section :ref:`qualified-names`). Note that only those subdirectories and files which obey the lexical conventions of what is an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive - than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive + than Coq. While Linux’s ext4 file system supports any Coq recursive layout (within the limit of 255 bytes per filename), the default on NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to disallow two files differing only in the case in the same directory. @@ -155,7 +155,7 @@ and ``coqtop``, unless stated otherwise: .. seealso:: Section :ref:`names-of-libraries`. :-R *directory* *dirpath*: Do as ``-Q`` *directory* *dirpath* but make the subdirectory structure of *directory* recursively visible so that the - recursive contents of physical *directory* is available from |Coq| using + recursive contents of physical *directory* is available from Coq using short or partially qualified names. .. seealso:: Section :ref:`names-of-libraries`. @@ -172,12 +172,12 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-l *file*, -load-vernac-source *file*: Load and execute the |Coq| +:-l *file*, -load-vernac-source *file*: Load and execute the Coq script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the - |Coq| script from *file.v*. Write its contents to the standard output as + 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 +:-load-vernac-object *qualid*: Load Coq compiled library :n:`@qualid`. This is equivalent to running :cmd:`Require` :n:`@qualid`. .. _interleave-command-line: @@ -191,27 +191,27 @@ and ``coqtop``, unless stated otherwise: :cmd:`Unset` commands will be executed in the order specified on the command-line. -:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. +:-rfrom *dirpath* *qualid*: Load Coq compiled library :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. +:-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. +:-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`. 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 + 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. + 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 @@ -219,11 +219,11 @@ and ``coqtop``, unless stated otherwise: :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-verbose: Output the content of the input file as it is compiled. This option is available for ``coqc`` only. -:-vos: Indicate |Coq| to skip the processing of opaque proofs +:-vos: Indicate Coq to skip the processing of opaque proofs (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 :cmd:`Require` commands. -:-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead +:-vok: Indicate Coq to check a file completely, to load ``.vos`` files instead 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 @@ -241,7 +241,7 @@ and ``coqtop``, unless stated otherwise: syntax/definitions/notations. :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. -:-impredicative-set: Change the logical theory of |Coq| by declaring the +:-impredicative-set: Change the logical theory of Coq by declaring the sort :g:`Set` impredicative. .. warning:: @@ -249,12 +249,12 @@ and ``coqtop``, unless stated otherwise: This is known to be inconsistent with some standard axioms of classical mathematics such as the functional axiom of choice or the principle of description. -:-type-in-type: Collapse the universe hierarchy of |Coq|. +:-type-in-type: Collapse the universe hierarchy of Coq. .. warning:: This makes the logic inconsistent. :-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace - |Coq|'s auto-generated name scheme with names of the form *ident0*, *ident1*, - etc. Within |Coq|, the :flag:`Mangle Names` flag turns this behavior on, + Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, + etc. Within Coq, the :flag:`Mangle Names` flag turns this behavior on, and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to @@ -264,7 +264,7 @@ and ``coqtop``, unless stated otherwise: 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. + 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. @@ -285,16 +285,16 @@ and ``coqtop``, unless stated otherwise: :-no-glob: Disable the dumping of references for global names. :-image *file*: Set the binary image to be used by ``coqc`` to be *file* instead of the standard one. Not of general use. -:-bindir *directory*: Set the directory containing |Coq| binaries to be +:-bindir *directory*: Set the directory containing Coq binaries to be used by ``coqc``. It is equivalent to doing export COQBIN= *directory* before launching ``coqc``. -:-where: Print the location of |Coq|’s standard library and exit. -:-config: Print the locations of |Coq|’s binaries, dependencies, and +:-where: Print the location of Coq’s standard library and exit. +:-config: Print the locations of Coq’s binaries, dependencies, and libraries, then exit. :-filteropts: Print the list of command line arguments that `coqtop` has recognized as options and exit. -:-v: Print |Coq|’s version and exit. -:-list-tags: Print the highlight tags known by |Coq| as well as their +:-v: Print Coq’s version and exit. +:-list-tags: Print the highlight tags known by Coq as well as their currently associated color and exit. :-h, --help: Print a short usage and exit. @@ -304,7 +304,7 @@ and ``coqtop``, unless stated otherwise: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- -Compiled interfaces help saving time while developing |Coq| formalizations, +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. @@ -401,7 +401,7 @@ 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 + 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``. @@ -412,7 +412,7 @@ When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., withou ``-vos`` nor ``-vok``), an empty file ``foo.vos`` and an empty file ``foo.vok`` are 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 +``-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`` @@ -473,7 +473,7 @@ set of reflexive transitive dependencies of set :math:`S`. Then: context without type checking. Basic integrity checks (checksums) are nonetheless performed. -As a rule of thumb, -admit can be used to tell |Coq| that some libraries +As a rule of thumb, -admit can be used to tell Coq that some libraries have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && ``coqchk B -admit A`` without type checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 64b433115c..c239797cc2 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -2,28 +2,28 @@ .. _coqintegrateddevelopmentenvironment: -|Coq| Integrated Development Environment +Coq Integrated Development Environment ======================================== -The |Coq| Integrated Development Environment is a graphical tool, to be +The Coq Integrated Development Environment is a graphical tool, to be used as a user-friendly replacement to `coqtop`. Its main purpose is to -allow the user to navigate forward and backward into a |Coq| vernacular +allow the user to navigate forward and backward into a Coq vernacular file, executing corresponding commands or undoing them respectively. -|CoqIDE| is run by typing the command `coqide` on the command line. +CoqIDE is run by typing the command `coqide` on the command line. Without argument, the main screen is displayed with an “unnamed buffer”, and with a filename as argument, another buffer displaying the contents of that file. Additionally, `coqide` accepts the same options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously -no meaning for |CoqIDE| being ignored. +no meaning for CoqIDE being ignored. .. _coqide_mainscreen: .. image:: ../_static/coqide.png - :alt: |CoqIDE| main screen + :alt: CoqIDE main screen -A sample |CoqIDE| main screen, while navigating into a file `Fermat.v`, -is shown in the figure :ref:`|CoqIDE| main screen <coqide_mainscreen>`. +A sample CoqIDE main screen, while navigating into a file `Fermat.v`, +is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`. At the top is a menu bar, and a tool bar below it. The large window on the left is displaying the various *script buffers*. The upper right window is the *goal window*, where @@ -39,15 +39,15 @@ The *File* menu allows you to open files or create some, save them, print or export them into various formats. Among all these buffers, there is always one which is the current *running buffer*, whose name is displayed on a background in the *processed* color (green by default), which -is the one where |Coq| commands are currently executed. +is the one where Coq commands are currently executed. Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, …) are available in the *Edit* menu. -|CoqIDE| offers only basic editing commands, so if you need more complex +CoqIDE offers only basic editing commands, so if you need more complex editing commands, you may launch your favorite text editor on the current buffer, using the *Edit/External Editor* menu. -Interactive navigation into |Coq| scripts +Interactive navigation into Coq scripts -------------------------------------------- The running buffer is the one where navigation takes place. The toolbar offers @@ -58,7 +58,7 @@ processed color. If that command fails, the error message is displayed in the message window, and the location of the error is emphasized by an underline in the error foreground color (red by default). -In the figure :ref:`|CoqIDE| main screen <coqide_mainscreen>`, +In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`, the running buffer is `Fermat.v`, all commands until the ``Theorem`` have been already executed, and the user tried to go forward executing ``Induction n``. That command failed because no such @@ -74,7 +74,7 @@ and use the goto button. Unlike with `coqtop`, you should never use There are two additional buttons for navigation within the running buffer. The "down" button with a line goes directly to the end; the "up" button with a line goes back to the beginning. The handling of errors when using the go-to-the-end -button depends on whether |Coq| is running in asynchronous mode or not (see +button depends on whether Coq is running in asynchronous mode or not (see Chapter :ref:`asynchronousandparallelproofprocessing`). If it is not running in that mode, execution stops as soon as an error is found. Otherwise, execution continues, and the error is marked with an underline in the error foreground color, with a @@ -86,12 +86,12 @@ If you ever try to execute a command that runs for a long time and would like to abort it before it terminates, you may use the interrupt button (the white cross on a red circle). -There are other buttons on the |CoqIDE| toolbar: a button to save the running +There are other buttons on the CoqIDE toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "gears" button submits proof terms to the |Coq| kernel for type checking. -When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), +The "gears" button submits proof terms to the Coq kernel for type checking. +When Coq uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. The presence of unchecked proof terms is indicated by ``Qed`` statements that have a subdued *being-processed* color (light blue by default), rather than the @@ -114,11 +114,11 @@ Queries ------------ .. image:: ../_static/coqide-queries.png - :alt: |CoqIDE| queries + :alt: CoqIDE queries We call *query* any vernacular command that does not change the current state, such as ``Check``, ``Search``, etc. To run such commands interactively, without -writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be +writing them in scripts, CoqIDE offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. Queries can also be performed by selecting a particular phrase, then choosing an item from the ``Queries`` menu. The response then appears in the message window. @@ -148,12 +148,12 @@ The first section is for selecting the text font used for scripts, goal and message windows. The second and third sections are for controlling colors and style of -the three main buffers. A predefined |Coq| highlighting style as well +the three main buffers. A predefined Coq highlighting style as well as standard |GtkSourceView| styles are available. Other styles can be added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see the general documentation about |GtkSourceView| for the various possibilities). Note that the style of the rest of graphical part of -|CoqIDE| is not under the control of |GtkSourceView| but of GTK+ and +CoqIDE is not under the control of |GtkSourceView| but of GTK+ and governed by files such as ``settings.ini`` and ``gtk.css`` in ``$XDG_CONFIG_HOME/gtk-3.0`` or files in ``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment @@ -169,7 +169,7 @@ The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a -third party, |CoqIDE| may read it again for you. Note that in the case +third party, CoqIDE may read it again for you. Note that in the case you edited that same file, you will be prompted to choose to either discard your changes or not. The File charset encoding choice is described below in :ref:`character-encoding-saved-files`. @@ -196,9 +196,9 @@ still edit this configuration file by hand, but this is more involved. Using Unicode symbols -------------------------- -|CoqIDE| is based on GTK+ and inherits from it support for Unicode in +CoqIDE is based on GTK+ and inherits from it support for Unicode in its text windows. Consequently a large set of symbols is available for -notations. Furthermore, |CoqIDE| conveniently provides a simple way to +notations. Furthermore, CoqIDE conveniently provides a simple way to input Unicode characters. @@ -219,9 +219,9 @@ mathematical symbols ∀ and ∃, you may define: : type_scope. There exists a small set of such notations already defined, in the -file `utf8.v` of |Coq| library, so you may enable them just by -``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently, -by starting |CoqIDE| with ``coqide -l utf8``. +file `utf8.v` of Coq library, so you may enable them just by +``Require Import Unicode.Utf8`` inside CoqIDE, or equivalently, +by starting CoqIDE with ``coqide -l utf8``. However, there are some issues when using such Unicode symbols: you of course need to use a character font which supports them. In the Fonts @@ -237,7 +237,7 @@ use antialiased fonts or not, by setting the environment variable Bindings for input of Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|CoqIDE| supports a builtin mechanism to input non-ASCII symbols. +CoqIDE supports a builtin mechanism to input non-ASCII symbols. For example, to input ``π``, it suffices to type ``\pi`` then press the combination of key ``Shift+Space`` (default key binding). Often, it suffices to type a prefix of the latex token, e.g. typing ``\p`` @@ -255,7 +255,7 @@ Custom bindings may be added, as explained further on. .. note:: It remains possible to input non-ASCII symbols using system-wide - approaches independent of |CoqIDE|. + approaches independent of CoqIDE. Adding custom bindings @@ -286,7 +286,7 @@ Similarly, the above settings ensure than ``\l`` resolves to ``\le``, and that ``\la`` resolves to ``\lambda``. It can be useful to work with per-project binding files. For this purpose -|CoqIDE| accepts a command line argument of the form +CoqIDE accepts a command line argument of the form ``-unicode-bindings file1,file2,...,fileN``. Each of the file tokens provided may consists of one of: @@ -320,7 +320,7 @@ related to the way files are saved. If you have no need to exchange files with non UTF-8 aware applications, it is better to choose the UTF-8 encoding, since it guarantees that your files will be read again without problems. (This -is because when |CoqIDE| reads a file, it tries to automatically detect +is because when CoqIDE reads a file, it tries to automatically detect its character encoding.) If you choose something else than UTF-8, then missing characters will diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index c3286199e8..ec3689bbbe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -8,7 +8,7 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -Using |Coq| as a library +Using Coq as a library ------------------------ In previous versions, ``coqmktop`` was used to build custom @@ -34,21 +34,21 @@ For example, to statically link |Ltac|, you can just do: and similarly for other plugins. -Building a |Coq| project +Building a Coq project ------------------------ -As of today it is possible to build |Coq| projects using two tools: +As of today it is possible to build Coq projects using two tools: -- coq_makefile, which is distributed by |Coq| and is based on generating a makefile, -- Dune, the standard |OCaml| build tool, which, since version 1.9, supports building |Coq| libraries. +- coq_makefile, which is distributed by Coq and is based on generating a makefile, +- Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries. .. _coq_makefile: -Building a |Coq| project with coq_makefile +Building a Coq project with coq_makefile ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The majority of |Coq| projects are very similar: a collection of ``.v`` -files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of +The majority of Coq projects are very similar: a collection of ``.v`` +files and eventually some ``.ml`` ones (a Coq plugin). The main piece of metadata needed in order to build the project are the command line options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command line options <command-line-options>`). Collecting the list of files @@ -74,11 +74,11 @@ to literally pass an argument ``foo`` to ``coqc``: in the example, this allows to pass the two-word option ``-w all`` (see :ref:`command line options <command-line-options>`). -|CoqIDE|, Proof-General and VSCoq all -understand ``_CoqProject`` files and can be used to invoke |Coq| with the desired options. +CoqIDE, Proof-General and VSCoq all +understand ``_CoqProject`` files and can be used to invoke Coq with the desired options. The ``coq_makefile`` utility can be used to set up a build infrastructure -for the |Coq| project based on makefiles. The recommended way of +for the Coq project based on makefiles. The recommended way of invoking ``coq_makefile`` is the following one: :: @@ -91,14 +91,14 @@ Such command generates the following files: CoqMakefile is a makefile for ``GNU Make`` with targets to build the project (e.g. generate .vo or .html files from .v or compile .ml* files) - and install it in the ``user-contrib`` directory where the |Coq| + and install it in the ``user-contrib`` directory where the Coq library is installed. Run ``make`` with the ``-f CoqMakefile`` option to use ``CoqMakefile``. CoqMakefile.conf contains make variables assignments that reflect the contents of the ``_CoqProject`` file as well as the path relevant to - |Coq|. + Coq. An optional file ``CoqMakefile.local`` can be provided by the user in order to @@ -111,11 +111,11 @@ The extensions of the files listed in ``_CoqProject`` is used in order to 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 ++ 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 ``.mlg`` extension -+ In order to generate a plugin one has to list all |OCaml| ++ 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). @@ -142,23 +142,23 @@ Here we describe only few of them. :CAMLPKGS: can be used to specify third party findlib packages, and is - passed to the |OCaml| compiler on building or linking of modules. Eg: + passed to the OCaml compiler on building or linking of modules. Eg: ``-package yojson``. :CAMLFLAGS: - can be used to specify additional flags to the |OCaml| + can be used to specify additional flags to the OCaml compiler, like ``-bin-annot`` or ``-w``.... :OCAMLWARN: it contains a default of ``-warn-error +a-3``, useful to modify this setting; beware this is not recommended for projects in - |Coq|'s CI. + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) :COQ_SRC_SUBDIRS: can be extended by including other paths in which ``*.cm*`` files are searched. For example ``COQ_SRC_SUBDIRS+=user-contrib/Unicoq`` - lets you build a plugin containing |OCaml| code that depends on the - |OCaml| code of ``Unicoq`` + lets you build a plugin containing OCaml code that depends on the + OCaml code of ``Unicoq`` :COQFLAGS: override the flags passed to ``coqc``. By default ``-q``. :COQEXTRAFLAGS: @@ -172,7 +172,7 @@ Here we describe only few of them. :COQDOCEXTRAFLAGS: extend the flags passed to ``coqdoc`` :COQLIBINSTALL, COQDOCINSTALL: - specify where the |Coq| libraries and documentation will be installed. + specify where the Coq libraries and documentation will be installed. By default a combination of ``$(DESTDIR)`` (if defined) with ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``. @@ -524,7 +524,7 @@ Precompiling for ``native_compute`` +++++++++++++++++++++++++++++++++++ To compile files for ``native_compute``, one can use the -``-native-compiler yes`` option of |Coq|, for instance by putting the +``-native-compiler yes`` option of Coq, for instance by putting the following in a :ref:`coqmakefilelocal` file: :: @@ -555,27 +555,27 @@ of installing the extra ``.coq-native`` directories. This requires all dependencies to be themselves compiled with ``-native-compiler yes``. -Building a |Coq| project with Dune +Building a Coq project with Dune ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. note:: - Dune's |Coq| support is still experimental; we strongly recommend + Dune's Coq support is still experimental; we strongly recommend using Dune 2.3 or later. .. note:: - The canonical documentation for the |Coq| Dune extension is + The canonical documentation for the Coq Dune extension is maintained upstream; please refer to the `Dune manual <https://dune.readthedocs.io/>`_ for up-to-date information. This documentation is up to date for Dune 2.3. -Building a |Coq| project with Dune requires setting up a Dune project +Building a Coq project with Dune requires setting up a Dune project for your files. This involves adding a ``dune-project`` and ``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated by Dune itself), and then providing ``dune`` files in the directories your ``.v`` files are placed. For the experimental version "0.1" of -the |Coq| Dune language, |Coq| library stanzas look like: +the Coq Dune language, Coq library stanzas look like: .. code:: scheme @@ -592,12 +592,12 @@ the library under ``<module_prefix>``. If you declare an ``<opam_package>``, an ``.install`` file for the library will be generated; the optional ``(modules <ordered_set_lang>)`` field allows you to filter the list of modules, and ``(libraries -<ocaml_libraries>)`` allows the |Coq| theory depend on ML plugins. For -the moment, Dune relies on |Coq|'s standard mechanisms (such as -``COQPATH``) to locate installed |Coq| libraries. +<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For +the moment, Dune relies on Coq's standard mechanisms (such as +``COQPATH``) to locate installed Coq libraries. By default Dune will skip ``.v`` files present in subdirectories. In -order to enable the usual recursive organization of |Coq| projects add +order to enable the usual recursive organization of Coq projects add .. code:: scheme @@ -611,7 +611,7 @@ of your project. .. example:: - A typical stanza for a |Coq| plugin is split into two parts. An |OCaml| build directive, which is standard Dune: + A typical stanza for a Coq plugin is split into two parts. An OCaml build directive, which is standard Dune: .. code:: scheme @@ -623,7 +623,7 @@ of your project. (coq.pp (modules g_equations)) - And a |Coq|-specific part that depends on it via the ``libraries`` field: + And a Coq-specific part that depends on it via the ``libraries`` field: .. code:: scheme @@ -642,37 +642,37 @@ Computing Module dependencies ----------------------------- In order to compute module dependencies (to be used by ``make`` or -``dune``), |Coq| provides the ``coqdep`` tool. +``dune``), Coq provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| +``coqdep`` computes inter-module dependencies for Coq programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. -Dependencies of |Coq| modules are computed by looking at ``Require`` +Dependencies of Coq modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the -dependencies among the files part of a |Coq| project. +dependencies among the files part of a Coq project. -Embedded |Coq| phrases inside |Latex| documents +Embedded Coq phrases inside |Latex| documents ----------------------------------------------- When writing documentation about a proof development, one may want -to insert |Coq| phrases inside a |Latex| document, possibly together +to insert Coq phrases inside a |Latex| document, possibly together with the corresponding answers of the system. We provide a mechanical -way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex`` -filter. This filter extracts |Coq| phrases embedded in |Latex| files, +way to process such Coq phrases embedded in |Latex| files: the ``coq-tex`` +filter. This filter extracts Coq phrases embedded in |Latex| files, evaluates them, and insert the outcome of the evaluation after each phrase. -Starting with a file ``file.tex`` containing |Coq| phrases, the ``coq-tex`` -filter produces a file named ``file.v.tex`` with the |Coq| outcome. +Starting with a file ``file.tex`` containing Coq phrases, the ``coq-tex`` +filter produces a file named ``file.v.tex`` with the Coq outcome. -There are options to produce the |Coq| parts in smaller font, italic, +There are options to produce the Coq parts in smaller font, italic, between horizontal rules, etc. See the man page of ``coq-tex`` for more details. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 8663ac646b..1cb83465b6 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|. We start by giving the syntax followed by the informal semantics. To learn more about the language and especially about its foundations, please refer to :cite:`Del00`. -(Note the examples in the paper won't work as-is; |Coq| has evolved +(Note the examples in the paper won't work as-is; Coq has evolved since the paper was written.) .. example:: Basic tactic macros @@ -41,7 +41,7 @@ higher precedence than `+`. Usually `a/b/c` is given the :gdef:`left associativ interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation `a/(b/c)`. -In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` +In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4` because `||` is part of :token:`ltac_expr2`, which has higher precedence than :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which @@ -784,7 +784,7 @@ single success: Checking for a single success: exactly_once ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| provides an experimental way to check that a tactic has *exactly +Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 @@ -813,7 +813,7 @@ one* success: Checking for failure: assert_fails ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 :name: assert_fails @@ -859,7 +859,7 @@ Checking for failure: assert_fails Checking for success: assert_succeeds ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @ltac_expr3 @@ -905,7 +905,7 @@ Failing See the example for a comparison of the two constructs. - Note that if |Coq| terms have to be + Note that if Coq terms have to be printed as part of the failure, term construction always forces the tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed. @@ -990,7 +990,7 @@ amount of time: timeout with some other tacticals. This tactical is hence proposed only for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that - this tactical isn’t available on the native Windows port of |Coq|. + this tactical isn’t available on the native Windows port of Coq. Timing a tactic ~~~~~~~~~~~~~~~ @@ -1523,7 +1523,7 @@ produce subgoals but generates a term to be used in tactic expressions: Generating fresh hypothesis names ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Tactics sometimes need to generate new names for hypothesis. Letting |Coq| +Tactics sometimes need to generate new names for hypothesis. Letting Coq choose a name with the intro tactic is not so good since it is very awkward to retrieve that name. The following expression returns an identifier: @@ -1885,7 +1885,7 @@ Proving that a list is a permutation of a second list From Section :ref:`ltac-syntax` we know that Ltac has a primitive notion of integers, but they are only used as arguments for primitive tactics and we cannot make computations with them. Thus, - instead, we use |Coq|'s natural number type :g:`nat`. + instead, we use Coq's natural number type :g:`nat`. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 41f376c43d..b912bcbdf8 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -4,7 +4,7 @@ Ltac2 ===== The |Ltac| tactic language is probably one of the ingredients of the success of -|Coq|, yet it is at the same time its Achilles' heel. Indeed, |Ltac|: +Coq, yet it is at the same time its Achilles' heel. Indeed, |Ltac|: - has often unclear semantics - is very non-uniform due to organic growth @@ -30,7 +30,7 @@ as Ltac1. Current limitations include: - There are a number of tactics that are not yet supported in Ltac2 because - the interface |OCaml| and/or Ltac2 notations haven't been written. See + the interface OCaml and/or Ltac2 notations haven't been written. See :ref:`defining_tactics`. - Missing usability features such as: @@ -89,7 +89,7 @@ In particular, Ltac2 is: * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of - |Coq|-side terms + Coq-side terms - a language featuring notation facilities to help write palatable scripts We describe these in more detail in the remainder of this document. @@ -107,14 +107,14 @@ that ML constitutes a sweet spot in PL design, as it is relatively expressive while not being either too lax (unlike dynamic typing) nor too strict (unlike, say, dependent types). -The main goal of Ltac2 is to serve as a meta-language for |Coq|. As such, it +The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it naturally fits in the ML lineage, just as the historical ML was designed as the tactic language for the LCF prover. It can also be seen as a general-purpose -language, by simply forgetting about the |Coq|-specific features. +language, by simply forgetting about the Coq-specific features. Sticking to a standard ML type system can be considered somewhat weak for a -meta-language designed to manipulate |Coq| terms. In particular, there is no -way to statically guarantee that a |Coq| term resulting from an Ltac2 +meta-language designed to manipulate Coq terms. In particular, there is no +way to statically guarantee that a Coq term resulting from an Ltac2 computation will be well-typed. This is actually a design choice, motivated by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are @@ -137,7 +137,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to |OCaml|. Types follow the simply-typed syntax of |OCaml|. +close to OCaml. Types follow the simply-typed syntax of OCaml. .. insertprodn ltac2_type ltac2_typevar @@ -159,7 +159,7 @@ declarations such as algebraic datatypes and records. Built-in types include: -- ``int``, machine integers (size not specified, in practice inherited from |OCaml|) +- ``int``, machine integers (size not specified, in practice inherited from OCaml) - ``string``, mutable strings - ``'a array``, mutable arrays - ``exn``, exceptions @@ -200,7 +200,7 @@ One can define new types with the following commands. :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`. Without :n:`{| := | ::= }` - Defines an abstract type for use representing data from |OCaml|. Not for + Defines an abstract type for use representing data from OCaml. Not for end users. :n:`with @tac2typ_def` @@ -226,9 +226,9 @@ One can define new types with the following commands. .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string :name: Ltac2 external - Declares abstract terms. Frequently, these declare |OCaml| functions - defined in |Coq| and give their type information. They can also declare - data structures from |OCaml|. This command has no use for the end user. + Declares abstract terms. Frequently, these declare OCaml functions + defined in Coq and give their type information. They can also declare + data structures from OCaml. This command has no use for the end user. APIs ~~~~ @@ -360,7 +360,7 @@ Reduction ~~~~~~~~~ We use the usual ML call-by-value reduction, with an otherwise unspecified -evaluation order. This is a design choice making it compatible with |OCaml|, +evaluation order. This is a design choice making it compatible with OCaml, if ever we implement native compilation. The expected equations are as follows:: (fun x => t) V ≡ t{x := V} (βv) @@ -404,7 +404,7 @@ standard IO monad as the ambient effectful world, Ltac2 is has a tactic monad. Note that the order of evaluation of application is *not* specified and is -implementation-dependent, as in |OCaml|. +implementation-dependent, as in OCaml. We recall that the `Proofview.tactic` monad is essentially a IO monad together with backtracking state representing the proof state. @@ -535,7 +535,7 @@ is a proper one or referring to something in the Ltac context. Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is not ``foo`` applied to the Ltac integer expression ``0`` (|Ltac| does have a -notion of integers, though it is not first-class), but rather the |Coq| term +notion of integers, though it is not first-class), but rather the Coq term :g:`Datatypes.O`. The implicit parsing is confusing to users and often gives unexpected results. @@ -567,11 +567,11 @@ Built-in quotations The current implementation recognizes the following built-in quotations: - ``ident``, which parses identifiers (type ``Init.ident``). -- ``constr``, which parses |Coq| terms and produces an-evar free term at runtime +- ``constr``, which parses Coq terms and produces an-evar free term at runtime (type ``Init.constr``). -- ``open_constr``, which parses |Coq| terms and produces a term potentially with +- ``open_constr``, which parses Coq terms and produces a term potentially with holes at runtime (type ``Init.constr`` as well). -- ``pattern``, which parses |Coq| patterns and produces a pattern used for term +- ``pattern``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). - ``reference`` Qualified names are globalized at internalization into the corresponding global reference, @@ -614,7 +614,7 @@ Term Antiquotations Syntax ++++++ -One can also insert Ltac2 code into |Coq| terms, similar to what is possible in +One can also insert Ltac2 code into Coq terms, similar to what is possible in Ltac1. .. prodn:: @@ -626,7 +626,7 @@ for their side-effects. Semantics +++++++++ -A quoted |Coq| term is interpreted in two phases, internalization and +A quoted Coq term is interpreted in two phases, internalization and evaluation. - Internalization is part of the static semantics, that is, it is done at Ltac2 @@ -634,17 +634,17 @@ evaluation. - Evaluation is part of the dynamic semantics, that is, it is done when a term gets effectively computed by Ltac2. -Note that typing of |Coq| terms is a *dynamic* process occurring at Ltac2 +Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 evaluation time, and not at Ltac2 typing time. Static semantics **************** -During internalization, |Coq| variables are resolved and antiquotations are -type checked as Ltac2 terms, effectively producing a ``glob_constr`` in |Coq| +During internalization, Coq variables are resolved and antiquotations are +type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq implementation terminology. Note that although it went through the type checking of **Ltac2**, the resulting term has not been fully computed and -is potentially ill-typed as a runtime **|Coq|** term. +is potentially ill-typed as a runtime **Coq** term. .. example:: @@ -666,7 +666,7 @@ of the corresponding term expression. let x := '0 in constr:(1 + ltac2:(exact x)) Beware that the typing environment of antiquotations is **not** -expanded by the |Coq| binders from the term. +expanded by the Coq binders from the term. .. example:: @@ -689,17 +689,17 @@ as follows. `constr:(fun x : nat => ltac2:(exact (hyp @x)))` -This pattern is so common that we provide dedicated Ltac2 and |Coq| term notations +This pattern is so common that we provide dedicated Ltac2 and Coq term notations for it. - `&x` as an Ltac2 expression expands to `hyp @x`. -- `&x` as a |Coq| constr expression expands to +- `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. -In the special case where Ltac2 antiquotations appear inside a |Coq| term +In the special case where Ltac2 antiquotations appear inside a Coq term notation, the notation variables are systematically bound in the body of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents -untyped syntactic |Coq| expressions, which can by typed in the +untyped syntactic Coq expressions, which can by typed in the current context using the `Ltac2.Constr.pretype` function. .. example:: @@ -745,9 +745,9 @@ the notation section. .. prodn:: term += $@lident -In a |Coq| term, writing :g:`$x` is semantically equivalent to +In a Coq term, writing :g:`$x` is semantically equivalent to :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to -insert in a concise way an Ltac2 variable of type :n:`constr` into a |Coq| term. +insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. Match over terms ~~~~~~~~~~~~~~~~ @@ -1126,7 +1126,7 @@ Match on values .. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end :name: match (Ltac2) - Matches a value, akin to the |OCaml| `match` construct. By itself, it doesn't cause backtracking + Matches a value, akin to the OCaml `match` construct. By itself, it doesn't cause backtracking as do the `*match*!` and `*match*! goal` constructs. .. insertprodn ltac2_branches atomic_tac2pat @@ -1186,7 +1186,7 @@ Notations into the right-hand side. The right-hand side is typechecked when the notation is used, not when it is defined. In the following example, `x` is the formal parameter name and `constr` is its :ref:`syntactic class<syntactic_classes>`. `print` and `of_constr` are - functions provided by |Coq| through `Message.v`. + functions provided by Coq through `Message.v`. .. todo "print" doesn't seem to pay attention to "Set Printing All" @@ -1258,7 +1258,7 @@ Abbreviations Introduces a special kind of notation, called an abbreviation, that does not add any parsing rules. It is similar in - spirit to |Coq| abbreviations (see :cmd:`Notation (abbreviation)`, + spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`, insofar as its main purpose is to give an absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. @@ -1285,7 +1285,7 @@ Abbreviations Defining tactics ~~~~~~~~~~~~~~~~ -Built-in tactics (those defined in |OCaml| code in the |Coq| executable) and Ltac1 tactics, +Built-in tactics (those defined in OCaml code in the Coq executable) and Ltac1 tactics, which are defined in `.v` files, must be defined through notations. (Ltac2 tactics can be defined with :cmd:`Ltac2`. @@ -1293,7 +1293,7 @@ Notations for many but not all built-in tactics are defined in `Notations.v`, wh loaded with Ltac2. The Ltac2 syntax for these tactics is often identical or very similar to the tactic syntax described in other chapters of this documentation. These notations rely on tactic functions declared in `Std.v`. Functions corresponding to some built-in tactics may not yet be defined in the -|Coq| executable or declared in `Std.v`. Adding them may require code changes to |Coq| or defining +Coq executable or declared in `Std.v`. Adding them may require code changes to Coq or defining workarounds through Ltac1 (described below). Two examples of syntax differences: @@ -1325,7 +1325,7 @@ Syntactic classes ~~~~~~~~~~~~~~~~~ The simplest syntactic classes in Ltac2 notations represent individual nonterminals -from the |Coq| grammar. Only a few selected nonterminals are available as syntactic classes. +from the Coq grammar. Only a few selected nonterminals are available as syntactic classes. In addition, there are metasyntactic operations for describing more complex syntax, such as making an item optional or representing a list of items. When parsing, each syntactic class expression returns a value that's bound to a name in the @@ -1799,7 +1799,7 @@ Transition from Ltac1 Owing to the use of a lot of notations, the transition should not be too difficult. In particular, it should be possible to do it incrementally. That said, we do *not* guarantee it will be a blissful walk either. -Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with |Coq| +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq will help you. We list the major changes and the transition strategies hereafter. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index cdbae8ade1..22544b2018 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -13,12 +13,12 @@ Introduction This chapter describes a set of tactics known as |SSR| originally designed to provide support for the so-called *small scale reflection* proof methodology. Despite the original purpose this set of tactic is -of general interest and is available in |Coq| starting from version 8.7. +of general interest and is available in Coq starting from version 8.7. |SSR| was developed independently of the tactics described in Chapter :ref:`tactics`. Indeed the scope of the tactics part of |SSR| largely overlaps with the standard set of tactics. Eventually the overlap will -be reduced in future releases of |Coq|. +be reduced in future releases of Coq. Proofs written in |SSR| typically look quite different from the ones written using only tactics as per Chapter :ref:`tactics`. We try to @@ -112,7 +112,7 @@ Compatibility issues ~~~~~~~~~~~~~~~~~~~~ Requiring the above modules creates an environment which is mostly -compatible with the rest of |Coq|, up to a few discrepancies: +compatible with the rest of Coq, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or @@ -124,11 +124,11 @@ compatible with the rest of |Coq|, up to a few discrepancies: + Identifiers with both leading and trailing ``_``, such as ``_x_``, are reserved by |SSR| and cannot appear in scripts. + The extensions to the :tacn:`rewrite` tactic are partly incompatible with those - available in current versions of |Coq|; in particular: ``rewrite .. in + available in current versions of Coq; in particular: ``rewrite .. in (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` will not work, and the |SSR| syntax and semantics for occurrence selection and rule chaining is different. Use an explicit rewrite direction - (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic. + (``rewrite <- …`` or ``rewrite -> …``) to access the Coq rewrite tactic. + New symbols (``//``, ``/=``, ``//=``) might clash with adjacent existing symbols. This can be avoided by inserting white spaces. @@ -158,34 +158,34 @@ compatible with the rest of |Coq|, up to a few discrepancies: generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. + The following flags can be unset to make |SSR| more compatible with - parts of |Coq|: + parts of Coq: .. flag:: SsrRewrite Controls whether the incompatible rewrite syntax is enabled (the default). - Disabling the flag makes the syntax compatible with other parts of |Coq|. + Disabling the flag makes the syntax compatible with other parts of Coq. .. flag:: SsrIdents Controls whether tactics can refer to |SSR|-generated variables that are in the form _xxx_. Scripts with explicit references to such variables are fragile; they are prone to failure if the proof is later modified or - if the details of variable name generation change in future releases of |Coq|. + if the details of variable name generation change in future releases of Coq. The default is on, which gives an error message when the user tries to create such identifiers. Disabling the flag generates a warning instead, - increasing compatibility with other parts of |Coq|. + increasing compatibility with other parts of Coq. -|Gallina| extensions +Gallina extensions -------------------- Small-scale reflection makes an extensive use of the programming -subset of |Gallina|, |Coq|’s logical specification language. This subset +subset of Gallina, Coq’s logical specification language. This subset is quite suited to the description of functions on representations, because it closely follows the well-established design of the ML programming language. The |SSR| extension provides three additions -to |Gallina|, for pattern assignment, pattern testing, and polymorphism; -these mitigate minor but annoying discrepancies between |Gallina| and +to Gallina, for pattern assignment, pattern testing, and polymorphism; +these mitigate minor but annoying discrepancies between Gallina and ML. @@ -199,7 +199,7 @@ irrefutable pattern matching, that is, destructuring assignment: term += let: @pattern := @term in @term Note the colon ``:`` after the ``let`` keyword, which avoids any ambiguity -with a function definition or |Coq|’s basic destructuring let. The let: +with a function definition or Coq’s basic destructuring let. The let: construct differs from the latter in that @@ -237,7 +237,7 @@ construct differs from the latter in that The ``let:`` construct is just (more legible) notation for the primitive -|Gallina| expression :n:`match @term with @pattern => @term end`. +Gallina expression :n:`match @term with @pattern => @term end`. The |SSR| destructuring assignment supports all the dependent match annotations; the full syntax is @@ -294,10 +294,10 @@ example, the null and all list function(al)s can be defined as follows: The pattern conditional also provides a notation for destructuring assignment with a refutable pattern, adapted to the pure functional -setting of |Gallina|, which lacks a ``Match_Failure`` exception. +setting of Gallina, which lacks a ``Match_Failure`` exception. Like ``let:`` above, the ``if…is`` construct is just (more legible) notation -for the primitive |Gallina| expression +for the primitive Gallina expression :n:`match @term with @pattern => @term | _ => @term end`. Similarly, it will always be displayed as the expansion of this form @@ -355,15 +355,15 @@ Note that :token:`pattern` eventually binds variables in the third Parametric polymorphism ~~~~~~~~~~~~~~~~~~~~~~~ -Unlike ML, polymorphism in core |Gallina| is explicit: the type +Unlike ML, polymorphism in core Gallina is explicit: the type parameters of polymorphic functions must be declared explicitly, and -supplied at each point of use. However, |Coq| provides two features to +supplied at each point of use. However, Coq provides two features to suppress redundant parameters: + Sections are used to provide (possibly implicit) parameters for a set of definitions. -+ Implicit arguments declarations are used to tell |Coq| to use type ++ Implicit arguments declarations are used to tell Coq to use type inference to deduce some parameters from the context at each point of call. @@ -392,11 +392,11 @@ expressions such as Definition all_null (s : list T) := all (@null T) s. Unfortunately, such higher-order expressions are quite frequent in -representation functions, especially those which use |Coq|'s +representation functions, especially those which use Coq's ``Structures`` to emulate Haskell typeclasses. -Therefore, |SSR| provides a variant of |Coq|’s implicit argument -declaration, which causes |Coq| to fill in some implicit parameters at +Therefore, |SSR| provides a variant of Coq’s implicit argument +declaration, which causes Coq to fill in some implicit parameters at each point of use, e.g., the above definition can be written: .. example:: @@ -432,7 +432,7 @@ The syntax of the new declaration is As these prenex implicit arguments are ubiquitous and have often large display strings, it is strongly recommended to change the default - display settings of |Coq| so that they are not printed (except after + display settings of Coq so that they are not printed (except after a ``Set Printing All`` command). All |SSR| library files thus start with the incantation @@ -957,7 +957,7 @@ context. This is essential in the context of an interactive development environment (IDE), because it facilitates navigating the proof, allowing to instantly "jump back" to the point at which a questionable assumption was added, and to find relevant assumptions by -browsing the pruned context. While novice or casual |Coq| users may find +browsing the pruned context. While novice or casual Coq users may find the automatic name selection feature convenient, the usage of such a feature severely undermines the readability and maintainability of proof scripts, much like automatic variable declaration in programming @@ -973,7 +973,7 @@ the foundation of the |SSR| proof language. Bookkeeping ~~~~~~~~~~~ -During the course of a proof |Coq| always present the user with a +During the course of a proof Coq always present the user with a *sequent* whose general form is:: ci : Ti @@ -1015,7 +1015,7 @@ are *ordered*, but *unnamed*: the display names of variables may change at any time because of α-conversion. Similarly, basic deductive steps such as apply can only operate on the -goal because the |Gallina| terms that control their action (e.g., the +goal because the Gallina terms that control their action (e.g., the type of the lemma used by ``apply``) only provide unnamed bound variables. [#2]_ Since the proof script can only refer directly to the context, it must constantly shift declarations from the goal to the context and @@ -1083,7 +1083,7 @@ simultaneously renames ``m`` and ``le_m_n`` into ``p`` and ``le_n_p``, respectively, by first turning them into unnamed variables, then turning these variables back into constants and facts. -Furthermore, |SSR| redefines the basic |Coq| tactics ``case``, ``elim``, +Furthermore, |SSR| redefines the basic Coq tactics ``case``, ``elim``, and ``apply`` so that they can take better advantage of ``:`` and ``=>``. In there |SSR| variants, these tactic operate on the first variable or @@ -1421,7 +1421,7 @@ Therefore this tactic changes any goal ``G`` into forall n n0 : nat, n = n0 -> G. -where the name ``n0`` is picked by the |Coq| display function, and assuming +where the name ``n0`` is picked by the Coq display function, and assuming ``n`` appeared only in ``G``. Finally, note that a discharge operation generalizes defined constants @@ -1927,7 +1927,7 @@ When the top assumption of a goal has an inductive type, two specific operations are possible: the case analysis performed by the :tacn:`case` tactic, and the application of an induction principle, performed by the :tacn:`elim` tactic. When this top assumption has an inductive type, which -is moreover an instance of a type family, |Coq| may need help from the +is moreover an instance of a type family, Coq may need help from the user to specify which occurrences of the parameters of the type should be substituted. @@ -2055,7 +2055,7 @@ Control flow Indentation and bullets ~~~~~~~~~~~~~~~~~~~~~~~ -A linear development of |Coq| scripts gives little information on the +A linear development of Coq scripts gives little information on the structure of the proof. In addition, replaying a proof after some changes in the statement to be proved will usually not display information to distinguish between the various branches of case @@ -3391,7 +3391,7 @@ rewrite operations prescribed by the rules on the current goal. Indeed rule ``eqab`` is the first to apply among the ones gathered in the tuple passed to the rewrite tactic. This multirule - ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a + ``(eqab, eqac)`` is actually a Coq term and we can name it with a definition: .. coqtop:: all @@ -3529,11 +3529,11 @@ Anyway this tactic is *not* equivalent to lemma that was used, while the latter requires you prove the quantified form. -When |SSR| rewrite fails on standard |Coq| licit rewrite +When |SSR| rewrite fails on standard Coq licit rewrite ```````````````````````````````````````````````````````` In a few cases, the |SSR| rewrite tactic fails rewriting some -redexes which standard |Coq| successfully rewrites. There are two main +redexes which standard Coq successfully rewrites. There are two main cases: @@ -3550,7 +3550,7 @@ cases: Lemma fubar (x : unit) : (let u := x in u) = tt. -+ The standard rewrite tactic provided by |Coq| uses a different algorithm ++ The standard rewrite tactic provided by Coq uses a different algorithm to find instances of the rewrite rule. .. example:: @@ -3953,7 +3953,7 @@ together with “term tagging” operations. The first one uses auxiliary definitions to introduce a provably equal copy of any term t. However this copy is (on purpose) *not -convertible* to t in the |Coq| system [#8]_. The job is done by the +convertible* to t in the Coq system [#8]_. The job is done by the following construction: .. coqdoc:: @@ -4542,7 +4542,7 @@ is a synonym for: elim x using V; clear x; intro y. where ``x`` is a variable in the context, ``y`` a fresh name and ``V`` -any second order lemma; |SSR| relaxes the syntactic restrictions of the |Coq| +any second order lemma; |SSR| relaxes the syntactic restrictions of the Coq ``elim``. The first pattern following ``:`` can be a ``_`` wildcard if the conclusion of the view ``V`` specifies a pattern for its last argument (e.g., if ``V`` is a functional induction lemma generated by the @@ -4590,7 +4590,7 @@ generation (see section :ref:`generation_of_equations_ssr`). elim/last_ind_list E : l=> [| u v]; last first. -User-provided eliminators (potentially generated with |Coq|’s ``Function`` +User-provided eliminators (potentially generated with Coq’s ``Function`` command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: @@ -4982,8 +4982,8 @@ distinction between logical propositions and boolean values. On the one hand, logical propositions are objects of *sort* ``Prop`` which is the carrier of intuitionistic reasoning. Logical connectives in ``Prop`` are *types*, which give precise information on the structure -of their proofs; this information is automatically exploited by |Coq| -tactics. For example, |Coq| knows that a proof of ``A \/ B`` is +of their proofs; this information is automatically exploited by Coq +tactics. For example, Coq knows that a proof of ``A \/ B`` is either a proof of ``A`` or a proof of ``B``. The tactics ``left`` and ``right`` change the goal ``A \/ B`` to ``A`` and ``B``, respectively; dually, the tactic ``case`` reduces the goal ``A \/ B => G`` to two @@ -5042,7 +5042,7 @@ mechanism: Coercion is_true (b : bool) := b = true. -This allows any boolean formula ``b`` to be used in a context where |Coq| +This allows any boolean formula ``b`` to be used in a context where Coq would expect a proposition, e.g., after ``Lemma … :``. It is then interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions are elided by the pretty-printer, so they are essentially transparent @@ -5077,9 +5077,9 @@ proposition ``b1 /\ b2`` hides two coercions. The conjunction of Expressing logical equivalences through this family of inductive types makes possible to take benefit from *rewritable equations* associated -to the case analysis of |Coq|’s inductive types. +to the case analysis of Coq’s inductive types. -Since the equivalence predicate is defined in |Coq| as: +Since the equivalence predicate is defined in Coq as: .. coqdoc:: @@ -5573,7 +5573,7 @@ Natural number .. prodn:: nat_or_ident ::= {| @natural | @ident } -where :token:`ident` is an Ltac variable denoting a standard |Coq| number +where :token:`ident` is an Ltac variable denoting a standard Coq number (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) @@ -5823,6 +5823,6 @@ Settings .. [#8] This is an implementation feature: there is no such obstruction in the metatheory .. [#9] The current state of the proof shall be displayed by the Show - Proof command of |Coq| proof mode. + Proof command of Coq proof mode. .. [#10] A simple proof context entry is a naked identifier (i.e. not between parentheses) designating a context entry that is not a section variable. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index c665026500..26a56005c1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -167,11 +167,11 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. Use these elementary patterns to specify a name: * :n:`@ident` — use the specified name -* :n:`?` — let |Coq| choose a name +* :n:`?` — let Coq choose a name * :n:`?@ident` — generate a name that begins with :n:`@ident` * :n:`_` — discard the matched part (unless it is required for another hypothesis) -* if a disjunction pattern omits a name, such as :g:`[|H2]`, |Coq| will choose a name +* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name **Splitting patterns** @@ -268,7 +268,7 @@ These patterns can be used when the hypothesis is an equality: For :n:`intros @intropattern_list`, controls how to handle a conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), |Coq| generates + all the arguments in the constructor. If set (the default), Coq generates additional names to match the number of arguments. Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to |SSR|'s intro patterns. @@ -843,7 +843,7 @@ Applying theorems .. flag:: Universal Lemma Under Conjunction - This flag, which preserves compatibility with versions of |Coq| prior to + This flag, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`). .. tacn:: apply @term in @ident @@ -1293,7 +1293,7 @@ Managing the local context .. tacv:: set @term {? in @goal_occurrences } This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` - but :token:`ident` is generated by |Coq|. + but :token:`ident` is generated by Coq. .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences } eset @term {? in @goal_occurrences } @@ -1338,7 +1338,7 @@ Managing the local context .. tacv:: pose @term This behaves as :n:`pose (@ident := @term)` but :token:`ident` is - generated by |Coq|. + generated by Coq. .. tacv:: epose (@ident {* @binder } := @term) epose @term @@ -1400,7 +1400,7 @@ Controlling the proof flow .. tacv:: assert @type This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is - generated by |Coq|. + generated by Coq. .. tacv:: assert @type by @tactic @@ -1480,7 +1480,7 @@ Controlling the proof flow .. tacv:: enough @type This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of - the hypothesis generated by |Coq|. + the hypothesis generated by Coq. .. tacv:: enough @type as @simple_intropattern @@ -1605,7 +1605,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. must have given the name explicitly (see :ref:`Existential-Variables`). .. note:: When you are referring to hypotheses which you did not name - explicitly, be aware that |Coq| may make a different decision on how to + explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. @@ -1759,7 +1759,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) between :token:`term` and the value that it takes in each of the possible cases. The name of the equation is specified by :token:`naming_intropattern` (see :tacn:`intros`), - in particular ``?`` can be used to let |Coq| generate a fresh name. + in particular ``?`` can be used to let Coq generate a fresh name. .. tacv:: destruct @term with @bindings @@ -2353,7 +2353,7 @@ and an explanation of the underlying technique. ``inversion`` generally behaves in a slightly more expectable way than ``inversion`` (no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to use - ``inversion ... as []``, letting the names being finally chosen by |Coq|. + ``inversion ... as []``, letting the names being finally chosen by Coq. .. example:: @@ -2912,14 +2912,14 @@ Proof maintenance *Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps -may explicitly refer to these names. However, future versions of |Coq| may not assign +may explicitly refer to these names. However, future versions of Coq may not assign names exactly the same way, which could cause the proof to fail because the new names don't match the explicit references in the proof. The following "Mangle Names" settings let users find all the places where proofs rely on automatically generated names, which can then be named explicitly to avoid any incompatibility. These -settings cause |Coq| to generate different names, producing errors for +settings cause Coq to generate different names, producing errors for references to automatically generated names. .. flag:: Mangle Names @@ -2941,7 +2941,7 @@ Performance-oriented tactic variants For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, it skips checking that :n:`@term` is convertible to the goal. - Recall that the |Coq| kernel typechecks proofs again when they are concluded to + Recall that the Coq kernel typechecks proofs again when they are concluded to ensure safety. Hence, using :tacn:`change` checks convertibility twice overall, while :tacn:`change_no_check` can produce ill-typed terms, but checks convertibility only once. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index dd0b12f8ec..36c722bf9b 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -433,7 +433,7 @@ Requests to the environment reference ::= @qualid | @string {? % @scope_key } - Displays the full name of objects from |Coq|'s various qualified namespaces such as terms, + Displays the full name of objects from Coq's various qualified namespaces such as terms, modules and Ltac, thereby showing the module they are defined in. It also displays notation definitions. :n:`@qualid` @@ -491,7 +491,7 @@ Printing flags .. flag:: Fast Name Printing - When turned on, |Coq| uses an asymptotically faster algorithm for the + When turned on, Coq uses an asymptotically faster algorithm for the generation of unambiguous names of bound variables while printing terms. While faster, it is also less clever and results in a typically less elegant display, e.g. it will generate more names rather than reusing certain names @@ -504,12 +504,12 @@ Printing flags Loading files ----------------- -|Coq| offers the possibility of loading different parts of a whole +Coq offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded -files are text files containing sequences of commands for |Coq|’s -toplevel. This kind of file is called a *script* for |Coq|. The standard -(and default) extension of |Coq|’s script files is .v. +files are text files containing sequences of commands for Coq’s +toplevel. This kind of file is called a *script* for Coq. The standard +(and default) extension of Coq’s script files is .v. .. cmd:: Load {? Verbose } {| @string | @ident } @@ -521,7 +521,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard If :n:`@string` is specified, it must specify a complete filename. `~` and .. abbreviations are - allowed as well as shell variables. If no extension is specified, |Coq| + allowed as well as shell variables. If no extension is specified, Coq will use the default extension ``.v``. Files loaded this way can't leave proofs open, nor can :cmd:`Load` @@ -531,7 +531,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard :cmd:`Require` loads `.vo` files that were previously compiled from `.v` files. - :n:`Verbose` displays the |Coq| output for each command and tactic + :n:`Verbose` displays the Coq output for each command and tactic in the loaded file, as if the commands and tactics were entered interactively. .. exn:: Can’t find file @ident on loadpath. @@ -556,14 +556,14 @@ file is a particular case of a module called a *library file*. .. cmd:: Require {? {| Import | Export } } {+ @qualid } :name: Require; Require Import; Require Export - Loads compiled modules into the |Coq| environment. For each :n:`@qualid`, which has the form + Loads compiled modules into the Coq environment. For each :n:`@qualid`, which has the form :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated filesystem directory. The process is applied recursively to all the loaded files; if they contain :cmd:`Require` commands, those commands are executed as well. - The compiled files must have been compiled with the same version of |Coq|. + The compiled files must have been compiled with the same version of Coq. The compiled files are neither replayed nor rechecked. * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined @@ -606,15 +606,15 @@ file is a particular case of a module called a *library file*. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably :n:`@ident.v` was + one already loaded in the current Coq session. Probably :n:`@ident.v` was not properly recompiled with the last version of the file containing module :token:`qualid`. .. exn:: Bad magic number. The file :n:`@ident.vo` was found but either it is not a - |Coq| compiled module, or it was compiled with an incompatible - version of |Coq|. + Coq compiled module, or it was compiled with an incompatible + version of Coq. .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2. @@ -633,14 +633,14 @@ file is a particular case of a module called a *library file*. .. cmd:: Print Libraries This command displays the list of library files loaded in the - current |Coq| session. + current Coq session. .. cmd:: Declare ML Module {+ @string } - This commands dynamically loads |OCaml| compiled code from + This commands dynamically loads OCaml compiled code from a :n:`.mllib` file. It is used to load plugins dynamically. The - files must be accessible in the current |OCaml| loadpath (see the + files must be accessible in the current OCaml loadpath (see the command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. This command is reserved for plugin developers, who should provide @@ -656,7 +656,7 @@ file is a particular case of a module called a *library file*. .. cmd:: Print ML Modules - This prints the name of all |OCaml| modules loaded with :cmd:`Declare ML Module`. + This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. To know from where these module were loaded, the user should use the command :cmd:`Locate File`. @@ -666,7 +666,7 @@ file is a particular case of a module called a *library file*. Loadpath ------------ -Loadpaths are preferably managed using |Coq| command line options (see +Loadpaths are preferably managed using Coq command line options (see Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them for practical purposes. Such commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -703,29 +703,29 @@ the toplevel, and using them in source files is discouraged. This command is equivalent to the command line option :n:`-R @string @dirpath`. It adds the physical directory string and all its - subdirectories to the current |Coq| loadpath. + subdirectories to the current Coq loadpath. .. cmd:: Remove LoadPath @string - This command removes the path :n:`@string` from the current |Coq| loadpath. + This command removes the path :n:`@string` from the current Coq loadpath. .. cmd:: Print LoadPath {? @dirpath } - This command displays the current |Coq| loadpath. If :n:`@dirpath` is specified, + This command displays the current Coq loadpath. If :n:`@dirpath` is specified, displays only the paths that extend that prefix. .. cmd:: Add ML Path @string - This command adds the path :n:`@string` to the current |OCaml| + This command adds the path :n:`@string` to the current OCaml loadpath (cf. :cmd:`Declare ML Module`). .. cmd:: Print ML Path - This command displays the current |OCaml| loadpath. This + This command displays the current OCaml loadpath. This command makes sense only under the bytecode version of ``coqtop``, i.e. using option ``-byte`` (cf. :cmd:`Declare ML Module`). @@ -789,25 +789,25 @@ Quitting and debugging .. cmd:: Quit - Causes |Coq| to exit. Valid only in coqtop. + Causes Coq to exit. Valid only in coqtop. .. cmd:: Drop - This command temporarily enters the |OCaml| toplevel. - It is a debug facility used by |Coq|’s implementers. Valid only in the + This command temporarily enters the OCaml toplevel. + It is a debug facility used by Coq’s implementers. Valid only in the bytecode version of coqtop. - The |OCaml| command: + The OCaml command: :: #use "include";; adds the right loadpaths and loads some toplevel printers for all - abstract types of |Coq|- section_path, identifiers, terms, judgments, …. + abstract types of Coq- section_path, identifiers, terms, judgments, …. You can also use the file base_include instead, that loads only the pretty-printers for section_paths and identifiers. You can return back - to |Coq| with the command: + to Coq with the command: :: @@ -815,9 +815,9 @@ Quitting and debugging .. warning:: - #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, + #. It only works with the bytecode version of Coq (i.e. `coqtop.byte`, see Section `interactive-use`). - #. You must have compiled |Coq| from the source package and set the + #. You must have compiled Coq from the source package and set the environment variable COQTOP to the root of your copy of the sources (see Section `customization-by-environment-variables`). @@ -961,7 +961,7 @@ Controlling the reduction strategies and the conversion algorithm ---------------------------------------------------------------------- -|Coq| provides reduction strategies that the tactics can invoke and two +Coq provides reduction strategies that the tactics can invoke and two different algorithms to check the convertibility of types. The first conversion algorithm lazily compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the @@ -985,8 +985,8 @@ described first. constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding a constant is replacing it by its definition). - :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling - it to delay the unfolding of a constant as much as possible when |Coq| + :cmd:`Opaque` has also an effect on the conversion algorithm of Coq, telling + it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section :ref:`conversion-rules`) of two distinct applied constants. @@ -1222,15 +1222,15 @@ in support libraries of plug-ins. .. _exposing-constants-to-ocaml-libraries: -Exposing constants to |OCaml| libraries +Exposing constants to OCaml libraries ``````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 - Makes the constant :n:`@qualid__1` accessible to |OCaml| libraries under + Makes the constant :n:`@qualid__1` accessible to OCaml libraries under the name :n:`@qualid__2`. The constant can then be dynamically located - in |OCaml| code by - calling :n:`Coqlib.lib_ref "@qualid__2"`. The |OCaml| code doesn't need + in OCaml code by + calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need to know where the constant is defined (what file, module, library, etc.). As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, @@ -1259,9 +1259,9 @@ Registering primitive operations .. cmd:: Primitive @ident_decl {? : @term } := #@ident - Makes the primitive type or primitive operator :n:`#@ident` defined in |OCaml| - accessible in |Coq| commands and tactics. - For internal use by implementors of |Coq|'s standard library or standard library + Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml + accessible in Coq commands and tactics. + For internal use by implementors of Coq's standard library or standard library replacements. No space is allowed after the `#`. Invalid values give a syntax error. diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index cc8af976d2..e6dc6f6c51 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -496,14 +496,14 @@ automatically created. ``typeclass_instances`` hint database. -Hint databases defined in the |Coq| standard library +Hint databases defined in the Coq standard library ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Several hint databases are defined in the |Coq| standard library. The +Several hint databases are defined in the Coq standard library. The actual content of a database is the collection of hints declared to belong to this database in each of the various modules currently loaded. Especially, requiring new modules may extend the database. -At |Coq| startup, only the core database is nonempty and can be used. +At Coq startup, only the core database is nonempty and can be used. :core: This special database is automatically used by ``auto``, except when pseudo-database ``nocore`` is given to ``auto``. The core database @@ -624,7 +624,7 @@ but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects |Coq| uses. Hints should only be made available when +for most of the other objects Coq uses. Hints should only be made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index acf64ae437..c4faa7284f 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -208,7 +208,7 @@ some incompatibilities. .. exn:: I don’t know how to handle dependent equality. The decision procedure managed to find a proof of the goal or of a - discriminable equality but this proof could not be built in |Coq| because of + discriminable equality but this proof could not be built in Coq because of dependently-typed functions. .. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst index f1d4fa789d..1af1b0b726 100644 --- a/doc/sphinx/proofs/creating-tactics/index.rst +++ b/doc/sphinx/proofs/creating-tactics/index.rst @@ -18,13 +18,13 @@ new tactics: - `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin which provides another typed tactic language. While Ltac2 belongs - to the ML language family, Mtac2 reuses the language of |Coq| itself - as the language to build |Coq| tactics. + to the ML language family, Mtac2 reuses the language of Coq itself + as the language to build Coq tactics. - The most traditional way of building new complex tactics is to write - a |Coq| plugin in |OCaml|. Beware that this also requires much more - effort and commitment. A tutorial for writing |Coq| plugins is - available in the |Coq| repository in `doc/plugin_tutorial + a Coq plugin in OCaml. Beware that this also requires much more + effort and commitment. A tutorial for writing Coq plugins is + available in the Coq repository in `doc/plugin_tutorial <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. .. toctree:: diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 1c7fd050f1..7724d7433c 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -4,7 +4,7 @@ Basic proof writing =================== -|Coq| is an interactive theorem prover, or proof assistant, which means +Coq is an interactive theorem prover, or proof assistant, which means that proofs can be constructed interactively through a dialog between the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index b74c9d3a23..fd8a0329d6 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -4,14 +4,14 @@ Proof handling ------------------- -In |Coq|’s proof editing mode all top-level commands documented in +In Coq’s proof editing mode all top-level commands documented in Chapter :ref:`vernacularcommands` remain available and the user has access to specialized commands dealing with proof development pragmas documented in this section. They can also use some other specialized commands called *tactics*. They are the very tools allowing the user to deal with logical reasoning. They are documented in Chapter :ref:`tactics`. -|Coq| user interfaces usually have a way of marking whether the user has +Coq user interfaces usually have a way of marking whether the user has switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into :n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. @@ -30,13 +30,13 @@ When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those +:cite:`How80,Bar81,Gir89,H89`, Coq stores proofs as terms of |Cic|. Those terms are called *proof terms*. .. exn:: No focused proof. - |Coq| raises this error message when one attempts to use a proof editing command + Coq raises this error message when one attempts to use a proof editing command out of the proof editing mode. .. _proof-editing-mode: @@ -62,7 +62,7 @@ list of assertion commands is given in :ref:`Assertions`. The command This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to |Coq| top-level and attaches the extracted + script, switches back to Coq top-level and attaches the extracted proof term to the declared name of the original goal. The name is added to the environment as an opaque constant. @@ -104,7 +104,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Abort {? {| All | @ident } } Cancels the current proof development, switching back to - the previous proof development, or to the |Coq| toplevel if no other + the previous proof development, or to the Coq toplevel if no other proof was being edited. :n:`@ident` @@ -298,8 +298,8 @@ Proof modes ``````````` When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, -|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes -shipped in the standard |Coq| installation, and furthermore some plugins define +Coq picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard Coq installation, and furthermore some plugins define their own proof modes. The default proof mode used when opening a proof can be changed using the following option. @@ -498,7 +498,7 @@ or focus the next one. .. note:: - In Proof General (``Emacs`` interface to |Coq|), you must use + In Proof General (``Emacs`` interface to Coq), you must use bullets with the priority ordering shown above to have a correct indentation. For example ``-`` must be the outer bullet and ``**`` the inner one in the example below. @@ -798,10 +798,10 @@ Requesting information Showing differences between proof steps --------------------------------------- -|Coq| can automatically highlight the differences between successive proof steps -and between values in some error messages. |Coq| can also highlight differences +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Coq can also highlight differences in the proof term. -For example, the following screenshots of |CoqIDE| and coqtop show the application +For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added to it. The second screenshot uses the "removed" option, so it shows the conclusion a @@ -825,24 +825,24 @@ new, no line of old text is shown for them. .. .. image:: ../../_static/diffs-coqide-on.png - :alt: |CoqIDE| with Set Diffs on + :alt: CoqIDE with Set Diffs on .. .. image:: ../../_static/diffs-coqide-removed.png - :alt: |CoqIDE| with Set Diffs removed + :alt: CoqIDE with Set Diffs removed .. .. image:: ../../_static/diffs-coqtop-on3.png :alt: coqtop with Set Diffs on -This image shows an error message with diff highlighting in |CoqIDE|: +This image shows an error message with diff highlighting in CoqIDE: .. .. image:: ../../_static/diffs-error-message.png - :alt: |CoqIDE| error message with diffs + :alt: CoqIDE error message with diffs How to enable diffs ``````````````````` @@ -858,21 +858,21 @@ How to enable diffs For coqtop, showing diffs can be enabled when starting coqtop with the ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option -within |Coq|. You will need to provide the ``-color on|auto`` command-line option when +within Coq. You will need to provide the ``-color on|auto`` command-line option when you start coqtop in either case. Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment variable. See section :ref:`customization-by-environment-variables`. Diffs use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. -In |CoqIDE|, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` -command in |CoqIDE|. You can change the background colors shown for diffs from the +In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in CoqIDE. You can change the background colors shown for diffs from the ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also lets you control other attributes of the highlights, such as the foreground color, bold, italic, underline and strikeout. -Proof General can also display |Coq|-generated proof diffs automatically. +Proof General can also display Coq-generated proof diffs automatically. Please see the PG documentation section "`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) for details. @@ -963,7 +963,7 @@ To show differences in the proof term: - In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. -- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term +- In CoqIDE, position the cursor on or just after a tactic to compare the proof term after the tactic with the proof term before the tactic, then select `View / Show Proof` from the menu or enter the associated key binding. Differences will be shown applying the current `Show Diffs` setting @@ -995,10 +995,10 @@ Controlling the effect of proof editing commands When turned on (it is off by default), this flag enables support for nested proofs: a new assertion command can be inserted before the current proof is - finished, in which case |Coq| will temporarily switch to the proof of this + finished, in which case Coq will temporarily switch to the proof of this *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` or :cmd:`Defined`), its statement will be made available (as if it had been - proved before starting the previous proof) and |Coq| will switch back to the + proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. .. flag:: Printing Goal Names @@ -1015,12 +1015,12 @@ Controlling memory usage Prints heap usage statistics, which are values from the `stat` type of the `Gc` module described `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ - in the |OCaml| documentation. + in the OCaml documentation. The `live_words`, `heap_words` and `top_heap_words` values give the basic information. Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. When experiencing high memory usage the following commands can be used -to force |Coq| to optimize some of its internal data structures. +to force Coq to optimize some of its internal data structures. .. cmd:: Optimize Proof @@ -1030,7 +1030,7 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Heap Perform a heap compaction. This is generally an expensive operation. - See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ There is also an analogous tactic :tacn:`optimize_heap`. Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 1358aad432..f3f69a2fdc 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -362,7 +362,7 @@ the conversion in hypotheses :n:`{+ @ident}`. These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In - correspondence with the kinds of reduction considered in |Coq| namely + correspondence with the kinds of reduction considered in Coq namely :math:`\beta` (reduction of functional application), :math:`\delta` (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of @@ -444,8 +444,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: native_compute :name: native_compute - This tactic evaluates the goal by compilation to |OCaml| as described - in :cite:`FullReduction`. If |Coq| is running in native code, it can be + This tactic evaluates the goal by compilation to OCaml as described + in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than :tacn:`vm_compute`. Note however that the compilation cost is higher, so it is worth using only for intensive computations. @@ -783,7 +783,7 @@ the conversion in hypotheses :n:`{+ @ident}`. If we try to prove :g:`id (fact n) = fact n` by :tacn:`reflexivity`, it will now take time proportional to - :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :math:`n!`, because Coq will keep unfolding :g:`fact` and :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full computation of :g:`fact n` (in unary, because we are using :g:`nat`), which takes time :math:`n!`. We can see this cross @@ -827,7 +827,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Time Defined. On small examples this sort of behavior doesn't matter, but - because |Coq| is a super-linear performance domain in so many + because Coq is a super-linear performance domain in so many places, unless great care is taken, tactic automation using :tacn:`with_strategy` may not be robustly performant when scaling the size of the input. diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index e67405a8dc..32d3e87e68 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -15,14 +15,9 @@ .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` .. |Cic| replace:: CIC -.. |Coq| replace:: :smallcaps:`Coq` -.. |CoqIDE| replace:: :smallcaps:`CoqIDE` .. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` -.. |Gallina| replace:: :smallcaps:`Gallina` .. |Latex| replace:: :smallcaps:`LaTeX` .. |Ltac| replace:: `L`:sub:`tac` -.. |ML| replace:: :smallcaps:`ML` -.. |OCaml| replace:: :smallcaps:`OCaml` .. |p_1| replace:: `p`\ :math:`_{1}` .. |p_i| replace:: `p`\ :math:`_{i}` .. |p_n| replace:: `p`\ :math:`_{n}` diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index abecee8459..f9d4864492 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -129,7 +129,7 @@ Automatic declaration of schemes .. warning:: - You have to be careful with these flags since |Coq| may now reject well-defined + You have to be careful with these flags since Coq may now reject well-defined inductive types because it cannot compute a Boolean equality for them. .. flag:: Rewriting Schemes diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9d1fcc160d..f36767b207 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -3,7 +3,7 @@ Syntax extensions and notation scopes ===================================== -In this chapter, we introduce advanced commands to modify the way |Coq| +In this chapter, we introduce advanced commands to modify the way Coq parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. @@ -13,7 +13,7 @@ The main commands to provide custom symbolic notations for terms are variant of :cmd:`Notation` which does not modify the parser; this provides a form of :ref:`abbreviation <Abbreviations>`. It is sometimes expected that the same symbolic notation has different meanings in -different contexts; to achieve this form of overloading, |Coq| offers a notion +different contexts; to achieve this form of overloading, Coq offers a notion of :ref:`notation scopes <Scopes>`. The main command to provide custom notations for tactics is :cmd:`Tactic Notation`. @@ -71,7 +71,7 @@ least 3 characters and starting with a simple quote must be quoted Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3). A notation binds a syntactic expression to a term. Unless the parser -and pretty-printer of |Coq| already know how to deal with the syntactic +and pretty-printer of Coq already know how to deal with the syntactic expression (such as through :cmd:`Reserved Notation` or for notations that contain only literals), explicit precedences and associativity rules have to be given. @@ -88,7 +88,7 @@ Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Mixing different symbolic notations in the same text may cause serious -parsing ambiguity. To deal with the ambiguity of notations, |Coq| uses +parsing ambiguity. To deal with the ambiguity of notations, Coq uses precedence levels ranging from 0 to 100 (plus one extra level numbered 200) and associativity rules. @@ -99,7 +99,7 @@ Consider for example the new notation Notation "A \/ B" := (or A B). Clearly, an expression such as :g:`forall A:Prop, True /\ A \/ A \/ False` -is ambiguous. To tell the |Coq| parser how to interpret the +is ambiguous. To tell the Coq parser how to interpret the expression, a priority between the symbols ``/\`` and ``\/`` has to be given. Assume for instance that we want conjunction to bind more than disjunction. This is expressed by assigning a precedence level to each @@ -117,7 +117,7 @@ defaults to :g:`True /\ (False /\ False)` (right associativity) or to expression is not well-formed and that parentheses are mandatory (this is a “no associativity”) [#no_associativity]_. We do not know of a special convention for the associativity of disjunction and conjunction, so let us apply -right associativity (which is the choice of |Coq|). +right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations are specified with a list of parenthesized :n:`@syntax_modifier`\s. Here is how the previous examples refine: @@ -187,7 +187,7 @@ left. See the next section for more about factorization. Simple factorization rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| extensible parsing is performed by *Camlp5* which is essentially a LL1 +Coq extensible parsing is performed by *Camlp5* which is essentially a LL1 parser: it decides which notation to parse by looking at tokens from left to right. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example. @@ -209,16 +209,16 @@ need to force the parsing level of ``y``, as follows. Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). -For the sake of factorization with |Coq| predefined rules, simple rules +For the sake of factorization with Coq predefined rules, simple rules have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list -of |Coq| predefined notations can be found in the chapter on :ref:`thecoqlibrary`. +of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. Displaying symbolic notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command :cmd:`Notation` has an effect both on the |Coq| parser and on the -|Coq| printer. For example: +The command :cmd:`Notation` has an effect both on the Coq parser and on the +Coq printer. For example: .. coqtop:: all @@ -226,7 +226,7 @@ The command :cmd:`Notation` has an effect both on the |Coq| parser and on the However, printing, especially pretty-printing, also requires some care. We may want specific indentations, line breaks, alignment if on -several lines, etc. For pretty-printing, |Coq| relies on |OCaml| +several lines, etc. For pretty-printing, Coq relies on OCaml formatting library, which provides indentation and automatic line breaks depending on page width by means of *formatting boxes*. @@ -349,12 +349,12 @@ Reserving notations .. cmd:: Reserved Notation @string {? ( {+, @syntax_modifier } ) } - A given notation may be used in different contexts. |Coq| expects all + A given notation may be used in different contexts. Coq expects all uses of the notation to be defined at the same precedence and with the same associativity. To avoid giving the precedence and associativity every time, this command declares a parsing rule (:token:`string`) in advance without giving its interpretation. Here is an example from the initial - state of |Coq|. + state of Coq. .. coqtop:: in @@ -454,7 +454,7 @@ Displaying information about notations definition where the nonterminal was referenced. This command shows the original grammar, so it won't exactly match the documentation. - The |Coq| parser is based on Camlp5. The documentation for + The Coq parser is based on Camlp5. The documentation for `Extensible grammars <http://camlp5.github.io/doc/htmlc/grammars.html>`_ is the most relevant but it assumes considerable knowledge. Here are the essentials: @@ -521,7 +521,7 @@ Displaying information about notations The file `doc/tools/docgram/fullGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar>`_ in the source tree extracts the full grammar for - |Coq| (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) + Coq (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) in a single file with minor changes to handle nonterminals using multiple levels (described in `doc/tools/docgram/README.md <http://github.com/coq/coq/blob/master/doc/tools/docgram/README.md>`_). This is complete and much easier to read than the grammar source files. @@ -762,7 +762,7 @@ recursive patterns. The basic example is: Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). On the right-hand side, an extra construction of the form ``.. t ..`` can -be used. Notice that ``..`` is part of the |Coq| syntax and it must not be +be used. Notice that ``..`` is part of the Coq syntax and it must not be confused with the three-dots notation “``…``” used in this manual to denote a sequence of arbitrary size. @@ -942,7 +942,7 @@ Custom entries Custom entries have levels, like the main grammar of terms and grammar of patterns have. The lower level is 0 and this is the level used by default to put rules delimited with tokens on both ends. The level is -left to be inferred by |Coq| when using :n:`in custom @ident`. The +left to be inferred by Coq when using :n:`in custom @ident`. The level is otherwise given explicitly by using the syntax :n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level. @@ -996,7 +996,7 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case |Coq| infer it. If the sub-expression is at a border of +in which case Coq infer it. If the sub-expression is at a border of the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is determined by the associativity. If the sub-expression is not at the border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is @@ -1097,7 +1097,7 @@ Here are the syntax elements used by the various notation commands. time. Type checking is done only at the time of use of the notation. .. note:: Some examples of Notation may be found in the files composing - the initial state of |Coq| (see directory :file:`$COQLIB/theories/Init`). + the initial state of Coq (see directory :file:`$COQLIB/theories/Init`). .. note:: The notation ``"{ x }"`` has a special status in the main grammars of terms and patterns so that @@ -1122,7 +1122,7 @@ Here are the syntax elements used by the various notation commands. .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax. This warning is disabled by default to avoid spurious diagnostics - due to legacy notation in the |Coq| standard library. + due to legacy notation in the Coq standard library. It can be turned on with the ``-w disj-pattern-notation`` flag. .. _Scopes: @@ -1156,7 +1156,7 @@ Most commands use :token:`scope_name`; :token:`scope_key`\s are used within :tok .. cmd:: Declare Scope @scope_name Declares a new notation scope. Note that the initial - state of |Coq| declares the following notation scopes: + state of Coq declares the following notation scopes: ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. @@ -1167,7 +1167,7 @@ Global interpretation rules for notations At any time, the interpretation of a notation for a term is done within a *stack* of notation scopes and lonely notations. If a -notation is defined in multiple scopes, |Coq| uses the interpretation from +notation is defined in multiple scopes, Coq uses the interpretation from the most recently opened notation scope or declared lonely notation. Note that "stack" is a misleading name. Each scope or lonely notation can only appear in @@ -1308,10 +1308,10 @@ recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or .. _notation-scopes: -Notation scopes used in the standard library of |Coq| +Notation scopes used in the standard library of Coq ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We give an overview of the scopes used in the standard library of |Coq|. +We give an overview of the scopes used in the standard library of Coq. For a complete list of notations in each scope, use the commands :cmd:`Print Scopes` or :cmd:`Print Scope`. @@ -1377,7 +1377,7 @@ Scopes` or :cmd:`Print Scope`. ``string_scope`` This scope includes notation for strings as elements of the type string. - Special characters and escaping follow |Coq| conventions on strings (see + Special characters and escaping follow Coq conventions on strings (see :ref:`lexical-conventions`). Especially, there is no convention to visualize non printable characters of a string. The file :file:`String.v` shows an example that contains quotes, a newline and a beep (i.e. the ASCII character @@ -1478,7 +1478,7 @@ Abbreviations An abbreviation expects no precedence nor associativity, since it is parsed as an usual application. Abbreviations are used as - much as possible by the |Coq| printers unless the modifier ``(only + much as possible by the Coq printers unless the modifier ``(only parsing)`` is given. An abbreviation is bound to an absolute name as an ordinary definition is @@ -1673,7 +1673,7 @@ Number notations with :n:`(abstract after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. Typically, this indicates that the fully computed representation - of numbers can be so large that non-tail-recursive |OCaml| + of numbers can be so large that non-tail-recursive OCaml functions run out of stack space when trying to walk them. .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type. @@ -2248,9 +2248,9 @@ Tactic notations allow customizing the syntax of tactics. .. rubric:: Footnotes .. [#and_or_levels] which are the levels effectively chosen in the current - implementation of |Coq| + implementation of Coq -.. [#no_associativity] |Coq| accepts notations declared as nonassociative but the parser on - which |Coq| is built, namely Camlp5, currently does not implement ``no associativity`` and - replaces it with ``left associativity``; hence it is the same for |Coq|: ``no associativity`` +.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on + which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` is in fact ``left associativity`` for the purposes of parsing diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index 95218322ff..0bd3054788 100644 --- a/doc/sphinx/using/libraries/index.rst +++ b/doc/sphinx/using/libraries/index.rst @@ -4,15 +4,15 @@ Libraries and plugins ===================== -|Coq| is distributed with a standard library and a set of internal +Coq is distributed with a standard library and a set of internal plugins (most of which provide tactics that have already been presented in :ref:`writing-proofs`). This chapter presents this standard library and some of these internal plugins which provide features that are not tactics. -In addition, |Coq| has a rich ecosystem of external libraries and +In addition, Coq has a rich ecosystem of external libraries and plugins. These libraries and plugins can be browsed online through -the `|Coq| Package Index <https://coq.inria.fr/opam/www/>`_ and +the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and installed with the `opam package manager <https://coq.inria.fr/opam-using.html>`_. diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 724bcd0488..917edf0774 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -1,9 +1,9 @@ -Writing |Coq| libraries and plugins +Writing Coq libraries and plugins =================================== -This section presents the part of the |Coq| language that is useful only -to library and plugin authors. A tutorial for writing |Coq| plugins is -available in the |Coq| repository in `doc/plugin_tutorial +This section presents the part of the Coq language that is useful only +to library and plugin authors. A tutorial for writing Coq plugins is +available in the Coq repository in `doc/plugin_tutorial <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_. Deprecating library objects or tactics diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 88c1a575d9..7ab8f9d763 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -2,14 +2,14 @@ .. _coqdoc: -Documenting |Coq| files with coqdoc +Documenting Coq files with coqdoc ----------------------------------- -coqdoc is a documentation tool for the proof assistant |Coq|, similar to +coqdoc is a documentation tool for the proof assistant Coq, similar to ``javadoc`` or ``ocamldoc``. The task of coqdoc is -#. to produce a nice |Latex| and/or HTML document from |Coq| source files, +#. to produce a nice |Latex| and/or HTML document from Coq source files, readable for a human and not only for the proof assistant; #. to help the user navigate his own (or third-party) sources. @@ -18,9 +18,9 @@ coqdoc is a documentation tool for the proof assistant |Coq|, similar to Principles ~~~~~~~~~~ -Documentation is inserted into |Coq| files as *special comments*. Thus +Documentation is inserted into Coq files as *special comments*. Thus your files will compile as usual, whether you use coqdoc or not. coqdoc -presupposes that the given |Coq| files are well-formed (at least +presupposes that the given Coq files are well-formed (at least lexically). Documentation starts with ``(**``, followed by a space, and ends with ``*)``. The documentation format is inspired by Todd A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with @@ -29,10 +29,10 @@ shouldn’t fail, whatever the input is. But remember: “garbage in, garbage out”. -|Coq| material inside documentation. +Coq material inside documentation. ++++++++++++++++++++++++++++++++++++ -|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets +Coq material is quoted between the delimiters ``[`` and ``]``. Square brackets may be nested, the inner ones being understood as being part of the quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun x => u]``). Inside quotations, the code is pretty-printed in the same @@ -46,7 +46,7 @@ Pretty-printing. ++++++++++++++++ coqdoc uses different faces for identifiers and keywords. The pretty- -printing of |Coq| tokens (identifiers or symbols) can be controlled +printing of Coq tokens (identifiers or symbols) can be controlled using one of the following commands: :: @@ -63,7 +63,7 @@ or (** printing *token* $...LATEX math...$ #...html...# *) -It gives the |Latex| and HTML texts to be produced for the given |Coq| +It gives the |Latex| and HTML texts to be produced for the given Coq token. Either the |Latex| or the HTML rule may be omitted, causing the default pretty-printing to be used for this token. @@ -91,7 +91,7 @@ commands. The recognition of tokens is done by a (``ocaml``) lex automaton and thus applies the longest-match rule. For instance, `->~` - is recognized as a single token, where |Coq| sees two tokens. It is the + is recognized as a single token, where Coq sees two tokens. It is the responsibility of the user to insert space between tokens *or* to give pretty-printing rules for the possible combinations, e.g. @@ -217,7 +217,7 @@ Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look for name resolutions in the file ``file`` (it will look in ``file.glob`` by default). -Identifiers from the |Coq| standard library are linked to the Coq website +Identifiers from the Coq standard library are linked to the Coq website `<http://coq.inria.fr/library/>`_. This behavior can be changed using command line options ``--no-externals`` and ``--coqlib``; see below. @@ -253,7 +253,7 @@ The latter cannot be used around some inner parts of a proof, but can be used around a whole proof. Lastly, it is possible to adopt a middle-ground approach when the -desired output is HTML, where a given snippet of |Coq| material is +desired output is HTML, where a given snippet of Coq material is hidden by default, but can be made visible with user interaction. :: @@ -280,12 +280,12 @@ Usage coqdoc is invoked on a shell command line as follows: ``coqdoc <options and files>``. Any command line argument which is not an option is considered to be a -file (even if it starts with a ``-``). |Coq| files are identified by the +file (even if it starts with a ``-``). Coq files are identified by the suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. :HTML output: This is the default output format. One HTML file is created for - each |Coq| file given on the command line, together with a file + each Coq file given on the command line, together with a file ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a style sheet named ``style.css``. Such a file is distributed with coqdoc. :|Latex| output: A single |Latex| file is created, on standard @@ -295,7 +295,7 @@ suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. document . DVI and PostScript can be produced directly with the options ``-dvi`` and ``-ps`` respectively. :TEXmacs output: To translate the input files to TEXmacs format, - to be used by the TEXmacs |Coq| interface. + to be used by the TEXmacs Coq interface. @@ -357,18 +357,18 @@ Command line options **Hyperlink options** - :--glob-from file: Make references using |Coq| globalizations from file - file. (Such globalizations are obtained with |Coq| option ``-dump-glob``). - :--no-externals: Do not insert links to the |Coq| standard library. + :--glob-from file: Make references using Coq globalizations from file + file. (Such globalizations are obtained with Coq option ``-dump-glob``). + :--no-externals: Do not insert links to the Coq standard library. :--external url coqdir: Use given URL for linking references whose name starts with prefix ``coqdir``. - :--coqlib url: Set base URL for the |Coq| standard library (default is + :--coqlib url: Set base URL for the Coq standard library (default is `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url Coq``. - :-R dir coqdir: Recursively map physical directory dir to |Coq| logical - directory ``coqdir`` (similarly to |Coq| option ``-R``). - :-Q dir coqdir: Map physical directory dir to |Coq| logical - directory ``coqdir`` (similarly to |Coq| option ``-Q``). + :-R dir coqdir: Recursively map physical directory dir to Coq logical + directory ``coqdir`` (similarly to Coq option ``-R``). + :-Q dir coqdir: Map physical directory dir to Coq logical + directory ``coqdir`` (similarly to Coq option ``-Q``). .. note:: @@ -420,7 +420,7 @@ Command line options :--plain-comments: Do not interpret comments, simply copy them as plain-text. :--interpolate: Use the globalization information to typeset - identifiers appearing in |Coq| escapings inside comments. + identifiers appearing in Coq escapings inside comments. **Language options** diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index 8543c5de8a..dfe38dfce9 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -5,11 +5,11 @@ Command-line and graphical tools ================================ This chapter presents the command-line tools that users will need to -build their |Coq| project, the documentation of the |CoqIDE| standalone +build their Coq project, the documentation of the CoqIDE standalone user interface and the documentation of the parallel proof processing -feature that is supported by |CoqIDE| and several other user interfaces. -A list of available user interfaces to interact with |Coq| is available -on the `|Coq| website <https://coq.inria.fr/user-interfaces.html>`_. +feature that is supported by CoqIDE and several other user interfaces. +A list of available user interfaces to interact with Coq is available +on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. .. toctree:: :maxdepth: 1 |