From 7cb49eda2c33c620f020cf7487ab9f53b74859da Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 14 Feb 2019 15:12:19 +0100 Subject: Sphinx: remove [coqtop:: undo] Co-authored-by: Vincent Laporte --- doc/tools/coqrst/coqdomain.py | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 0dd9b3aa3e..f9840dc19a 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,7 +560,7 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in undo + .. coqtop:: in reset Print nat. Definition a := 1. @@ -580,7 +580,6 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Reset state after executing. Not compatible with ``reset``. ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -829,20 +828,17 @@ class CoqtopBlocksTransform(Transform): @staticmethod def parse_options(options): """Parse options according to the description in CoqtopDirective.""" - opt_undo = 'undo' in options opt_reset = 'reset' 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', 'undo', 'all', 'none', 'in', 'out'))) + unexpected_options = list(set(options) - set(('reset', '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’") - elif opt_reset and opt_undo: - raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’") - return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none + return opt_reset, opt_input and not opt_none, opt_output and not opt_none @staticmethod def block_classes(should_show, contents=None): @@ -873,15 +869,13 @@ class CoqtopBlocksTransform(Transform): with CoqTop(color=True) as repl: for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): options = node['coqtop_options'] - opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options) + opt_reset, opt_input, opt_output = self.parse_options(options) if opt_reset: repl.sendone("Reset Initial.") pairs = [] for sentence in self.split_sentences(node.rawsource): pairs.append((sentence, repl.sendone(sentence))) - if opt_undo: - repl.sendone("Undo {}.".format(len(pairs))) dli = nodes.definition_list_item() for sentence, output in pairs: -- cgit v1.2.3 From f3db5a4006a3da598c4aa76adcf26729305b8dc5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Feb 2019 14:19:28 +0100 Subject: 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). --- doc/tools/coqrst/coqdomain.py | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'doc/tools') 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: -- cgit v1.2.3 From 7c4d6b904adb4a5d025ebcb804613f558e5b8be9 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 11 Feb 2019 12:50:03 +0100 Subject: Sphinx: nicer error reporting Example: add this to the first block in canonical-structures.rst: ~~~ Check nat. Check nat nat. ~~~ Output: ~~~ reading sources... [ 2%] addendum/canonical-structures Extension error: /home/gaetan/dev/coq/coq/doc/sphinx/addendum/canonical-structures.rst:43: Error while sending the following to coqtop: Check nat nat. coqtop output: Toplevel input, characters 6-13: > Check nat nat. > ^^^^^^^ Error: Illegal application (Non-functional construction): The expression "nat" of type "Set" cannot be applied to the term "nat" : "Set" Full error text: End Of File (EOF). Exception style platform. command: /home/gaetan/dev/coq/coq/bin/coqtop args: [b'/home/gaetan/dev/coq/coq/bin/coqtop', b'-boot', b'-color', b'on'] buffer (last 100 chars): '' before (last 100 chars): 'xpression "nat" of type "\x1b[33;1mSet\x1b[0m"\r\ncannot be applied to the term\r\n "nat" : "\x1b[33;1mSet\x1b[0m"\r\n' after: match: None match_index: None exitstatus: None flag_eof: True pid: 11150 child_fd: 5 closed: False timeout: 30 delimiter: logfile: None logfile_read: None logfile_send: None maxread: 2000 ignorecase: False searchwindowsize: None delaybeforesend: 0 delayafterclose: 0.1 delayafterterminate: 0.1 searcher: searcher_re: 0: re.compile('\r\n[^< ]+ < ') make[1]: *** [Makefile.doc:65: refman-html] Error 2 ~~~ Co-authored-by: Clément Pit-Claudel --- doc/tools/coqrst/coqdomain.py | 74 +++++++++++++++++++++++++---------------- doc/tools/coqrst/repl/coqtop.py | 18 ++++++---- 2 files changed, 57 insertions(+), 35 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index c9535bd2fc..791953eeaf 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -30,7 +30,7 @@ from sphinx import addnodes from sphinx.roles import XRefRole from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode -from sphinx.util.logging import getLogger +from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs @@ -38,7 +38,7 @@ from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors -from .repl.coqtop import CoqTop +from .repl.coqtop import CoqTop, CoqTopError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses @@ -864,6 +864,36 @@ class CoqtopBlocksTransform(Transform): blocks.append(re.sub("^", " ", output, flags=re.MULTILINE) + "\n") return '\n'.join(blocks) + def add_coq_output_1(self, repl, node): + options = node['coqtop_options'] + opt_reset, opt_fail, opt_input, opt_output = self.parse_options(options) + + pairs = [] + + if opt_reset: + repl.sendone("Reset Initial.") + repl.sendone("Set Coqtop Exit On Error.") + if opt_fail: + repl.sendone("Unset Coqtop Exit On Error.") + 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: + # Use Coqdoq to highlight input + in_chunks = highlight_using_coqdoc(sentence) + dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output)) + node.clear() + node.rawsource = self.make_rawsource(pairs, opt_input, opt_output) + node['classes'].extend(self.block_classes(opt_input or opt_output)) + node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset) + node += nodes.definition_list(node.rawsource, dli) + def add_coqtop_output(self): """Add coqtop's responses to a Sphinx AST @@ -871,33 +901,19 @@ class CoqtopBlocksTransform(Transform): 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_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: - # Use Coqdoq to highlight input - in_chunks = highlight_using_coqdoc(sentence) - dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output)) - node.clear() - node.rawsource = self.make_rawsource(pairs, opt_input, opt_output) - node['classes'].extend(self.block_classes(opt_input or opt_output)) - node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset) - node += nodes.definition_list(node.rawsource, dli) + try: + self.add_coq_output_1(repl, node) + except CoqTopError as err: + import textwrap + MSG = ("{}: Error while sending the following to coqtop:\n{}" + + "\n coqtop output:\n{}" + + "\n Full error text:\n{}") + indent = " " + loc = get_node_location(node) + le = textwrap.indent(str(err.last_sentence), indent) + bef = textwrap.indent(str(err.before), indent) + fe = textwrap.indent(str(err.err), indent) + raise ExtensionError(MSG.format(loc, le, bef, fe)) @staticmethod def merge_coqtop_classes(kept_node, discarded_node): diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3ff00eaaf3..6d65d30d46 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -20,6 +20,14 @@ import re import pexpect + +class CoqTopError(Exception): + def __init__(self, err, last_sentence, before): + super().__init__() + self.err = err + self.before = before + self.last_sentence = last_sentence + class CoqTop: """Create an instance of coqtop. @@ -63,7 +71,7 @@ class CoqTop: self.coqtop.kill(9) def next_prompt(self): - "Wait for the next coqtop prompt, and return the output preceeding it." + """Wait for the next coqtop prompt, and return the output preceeding it.""" self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10) return self.coqtop.before @@ -75,13 +83,11 @@ class CoqTop: """ # Suppress newlines, but not spaces: they are significant in notations sentence = re.sub(r"[\r\n]+", " ", sentence).strip() - self.coqtop.sendline(sentence) try: + self.coqtop.sendline(sentence) output = self.next_prompt() - except: - print("Error while sending the following sentence to coqtop: {}".format(sentence)) - raise - # print("Got {}".format(repr(output))) + except Exception as err: + raise CoqTopError(err, sentence, self.coqtop.before) return output def sendmany(*sentences): -- cgit v1.2.3 From 2e4e082637771bc047fbd977aaa5de26956c4618 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 14 Feb 2019 14:57:52 +0100 Subject: coqdomain.py fix typo in comment --- doc/tools/coqrst/coqdomain.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 791953eeaf..2d8bb43e62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -882,7 +882,7 @@ class CoqtopBlocksTransform(Transform): dli = nodes.definition_list_item() for sentence, output in pairs: - # Use Coqdoq to highlight input + # Use Coqdoc to highlight input in_chunks = highlight_using_coqdoc(sentence) dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) # Parse ANSI sequences to highlight output -- cgit v1.2.3 From ea8a9125a4e81e7c848cf53f1e34f534d359e832 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 16 Feb 2019 15:14:46 +0100 Subject: [sphinx] Add abort and restart options to directive coqtop. --- doc/tools/coqrst/coqdomain.py | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 2d8bb43e62..36b842d347 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -566,7 +566,7 @@ class CoqtopDirective(Directive): Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: @@ -580,7 +580,9 @@ 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 + - ``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) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -831,16 +833,18 @@ class CoqtopBlocksTransform(Transform): """Parse options according to the description in CoqtopDirective.""" opt_reset = 'reset' in options opt_fail = 'fail' in options + opt_restart = 'restart' in options + opt_abort = 'abort' 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', 'fail', 'all', 'none', 'in', 'out'))) + unexpected_options = list(set(options) - set(('reset', 'fail', 'restart', 'abort', '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_fail, opt_input and not opt_none, opt_output and not opt_none + return opt_reset, opt_fail, opt_restart, opt_abort, opt_input and not opt_none, opt_output and not opt_none @staticmethod def block_classes(should_show, contents=None): @@ -866,10 +870,12 @@ class CoqtopBlocksTransform(Transform): def add_coq_output_1(self, repl, node): options = node['coqtop_options'] - opt_reset, opt_fail, opt_input, opt_output = self.parse_options(options) + opt_reset, opt_fail, opt_restart, opt_abort, opt_input, opt_output = self.parse_options(options) pairs = [] + if opt_restart: + repl.sendone("Restart.") if opt_reset: repl.sendone("Reset Initial.") repl.sendone("Set Coqtop Exit On Error.") @@ -877,6 +883,8 @@ class CoqtopBlocksTransform(Transform): repl.sendone("Unset Coqtop Exit On Error.") for sentence in self.split_sentences(node.rawsource): pairs.append((sentence, repl.sendone(sentence))) + if opt_abort: + repl.sendone("Abort All.") if opt_fail: repl.sendone("Set Coqtop Exit On Error.") -- cgit v1.2.3 From 499491f8efd3a02dacb64c779edc246510b1d35f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 16 Feb 2019 16:42:52 +0100 Subject: [sphinx] Refactor handling of options for coqtop directive. Make it mandatory to give exactly one display option. --- doc/tools/coqrst/coqdomain.py | 72 ++++++++++++++++++++++++++----------------- 1 file changed, 44 insertions(+), 28 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 36b842d347..8df0f2be97 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -570,7 +570,7 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -589,8 +589,8 @@ class CoqtopDirective(Directive): reST source file). Use the ``reset`` option to reset Coq's state. """ has_content = True - required_arguments = 0 - optional_arguments = 1 + required_arguments = 1 + optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } directive_name = "coqtop" @@ -599,10 +599,8 @@ class CoqtopDirective(Directive): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - args = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in args: - args.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(args)), + args = self.arguments[0].split() + node = nodes.container(content, coqtop_options = set(args), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -829,22 +827,41 @@ class CoqtopBlocksTransform(Transform): return re.split(r"(?<=(?