Sphinx: fail when a command fails

This uses a new coqtop-only option "Coqtop Exit On Error", not sure where
to put the doc for it. It being an option means we can locally turn it
off (.. coqtop:: fail).

5 files changed, 24 insertions, 4 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4f61824e67..a341cd9401 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -234,6 +234,7 @@ 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.
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 1b4d2315aa..eebf1f11e1 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -34,6 +34,11 @@ 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
+
+   This option, off by default, causes coqtop to exit with status code
+   ``1`` if a command produces an error instead of recovering from it.
+
 Batch compilation (coqc)
 ------------------------
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c134563efe..c1da1112c8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -602,7 +602,7 @@ Failing
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all fail
 
          Goal True.
          Proof. fail. Abort.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f9840dc19a..c9535bd2fc 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -580,6 +580,7 @@ class CoqtopDirective(Directive):
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
+      - ``fail``: Don't die if a command fails.
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
@@ -829,16 +830,17 @@ class CoqtopBlocksTransform(Transform):
     def parse_options(options):
         """Parse options according to the description in CoqtopDirective."""
         opt_reset = 'reset' in options
+        opt_fail = 'fail' in options
         opt_all, opt_none = 'all' in options, 'none' in options
         opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options
 
-        unexpected_options = list(set(options) - set(('reset', 'all', 'none', 'in', 'out')))
+        unexpected_options = list(set(options) - set(('reset', 'fail', 'all', 'none', 'in', 'out')))
         if unexpected_options:
             raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options))
         elif (opt_input or opt_output) and opt_none:
             raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’")
 
-        return opt_reset, opt_input and not opt_none, opt_output and not opt_none
+        return opt_reset, opt_fail, opt_input and not opt_none, opt_output and not opt_none
 
     @staticmethod
     def block_classes(should_show, contents=None):
@@ -867,15 +869,21 @@ class CoqtopBlocksTransform(Transform):
 
         Finds nodes to process using is_coqtop_block."""
         with CoqTop(color=True) as repl:
+            repl.sendone("Set Coqtop Exit On Error.")
             for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
                 options = node['coqtop_options']
-                opt_reset, opt_input, opt_output = self.parse_options(options)
+                opt_reset, opt_fail, opt_input, opt_output = self.parse_options(options)
 
                 if opt_reset:
                     repl.sendone("Reset Initial.")
+                    repl.sendone("Set Coqtop Exit On Error.")
+                if opt_fail:
+                    repl.sendone("Unset Coqtop Exit On Error.")
                 pairs = []
                 for sentence in self.split_sentences(node.rawsource):
                     pairs.append((sentence, repl.sendone(sentence)))
+                if opt_fail:
+                    repl.sendone("Set Coqtop Exit On Error.")
 
                 dli = nodes.definition_list_item()
                 for sentence, output in pairs:
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e933f08735..1094fc86b4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -366,6 +366,11 @@ let top_goal_print ~doc c oldp newp =
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
 
+let exit_on_error =
+  let open Goptions in
+  declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"]
+    ~value:false
+
 let rec vernac_loop ~state =
   let open CAst in
   let open Vernac.State in
@@ -410,6 +415,7 @@ let rec vernac_loop ~state =
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+    if exit_on_error () then exit 1;
     vernac_loop ~state
 
 let rec loop ~state =