Merge PR #9654: [sphinx] Add warn option to coqtop directive.

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: vbgl
Reviewed-by: cpitclaudel

10 files changed, 81 insertions, 59 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index fac0035de1..881f7a310d 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -234,7 +234,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``fail``: Don't die if a command fails
+      - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both)
+      - ``warn``: Don't die if a command emits a warning
       - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
       - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 3e414a714c..a9d894cab5 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -313,7 +313,9 @@ constructor ``*``. It also tests that they work as expected.
 Unfortunately, these declarations are very verbose. In the following
 subsection we show how to make them more compact.
 
-.. coqtop:: all
+.. FIXME shouldn't warn
+
+.. coqtop:: all warn
 
   Module Add_instance_attempt.
 
@@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-.. coqtop:: all
+.. FIXME should not warn
+
+.. coqtop:: all warn
 
   Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
   
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index c1eab8a970..d1b95e6203 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``,
   single: ge (term)
   single: gt (term)
 
-.. coqtop:: in
+.. This emits a notation already used warning but it won't be shown to
+   the user.
+
+.. coqtop:: in warn
 
   Inductive le (n:nat) : nat -> Prop :=
   | le_n : le n n
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 9ab3f905e6..9bd41d79b7 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1023,7 +1023,7 @@ Mutually defined inductive types
 
    .. coqtop:: in
 
-      Variables A B : Set.
+      Parameters A B : Set.
 
       Inductive tree : Set := node : A -> forest -> tree
 
@@ -1533,7 +1533,7 @@ the following attributes names are recognized:
 
 .. example::
 
-   .. coqtop:: all reset
+   .. coqtop:: all reset warn
 
         From Coq Require Program.
         #[program] Definition one : nat := S _.
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 63d6a229ed..b629d15b11 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -33,7 +33,7 @@ example, revisiting the first example of the inversion documentation:
         | LeO : forall n:nat, Le 0 n
         | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
 
-   Variable P : nat -> nat -> Prop.
+   Parameter P : nat -> nat -> Prop.
 
    Goal forall n m:nat, Le (S n) m -> P n m.
 
@@ -69,7 +69,7 @@ as well in this case, e.g.:
 
 .. coqtop:: in
 
-   Variable Q : forall (n m : nat), Le n m -> Prop.
+   Parameter Q : forall (n m : nat), Le n m -> Prop.
    Goal forall n m (p : Le (S n) m), Q (S n) m p.
 
 .. coqtop:: all
@@ -124,7 +124,7 @@ the following example on vectors:
 
 .. coqtop:: in
 
-   Variable A : Set.
+   Parameter A : Set.
 
 .. coqtop:: in
 
@@ -329,7 +329,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Variable Ack : nat -> nat -> nat.
+      Parameter Ack : nat -> nat -> nat.
 
    .. coqtop:: in
 
@@ -357,7 +357,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Variable g : nat -> nat -> nat.
+      Parameter g : nat -> nat -> nat.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b81830f06b..b240cef40c 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2902,6 +2902,7 @@ pattern will be used to process its instance.
 
      Axiom P : nat -> Prop.
      Axioms eqn leqn : nat -> nat -> bool.
+     Declare Scope this_scope.
      Notation "a != b" := (eqn a b) (at level 70) : this_scope.
      Notation "a <= b" := (leqn a b) (at level 70) : this_scope.
      Open Scope this_scope.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index b5e9a902c6..7b395900e9 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -378,7 +378,7 @@ Examples:
 
       .. coqtop:: reset none
 
-         Variables (A : Prop) (B: nat -> Prop) (C: Prop).
+         Parameters (A : Prop) (B: nat -> Prop) (C: Prop).
 
       .. coqtop:: out
 
@@ -730,15 +730,15 @@ Applying theorems
 
    .. coqtop:: reset in
 
-      Variable R : nat -> nat -> Prop.
+      Parameter R : nat -> nat -> Prop.
 
-      Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
+      Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
 
-      Variables n m p : nat.
+      Parameters n m p : nat.
 
-      Hypothesis Rnm : R n m.
+      Axiom Rnm : R n m.
 
-      Hypothesis Rmp : R m p.
+      Axiom Rmp : R m p.
 
    Consider the goal ``(R n p)`` provable using the transitivity of ``R``:
 
@@ -3683,11 +3683,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       Local is useless since hints do not survive anyway to the closure of
       sections.
 
-   .. cmdv:: Local Hint @hint_definition
-
-      Idem for the core database.
-
-   .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}}
+   .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident
       :name: Hint Resolve
 
       This command adds :n:`simple apply @term` to the hint list with the head
