diff options
| -rw-r--r-- | doc/README.md | 7 | ||||
| -rw-r--r-- | doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 114 |
5 files changed, 83 insertions, 79 deletions
diff --git a/doc/README.md b/doc/README.md index 99d285320d..79d1e1b756 100644 --- a/doc/README.md +++ b/doc/README.md @@ -28,10 +28,9 @@ Dependencies To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based -reference manual requires Python 3, and the following Python packages -(note the version constraints on Sphinx): +reference manual requires Python 3, and the following Python packages: - - sphinx >= 2.3.1 & < 3.0.0 + - sphinx >= 2.3.1 - sphinx_rtd_theme >= 0.4.3 - beautifulsoup4 >= 4.0.6 - antlr4-python3-runtime >= 4.7.1 @@ -41,7 +40,7 @@ reference manual requires Python 3, and the following Python packages To install them, you should first install pip and setuptools (for instance, with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: - pip3 install sphinx==2.3.1 sphinx_rtd_theme beautifulsoup4 \ + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \ antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex Nix users should get the correct development environment to build the diff --git a/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst new file mode 100644 index 0000000000..d17a2dff6b --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/13011-sphinx-3.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The reference manual can now build with Sphinx 3 + (`#13011 <https://github.com/coq/coq/pull/13011>`_, + fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, + by Théo Zimmermann and Jim Fehrle). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 070e899c9d..ba5bac6489 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -61,19 +61,23 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. -The syntax of the formulas is the following: +The syntax for formulas over :math:`\mathbb{Z}` is: - .. productionlist:: F - F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F - A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p - p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n + .. note the following is not an insertprodn -where :math:`F` is interpreted over either `Prop` or `bool`, -:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the -operators :math:`−, +, ×` are respectively subtraction, addition, and product; -:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. -For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of -rationals ``==``. + .. prodn:: + F ::= {| @A | P | True | False | @F /\\ @F | @F \\/ @F | @F <-> @F | @F -> @F | ~ @F | @F = @F } + A ::= {| @p = @p | @p > @p | @p < @p | @p >= @p | @p <= @p } + p ::= {| c | x | −@p | @p − @p | @p + @p | @p * @p | @p ^ n } + +where + + - :token:`F` is interpreted over either `Prop` or `bool` + - :n:`P` is an arbitrary proposition + - :n:`c` is a numeric constant of :math:`D` + - :n:`x` :math:`\in D` is a numeric variable + - :n:`−`, :n:`+` and :n:`*` are respectively subtraction, addition and product + - :n:`p ^ n` is exponentiation by a constant :math:`n` When :math:`F` is interpreted over `bool`, the boolean operators are `&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons @@ -81,6 +85,9 @@ in :math:`A` are also interpreted over the booleans (e.g., for :math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`, `Z.leb`). +For :math:`\mathbb{Q}`, use the equality of rationals ``==`` rather than +Leibniz equality ``=``. + For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the following expressions: diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b5618c5721..3d36c5c50f 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -196,12 +196,9 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition } - The optional order annotation follows the grammar: - - .. productionlist:: orderannot - order : measure `term` [ `term` ] | wf `term` `ident` + The optional :n:`@fixannot` annotation can be one of: + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on any subset of the arguments and the optional term diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2211a58e6e..99888cbe1d 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -59,9 +59,9 @@ specified, the default selector is used. .. _tactic_invocation_grammar: - .. productionlist:: sentence - tactic_invocation : `toplevel_selector` : `tactic`. - : `tactic`. + .. prodn:: + tactic_invocation ::= @toplevel_selector : @tactic. + | @tactic. .. todo: fully describe selectors. At the moment, ltac has a fairly complete description @@ -98,11 +98,11 @@ The general form of a term with a bindings list is .. _bindings_list_grammar: - .. productionlist:: bindings_list - ref : `ident` - : `num` - bindings_list : (`ref` := `term`) ... (`ref` := `term`) - : `term` ... `term` + .. prodn:: + ref ::= @ident + | @num + bindings_list ::= {+ (@ref := @term) } + | {+ @term } + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an :n:`@ident` or a :n:`@num`. The references are determined according to the type of @@ -137,30 +137,28 @@ introduced by tactics. They also let you split an introduced hypothesis into multiple hypotheses or subgoals. Common tactics that accept intro patterns include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. -.. productionlist:: coq - intropattern_list : `intropattern` ... `intropattern` - : `empty` - empty : - intropattern : * - : ** - : `simple_intropattern` - simple_intropattern : `simple_intropattern_closed` [ % `term` ... % `term` ] - simple_intropattern_closed : `naming_intropattern` - : _ - : `or_and_intropattern` - : `rewriting_intropattern` - : `injection_intropattern` - naming_intropattern : `ident` - : ? - : ?`ident` - or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] - : ( `simple_intropattern` , ... , `simple_intropattern` ) - : ( `simple_intropattern` & ... & `simple_intropattern` ) - rewriting_intropattern : -> - : <- - injection_intropattern : [= `intropattern_list` ] - or_and_intropattern_loc : `or_and_intropattern` - : `ident` +.. prodn:: + intropattern_list ::= {* @intropattern } + intropattern ::= * + | ** + | @simple_intropattern + simple_intropattern ::= @simple_intropattern_closed {* % @term0 } + simple_intropattern_closed ::= @naming_intropattern + | _ + | @or_and_intropattern + | @rewriting_intropattern + | @injection_intropattern + naming_intropattern ::= @ident + | ? + | ?@ident + or_and_intropattern ::= [ {*| @intropattern_list } ] + | ( {*, @simple_intropattern } ) + | ( {*& @simple_intropattern } ) + rewriting_intropattern ::= -> + | <- + injection_intropattern ::= [= @intropattern_list ] + or_and_intropattern_loc ::= @or_and_intropattern + | ident Note that the intro pattern syntax varies between tactics. Most tactics use :n:`@simple_intropattern` in the grammar. @@ -480,13 +478,13 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: coq - occurrence_clause : in `goal_occurrences` - goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] - : * |- [* [`at_occurrences`]] - : * - at_occurrences : at `occurrences` - occurrences : [-] `num` ... `num` + .. prodn:: + occurrence_clause ::= in @goal_occurrences + goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } } + | * |- {? * {? @at_occurrences } } + | * + at_occurrences ::= at @occurrences + occurrences ::= {? - } {* @num } The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate @@ -3975,15 +3973,15 @@ automatically created. the following. Beware, there is no operator precedence during parsing, one can check with :cmd:`Print HintDb` to verify the current cut expression: - .. productionlist:: regexp - regexp : `ident` (hint or instance identifier) - : _ (any hint) - : `regexp` | `regexp` (disjunction) - : `regexp` `regexp` (sequence) - : `regexp` * (Kleene star) - : emp (empty) - : eps (epsilon) - : ( `regexp` ) + .. prodn:: + regexp ::= @ident (hint or instance identifier) + | _ (any hint) + | @regexp | @regexp (disjunction) + | @regexp @regexp (sequence) + | @regexp * (Kleene star) + | emp (empty) + | eps (epsilon) + | ( @regexp ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of @@ -4672,17 +4670,15 @@ Automating tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are constructed over the following grammar: - .. _btauto_grammar: - - .. productionlist:: sentence - btauto_term : `ident` - : true - : false - : orb `btauto_term` `btauto_term` - : andb `btauto_term` `btauto_term` - : xorb `btauto_term` `btauto_term` - : negb `btauto_term` - : if `btauto_term` then `btauto_term` else `btauto_term` + .. prodn:: + btauto_term ::= @ident + | true + | false + | orb @btauto_term @btauto_term + | andb @btauto_term @btauto_term + | xorb @btauto_term @btauto_term + | negb @btauto_term + | if @btauto_term then @btauto_term else @btauto_term Whenever the formula supplied is not a tautology, it also provides a counter-example. |