diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/README.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 14 |
4 files changed, 18 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: |