@@ -3706,16 +3702,16 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       typical example of a hint that is used only by :tacn:`eauto` is a transitivity
       lemma.
 
-   .. exn:: @term cannot be used as a hint
+      .. exn:: @term cannot be used as a hint
 
-      The head symbol of the type of :n:`@term` is a bound variable such that
-      this tactic cannot be associated to a constant.
+         The head symbol of the type of :n:`@term` is a bound variable
+         such that this tactic cannot be associated to a constant.
 
-   .. cmdv:: Hint Resolve {+ @term}
+   .. cmdv:: Hint Resolve {+ @term} : @ident
 
       Adds each :n:`Hint Resolve @term`.
 
-   .. cmdv:: Hint Resolve -> @term
+   .. cmdv:: Hint Resolve -> @term : @ident
 
       Adds the left-to-right implication of an equivalence as a hint (informally
       the hint will be used as :n:`apply <- @term`, although as mentionned
@@ -3726,7 +3722,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
       Adds the right-to-left implication of an equivalence  as a hint.
 
-   .. cmdv:: Hint Immediate @term
+   .. cmdv:: Hint Immediate @term : @ident
       :name: Hint Immediate
 
       This command adds :n:`simple apply @term; trivial` to the hint list associated
@@ -3742,37 +3738,37 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. exn:: @term cannot be used as a hint
       :undocumented:
 
-   .. cmdv:: Immediate {+ @term}
+   .. cmdv:: Immediate {+ @term} : @ident
 
       Adds each :n:`Hint Immediate @term`.
 
-   .. cmdv:: Hint Constructors @ident
+   .. cmdv:: Hint Constructors @qualid : @ident
       :name: Hint Constructors
 
-      If :n:`@ident` is an inductive type, this command adds all its constructors as
+      If :token:`qualid` is an inductive type, this command adds all its constructors as
       hints of type ``Resolve``. Then, when the conclusion of current goal has the form
-      :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor.
+      :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor.
 
-   .. exn:: @ident is not an inductive type
-      :undocumented:
+      .. exn:: @qualid is not an inductive type
+         :undocumented:
 
-   .. cmdv:: Hint Constructors {+ @ident}
+   .. cmdv:: Hint Constructors {+ @qualid} : @ident
 
-      Adds each :n:`Hint Constructors @ident`.
+      Extends the previous command for several inductive types.
 
-   .. cmdv:: Hint Unfold @qualid
+   .. cmdv:: Hint Unfold @qualid : @ident
       :name: Hint Unfold
 
       This adds the tactic :n:`unfold @qualid` to the hint list that will only be
-      used when the head constant of the goal is :n:`@ident`.
+      used when the head constant of the goal is :token:`qualid`.
       Its cost is 4.
 
-   .. cmdv:: Hint Unfold {+ @ident}
+   .. cmdv:: Hint Unfold {+ @qualid}
 
-      Adds each :n:`Hint Unfold @ident`.
+      Extends the previous command for several defined constants.
 
-   .. cmdv:: Hint Transparent {+ @qualid}
-             Hint Opaque {+ @qualid}
+   .. cmdv:: Hint Transparent {+ @qualid} : @ident
+             Hint Opaque {+ @qualid} : @ident
       :name: Hint Transparent; Hint Opaque
 
       This adds transparency hints to the database, making :n:`@qualid`
@@ -3781,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-   .. cmdv:: Hint Variables %( Transparent %| Opaque %)
-             Hint Constants %( Transparent %| Opaque %)
+   .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident
+             Hint Constants %( Transparent %| Opaque %) : @ident
       :name: Hint Variables; Hint Constants
 
       This sets the transparency flag used during unification of
@@ -3790,7 +3786,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       overwritting the existing settings of opacity. It is advised
       to use this just after a :cmd:`Create HintDb` command.
 
-   .. cmdv:: Hint Extern @num {? @pattern} => @tactic
+   .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident
       :name: Hint Extern
 
       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
@@ -3801,7 +3797,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
          .. coqtop:: in
 
-            Hint Extern 4 (~(_ = _)) => discriminate.
+            Hint Extern 4 (~(_ = _)) => discriminate : core.
 
          Now, when the head of the goal is a disequality, ``auto`` will try
          discriminate if it does not manage to solve the goal with hints with a
@@ -3820,7 +3816,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
             Info 1 auto with eqdec.
 
-   .. cmdv:: Hint Cut @regexp
+   .. cmdv:: Hint Cut @regexp : @ident
       :name: Hint Cut
 
       .. warning::
@@ -3854,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
       initial cut expression being `emp`.
 
-   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident
       :name: Hint Mode
 
       This sets an optional mode of use of the identifier :n:`@qualid`. When
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 4f46a80dcf..e5eb7eb4f5 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1115,6 +1115,8 @@ Binding arguments of a constant to an interpretation scope
    .. coqtop:: all
 
       Parameter g : bool -> bool.
+      Declare Scope mybool_scope.
+
       Notation "@@" := true (only parsing) : bool_scope.
       Notation "@@" := false (only parsing): mybool_scope.
 
@@ -1151,6 +1153,7 @@ Binding types of arguments to an interpretation scope
    .. coqtop:: in reset
 
       Parameter U : Set.
+      Declare Scope U_scope.
       Bind Scope U_scope with U.
       Parameter Uplus : U -> U -> U.
       Parameter P : forall T:Set, T -> U -> Prop.
@@ -1575,7 +1578,7 @@ Numeral notations
 
      For example
 
-     .. coqtop:: all
+     .. coqtop:: all warn
 
         Check 90000.
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8df0f2be97..eaf1b2c2ad 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -580,7 +580,8 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``fail``: Don't die if a command fails
+      - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both)
+      - ``warn``: Don't die if a command emits a warning
       - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode)
       - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any)
 
