diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/10430-extraction-int63.rst | 5 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/09811-remove-zlogarithm.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/10445-constructive-reals.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 36 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 107 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 126 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 20 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 5 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 38 |
13 files changed, 220 insertions, 198 deletions
diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst new file mode 100644 index 0000000000..ab625b9e03 --- /dev/null +++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst @@ -0,0 +1,4 @@ +- Removes deprecated modules `Coq.ZArith.Zlogarithm` + and `Coq.ZArith.Zsqrt_compat` + (#9881 <https://github.com/coq/coq/pull/9811> + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst new file mode 100644 index 0000000000..d69056fc2f --- /dev/null +++ b/doc/changelog/10-standard-library/10445-constructive-reals.rst @@ -0,0 +1,12 @@ +- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers. Classical real numbers are now defined + as a quotient of these constructive real numbers, which significantly reduces + the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), + while preserving backward compatibility. + + Futhermore, the new axioms for classical real numbers include the limited + principle of omniscience (`sig_forall_dec`), which is a logical principle + instead of an ad hoc property of the real numbers. + + See `#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters. diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d1b95e6203..ac75240cfb 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -7,22 +7,20 @@ The |Coq| library single: Theories -The |Coq| library is structured into two parts: +The |Coq| library has two parts: - * **The initial library**: it contains elementary logical notions and - data-types. It constitutes the basic state of the system directly - available when running |Coq|; + * **The basic library**: definitions and theorems for + the most commonly used elementary logical notions and + data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries containing various - developments of |Coq| axiomatizations about sets, lists, sorting, - arithmetic, etc. This library comes with the system and its modules - are directly accessible through the ``Require`` command (see - Section :ref:`compiled-files`); + * **The 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`) -In addition, user-provided libraries or developments are provided by -|Coq| users' community. These libraries and developments are available -for download at http://coq.inria.fr (see -Section :ref:`userscontributions`). +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 also be browsed at http://coq.inria.fr/stdlib. @@ -514,8 +512,8 @@ realizability interpretation. forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. -Basic Arithmetics -~~~~~~~~~~~~~~~~~ +Basic Arithmetic +~~~~~~~~~~~~~~~~ The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and @@ -804,8 +802,8 @@ Notation Interpretation =============== =================== -Notations for integer arithmetics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Notations for integer arithmetic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. index:: single: Arithmetical notations @@ -822,7 +820,7 @@ Notations for integer arithmetics The following table describes the syntax of expressions -for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. +for integer arithmetic. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. @@ -866,7 +864,7 @@ Notations for real numbers This is provided by requiring and opening the module ``Reals`` and opening scope ``R_scope``. This set of notations is very similar to -the notation for integer arithmetics. The inverse function was added. +the notation for integer arithmetic. The inverse function was added. =============== =================== Notation Interpretation diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..dc4f91e66b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -260,10 +260,7 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -:flag:`Printing Primitive Projection Parameters` flag. Further compatibility -printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern matching -over primitive records. +:flag:`Printing Primitive Projection Parameters` flag. There are currently two ways to introduce primitive records types: @@ -2443,12 +2440,19 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said module is not produced by +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. 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. +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). + Bidirectionality hints ---------------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 38f6714f46..91dfa34494 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -44,78 +44,91 @@ Lexical conventions =================== Blanks - Space, newline and horizontal tabulation are considered as blanks. + Space, newline and horizontal tab are considered blanks. Blanks are ignored but they separate tokens. Comments - Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, :token:`string` literals must be + Comments are enclosed between ``(*`` and ``*)``. They can be nested. + They can contain any character. However, embedded :token:`string` literals must be correctly closed. Comments are treated as blanks. -Identifiers and access identifiers +Identifiers and field identifiers Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and - ``'``, that do not start with a digit or ``'``. That is, they are - recognized by the following lexical class: + ``'``, that do not start with a digit or ``'``. That is, they are + recognized by the following grammar (except that the string ``_`` is reserved; + it is not a valid identifier): .. productionlist:: coq - first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter - subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - access_ident : .`ident` + field : .`ident` + first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` + subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` All characters are meaningful. In particular, identifiers are case-sensitive. - The entry ``unicode-letter`` non-exhaustively includes Latin, + :production:`unicode_letter` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. - Access identifiers, written :token:`access_ident`, are identifiers prefixed by - `.` (dot) without blank. They are used in the syntax of qualified - identifiers. + Field identifiers, written :token:`field`, are identifiers prefixed by + `.` (dot) with no blank between the dot and the identifier. They are used in + the syntax of qualified identifiers. Numerals - Numerals are sequences of digits with a potential fractional part - and exponent. Integers are numerals without fractional nor exponent - part and optionally preceded by a minus sign. Underscores ``_`` can - be used as comments in numerals. + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :token:`int` is an integer; + a numeral without fractional or exponent parts. :token:`num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. .. productionlist:: coq - digit : 0..9 + numeral : `num`[. `num`][`exp`[`sign`]`num`] + int : [-]`num` num : `digit`…`digit` - integer : [-]`num` - dot : . + digit : 0..9 exp : e | E sign : + | - - numeral : `num`[`dot` `num`][`exp`[`sign`]`num`] Strings - Strings are delimited by ``"`` (double quote), and enclose a sequence of - any characters different from ``"`` or the sequence ``""`` to denote the - double quote character. In grammars, the entry for quoted strings is - :production:`string`. + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. Keywords - The following identifiers are reserved keywords, and cannot be - employed otherwise:: - - _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod return - SProp Prop Set Type then using where with - -Special tokens - The following sequences of characters are special tokens:: - - ! % & && ( () ) * + ++ , - -> . .( .. - / /\ : :: :< := :> ; < <- <-> <: <= <> = - => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ #[ - - Lexical ambiguities are resolved according to the “longest match” - rule: when a sequence of non alphanumerical characters can be - decomposed into several different ways, then the first token is the - longest possible one (among all tokens defined at this moment), and so - on. + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +Other tokens + The set of + tokens defined at any given time can vary because the :cmd:`Notation` + command can define new tokens. A :cmd:`Require` command may load more notation definitions, + while the end of a :cmd:`Section` may remove notations. Some notations + are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token is used. + Occasionally you may need to insert spaces to separate tokens. For example, + if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and + ``~~`` generate different tokens, whereas if `~~` is not defined, then the + two inputs are equivalent. .. _term: @@ -164,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ( `name` [: `term`] := `term` ) : ' `pattern` name : `ident` | _ - qualid : `ident` | `qualid` `access_ident` + qualid : `ident` | `qualid` `field` sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ 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 "information" button is described in Section :ref:`try-tactics-automatically`. - 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. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 46f9826e41..362c3da6cb 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -31,10 +31,10 @@ Syntax The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this -chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +chapter: entries :token:`num`, :token:`int`, :token:`ident` :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, Coq terms and patterns and all the atomic +represent respectively natural and integer numbers, +identifiers, qualified names, Coq terms, patterns and the atomic tactics described in Chapter :ref:`tactics`. The syntax of :production:`cpattern` is @@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below. : `atom` atom : `qualid` : () - : `integer` + : `int` : ( `ltac_expr` ) component : `string` | `qualid` - message_token : `string` | `ident` | `integer` + message_token : `string` | `ident` | `int` tacarg : `qualid` : () : ltac : `atom` @@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below. match_rule : `cpattern` => `ltac_expr` : context [`ident`] [ `cpattern` ] => `ltac_expr` : _ => `ltac_expr` - test : `integer` = `integer` - : `integer` (< | <= | > | >=) `integer` + test : `int` = `int` + : `int` (< | <= | > | >=) `int` selector : [`ident`] - : `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `int` + : (`int` | `int` - `int`), ..., (`int` | `int` - `int`) toplevel_selector : `selector` : all : par diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..c545287fdd 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -17,16 +17,16 @@ Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: - is error-prone and fragile - has an intricate implementation -Following the need of users that start developing huge projects relying +Following the need of users who are developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following: - at least informal, predictable semantics -- a typing system -- standard programming facilities (i.e. datatypes) +- a type system +- standard programming facilities (e.g., datatypes) This new language, called Ltac2, is described in this chapter. It is still -experimental but we encourage nonetheless users to start testing it, +experimental but we nonetheless encourage users to start testing it, especially wherever an advanced tactic language is needed. The previous implementation of Ltac, described in the previous chapter, will be referred to as Ltac1. @@ -36,9 +36,9 @@ as Ltac1. General design -------------- -There are various alternatives to Ltac1, such that Mtac or Rtac for instance. -While those alternatives can be quite distinct from Ltac1, we designed -Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +There are various alternatives to Ltac1, such as Mtac or Rtac for instance. +While those alternatives can be quite different from Ltac1, we designed +Ltac2 to be as close as reasonably possible to Ltac1, while fixing the aforementioned defects. In particular, Ltac2 is: @@ -47,11 +47,11 @@ In particular, Ltac2 is: * a call-by-value functional language * with effects - * together with Hindley-Milner type system + * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of Coq-side terms -- a language featuring notation facilities to help writing palatable scripts +- a language featuring notation facilities to help write palatable scripts We describe more in details each point in the remainder of this document. @@ -77,7 +77,7 @@ 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 computation will be well-typed. This is actually a design choice, motivated -by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are provided with an ill-typed term. @@ -92,7 +92,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. +close to OCaml. Types follow the simply-typed syntax of OCaml. The non-terminal :production:`lident` designates identifiers starting with a lowercase. @@ -122,7 +122,7 @@ Built-in types include: Type declarations ~~~~~~~~~~~~~~~~~ -One can define new types by the following commands. +One can define new types with the following commands. .. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type @@ -149,7 +149,7 @@ One can define new types by the following commands. Variants are sum types defined by constructors and eliminated by pattern-matching. They can be recursive, but the `rec` flag must be - explicitly set. Pattern-maching must be exhaustive. + explicitly set. Pattern matching must be exhaustive. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. @@ -158,15 +158,15 @@ One can define new types by the following commands. Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example - is the standard `exn` type. Pattern-matching must always include a catch-all - clause. They can be extended by this command. + is the standard `exn` type. Pattern matching on open variants must always include a catch-all + clause. They can be extended with this command. Term Syntax ~~~~~~~~~~~ The syntax of the functional fragment is very close to the one of Ltac1, except that it adds a true pattern-matching feature, as well as a few standard -constructions from ML. +constructs from ML. .. productionlist:: coq ltac2_var : `lident` @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -202,7 +202,7 @@ constructions from ML. In practice, there is some additional syntactic sugar that allows e.g. to bind a variable and match on it at the same time, in the usual ML style. -There is a dedicated syntax for list and array literals. +There is dedicated syntax for list and array literals. .. note:: @@ -217,7 +217,7 @@ Ltac Definitions This command defines a new global Ltac2 value. For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, i.e. a function, a constant or a pure constructor recursively applied to + value, that is, a function, a constant or a pure constructor recursively applied to values. If ``rec`` is set, the tactic is expanded into a recursive binding. @@ -247,7 +247,7 @@ if ever we implement native compilation. The expected equations are as follows:: (t any term, V values, C constructor) Note that call-by-value reduction is already a departure from Ltac1 which uses -heuristics to decide when evaluating an expression. For instance, the following +heuristics to decide when to evaluate an expression. For instance, the following expressions do not evaluate the same way in Ltac1. :n:`foo (idtac; let x := 0 in bar)` @@ -255,7 +255,7 @@ expressions do not evaluate the same way in Ltac1. :n:`foo (let x := 0 in bar)` Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk -not to compute the argument, and :n:`foo` would have e.g. type +to not compute the argument, and :n:`foo` would have e.g. type :n:`(unit -> unit) -> unit`. :n:`foo (fun () => let x := 0 in bar)` @@ -263,19 +263,19 @@ not to compute the argument, and :n:`foo` would have e.g. type Typing ~~~~~~ -Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there +Typing is strict and follows the Hindley-Milner system. Unlike Ltac1, there are no type casts at runtime, and one has to resort to conversion functions. See notations though to make things more palatable. -In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but -one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`, +In this setting, all the usual argument-free tactics have type :n:`unit -> unit`, but +one can return a value of type :n:`t` thanks to terms of type :n:`unit -> t`, or take additional arguments. Effects ~~~~~~~ Effects in Ltac2 are straightforward, except that instead of using the -standard IO monad as the ambient effectful world, Ltac2 is going to use the +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 @@ -288,15 +288,15 @@ Intuitively a thunk of type :n:`unit -> 'a` can do the following: - It can perform non-backtracking IO like printing and setting mutable variables - It can fail in a non-recoverable way -- It can use first-class backtrack. The proper way to figure that is that we - morally have the following isomorphism: +- It can use first-class backtracking. One way to think about this is that + thunks are isomorphic to this type: :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a lazy list of results where each tail is waiting for a continuation exception. -- It can access a backtracking proof state, made out amongst other things of +- It can access a backtracking proof state, consisting among other things of the current evar assignation and the list of goals under focus. -We describe more thoroughly the various effects existing in Ltac2 hereafter. +We now describe more thoroughly the various effects in Ltac2. Standard IO +++++++++++ @@ -315,28 +315,28 @@ Fatal errors ++++++++++++ The Ltac2 language provides non-backtracking exceptions, also known as *panics*, -through the following primitive in module `Control`.:: +through the following primitive in module `Control`:: val throw : exn -> 'a Unlike backtracking exceptions from the next section, this kind of error is never caught by backtracking primitives, that is, throwing an exception -destroys the stack. This is materialized by the following equation, where `E` -is an evaluation context.:: +destroys the stack. This is codified by the following equation, where `E` +is an evaluation context:: E[throw e] ≡ throw e (e value) -There is currently no way to catch such an exception and it is a design choice. -There might be at some future point a way to catch it in a brutal way, -destroying all backtrack and return values. +There is currently no way to catch such an exception, which is a deliberate design choice. +Eventually there might be a way to catch it and +destroy all backtrack and return values. -Backtrack -+++++++++ +Backtracking +++++++++++++ In Ltac2, we have the following backtracking primitives, defined in the -`Control` module.:: +`Control` module:: Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. @@ -344,7 +344,7 @@ In Ltac2, we have the following backtracking primitives, defined in the val plus : (unit -> 'a) -> (exn -> 'a) -> 'a val case : (unit -> 'a) -> ('a * (exn -> 'a)) result -If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +If one views thunks as lazy lists, then `zero` is the empty list and `plus` is list concatenation, while `case` is pattern-matching. The backtracking is first-class, i.e. one can write @@ -376,8 +376,8 @@ represent several goals, including none. Thus, there is no such thing as *the current goal*. Goals are naturally ordered, though. It is natural to do the same in Ltac2, but we must provide a way to get access -to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focused goal in turn.:: +to a given goal. This is the role of the `enter` primitive, which applies a +tactic to each currently focused goal in turn:: val enter : (unit -> unit) -> unit @@ -452,9 +452,9 @@ The following syntactic sugar is provided for two common cases. Strict vs. non-strict mode ++++++++++++++++++++++++++ -Depending on the context, quotations producing terms (i.e. ``constr`` or +Depending on the context, quotation-producing terms (i.e. ``constr`` or ``open_constr``) are not internalized in the same way. There are two possible -modes, respectively called the *strict* and the *non-strict* mode. +modes, the *strict* and the *non-strict* mode. - In strict mode, all simple identifiers appearing in a term quotation are required to be resolvable statically. That is, they must be the short name of @@ -467,7 +467,7 @@ modes, respectively called the *strict* and the *non-strict* mode. of the term at runtime will fail if there is no such variable in the dynamic context. -Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +Strict mode is enforced by default, such as for all Ltac2 definitions. Non-strict mode is only set when evaluating Ltac2 snippets in interactive proof mode. The rationale is that it is cumbersome to explicitly add ``&`` interactively, while it is expected that global tactics enforce more invariants on their code. @@ -490,12 +490,12 @@ for their side-effects. Semantics +++++++++ -Interpretation of a quoted Coq term is done in two phases, internalization and +A quoted Coq term is interpreted in two phases, internalization and evaluation. -- Internalization is part of the static semantics, i.e. it is done at Ltac2 +- Internalization is part of the static semantics, that is, it is done at Ltac2 typing time. -- Evaluation is part of the dynamic semantics, i.e. it is done when +- 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 @@ -670,9 +670,9 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } -A few scopes contain antiquotation features. For sake of uniformity, all +A few scopes contain antiquotation features. For the sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. The following scopes are built-in. @@ -713,15 +713,15 @@ The following scopes are built-in. - :n:`self`: - + parses a Ltac2 expression at the current level and return it as is. + + parses a Ltac2 expression at the current level and returns it as is. - :n:`next`: - + parses a Ltac2 expression at the next level and return it as is. + + parses a Ltac2 expression at the next level and returns it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: - + parses a Ltac2 expression at the provided level :n:`n` and return it as is. + + parses a Ltac2 expression at the provided level :n:`n` and returns it as is. - :n:`thunk(@ltac2_scope)`: @@ -747,7 +747,7 @@ The following scopes are built-in. out of the parsed values in the same order. As an optimization, all subscopes of the form :n:`STRING` are left out of the returned tuple, instead of returning a useless unit value. It is forbidden for the various - subscopes to refer to the global entry using self or next. + subscopes to refer to the global entry using :n:`self` or :n:`next`. A few other specific scopes exist to handle Ltac1-like syntax, but their use is discouraged and they are thus not documented. @@ -758,9 +758,9 @@ planned. Notations ~~~~~~~~~ -The Ltac2 parser can be extended by syntactic notations. +The Ltac2 parser can be extended with syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -793,10 +793,10 @@ Abbreviations .. cmdv:: Ltac2 Notation @lident := @ltac2_term - This command introduces a special kind of notations, called abbreviations, + This command introduces a special kind of notation, called an abbreviation, that is designed so that it does not add any parsing rules. It is similar in spirit to Coq abbreviations, insofar as its main purpose is to give an - absolute name to a piece of pure syntax, which can be transparently referred + absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. The abbreviation can then be manipulated just as a normal Ltac2 definition, @@ -851,7 +851,7 @@ corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can -be done via an explicit annotation to the :n:`ltac1` quotation. +be done with an explicit annotation on the :n:`ltac1` quotation. .. productionlist:: coq ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) @@ -888,7 +888,7 @@ Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation instead. Note that the tactic expression is evaluated eagerly, if one wants to use it as -an argument to a Ltac1 function, she has to resort to the good old +an argument to a Ltac1 function, one has to resort to the good old :n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately and won't print anything. @@ -923,8 +923,8 @@ Due to conflicts, a few syntactic rules have changed. - The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`. - Levels of a few operators have been revised. Some tacticals now parse as if - they were a normal function, i.e. one has to put parentheses around the - argument when it is complex, e.g an abstraction. List of affected tacticals: + they were normal functions. Parentheses are now required around complex + arguments, such as abstractions. The tacticals affected are: :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`. - :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen, :n:`(fun () => ())` if you want a thunk (see next section), or use printing @@ -1010,4 +1010,4 @@ Exception catching Ltac2 features a proper exception-catching mechanism. For this reason, the Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it, has been removed. Now exceptions are preserved by all tacticals, and it is -your duty to catch them and reraise them depending on your use. +your duty to catch them and re-raise them as needed. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a561de1d0c..dcfe4a08f3 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -181,14 +181,12 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v - theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v @@ -516,7 +514,9 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Reals/Rdefinitions.v + theories/Reals/ConstructiveCauchyReals.v theories/Reals/Raxioms.v + theories/Reals/ConstructiveRIneq.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -561,6 +561,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v + theories/Reals/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 9f0a1942f9..eb86bab37e 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1020,6 +1020,37 @@ let apply_edit_file g edits = in List.rev (List.concat (List.map traverse prod)) + (* get the special tokens in the grammar *) +let print_special_tokens g = + let rec traverse set = function + | Sterm s -> + let c = s.[0] in + if (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') then set + else StringSet.add s set + | Snterm s -> set + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse set sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse (traverse set sym) sep + | Sparen sym_list -> traverse_prod set sym_list + | Sprod sym_list_list -> traverse_prods set sym_list_list + | Sedit _ + | Sedit2 _ -> set + and traverse_prod set prod = List.fold_left traverse set prod + and traverse_prods set prods = List.fold_left traverse_prod set prods + in + let spec_toks = List.fold_left (fun set b -> + let nt, prods = b in + traverse_prods set prods) + StringSet.empty (NTMap.bindings !g.map) + in + Printf.printf "Special tokens:"; + StringSet.iter (fun t -> Printf.printf " %s" t) spec_toks; + Printf.printf "\n\n" + (* get the transitive closure of a non-terminal excluding "stops" symbols. Preserve ordering to the extent possible *) (* todo: at the moment, the code doesn't use the ordering; consider switching to using @@ -1099,8 +1130,9 @@ let print_chunks g out fmt () = (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) -let start_symbols = ["vernac_toplevel"; "tactic_mode"] -let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *) +let start_symbols = ["vernac_toplevel"] +(* don't report tokens as undefined *) +let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ] let report_bad_nts g file = let rec get_nts refd defd bindings = @@ -1468,6 +1500,8 @@ let process_grammar args = print_in_order out g `MLG !g.order StringSet.empty; close_out out; finish_with_file (dir "fullGrammar") args.verify; + if args.verbose then + print_special_tokens g; if not args.fullGrammar then begin (* do shared edits *) |