@@ -835,11 +836,12 @@ class CoqtopBlocksTransform(Transform):
         # Behavior options
         opt_reset = 'reset' in options
         opt_fail = 'fail' in options
+        opt_warn = 'warn' in options
         opt_restart = 'restart' in options
         opt_abort = 'abort' in options
-        options = options - set(('reset', 'fail', 'restart', 'abort'))
+        options = options - {'reset', 'fail', 'warn', 'restart', 'abort'}
 
-        unexpected_options = list(options - set(('all', 'none', 'in', 'out')))
+        unexpected_options = list(options - {'all', 'none', 'in', 'out'})
         if unexpected_options:
             loc = get_node_location(node)
             raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options))
@@ -857,6 +859,9 @@ class CoqtopBlocksTransform(Transform):
         return {
             'reset': opt_reset,
             'fail': opt_fail,
+            # if errors are allowed, then warnings too
+            # and they should be displayed as warnings, not errors
+            'warn': opt_warn or opt_fail,
             'restart': opt_restart,
             'abort': opt_abort,
             'input': opt_input or opt_all,
@@ -891,18 +896,22 @@ class CoqtopBlocksTransform(Transform):
         pairs = []
 
         if options['restart']:
-            repl.sendone("Restart.")
+            repl.sendone('Restart.')
         if options['reset']:
-            repl.sendone("Reset Initial.")
-            repl.sendone("Set Coqtop Exit On Error.")
+            repl.sendone('Reset Initial.')
+            repl.send_initial_options()
         if options['fail']:
-            repl.sendone("Unset Coqtop Exit On Error.")
+            repl.sendone('Unset Coqtop Exit On Error.')
+        if options['warn']:
+            repl.sendone('Set Warnings "default".')
         for sentence in self.split_sentences(node.rawsource):
             pairs.append((sentence, repl.sendone(sentence)))
         if options['abort']:
-            repl.sendone("Abort All.")
+            repl.sendone('Abort All.')
         if options['fail']:
-            repl.sendone("Set Coqtop Exit On Error.")
+            repl.sendone('Set Coqtop Exit On Error.')
+        if options['warn']:
+            repl.sendone('Set Warnings "+default".')
 
         dli = nodes.definition_list_item()
         for sentence, output in pairs:
@@ -923,7 +932,7 @@ class CoqtopBlocksTransform(Transform):
 
         Finds nodes to process using is_coqtop_block."""
         with CoqTop(color=True) as repl:
-            repl.sendone("Set Coqtop Exit On Error.")
+            repl.send_initial_options()
             for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
                 try:
                     self.add_coq_output_1(repl, node)
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index ddba2edd4a..26f6255069 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -87,6 +87,11 @@ class CoqTop:
             raise CoqTopError(err, sentence, self.coqtop.before)
         return output
 
+    def send_initial_options(self):
+        """Options to send when starting the toplevel and after a Reset Initial."""
+        self.sendone('Set Coqtop Exit On Error.')
+        self.sendone('Set Warnings "+default".')
+
 def sendmany(*sentences):
     """A small demo: send each sentence in sentences and print the output"""
     with CoqTop() as coqtop: