diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 139 | ||||
| -rwxr-xr-x | doc/tools/coqrst/regen_readme.py | 15 | ||||
| -rw-r--r-- | doc/tools/coqrst/repl/coqtop.py | 23 |
3 files changed, 114 insertions, 63 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 067af954ad..8df0f2be97 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 @@ -560,17 +560,17 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in reset undo + .. coqtop:: in reset Print nat. 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: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -580,16 +580,17 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``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 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" @@ -598,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] @@ -828,22 +827,41 @@ class CoqtopBlocksTransform(Transform): return re.split(r"(?<=(?<!\.)\.)\s+", source) @staticmethod - def parse_options(options): + def parse_options(node): """Parse options according to the description in CoqtopDirective.""" - opt_undo = 'undo' in options + + options = node['coqtop_options'] + + # Behavior 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 + opt_fail = 'fail' in options + opt_restart = 'restart' in options + opt_abort = 'abort' in options + options = options - set(('reset', 'fail', 'restart', 'abort')) - unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out'))) + unexpected_options = list(options - set(('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 + loc = get_node_location(node) + raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) + + # Display options + if len(options) != 1: + loc = get_node_location(node) + raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) + + opt_all = 'all' in options + opt_none = 'none' in options + opt_input = 'in' in options + opt_output = 'out' in options + + return { + 'reset': opt_reset, + 'fail': opt_fail, + 'restart': opt_restart, + 'abort': opt_abort, + 'input': opt_input or opt_all, + 'output': opt_output or opt_all + } @staticmethod def block_classes(should_show, contents=None): @@ -867,36 +885,59 @@ 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 = self.parse_options(node) + + pairs = [] + + if options['restart']: + repl.sendone("Restart.") + if options['reset']: + repl.sendone("Reset Initial.") + repl.sendone("Set Coqtop Exit On Error.") + if options['fail']: + repl.sendone("Unset Coqtop Exit On Error.") + for sentence in self.split_sentences(node.rawsource): + pairs.append((sentence, repl.sendone(sentence))) + if options['abort']: + repl.sendone("Abort All.") + if options['fail']: + repl.sendone("Set Coqtop Exit On Error.") + + dli = nodes.definition_list_item() + for sentence, output in pairs: + # Use Coqdoc to highlight input + in_chunks = highlight_using_coqdoc(sentence) + dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + node.clear() + node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) + node['classes'].extend(self.block_classes(options['input'] or options['output'])) + node += nodes.inline('', '', classes=['coqtop-reset'] * options['reset']) + node += nodes.definition_list(node.rawsource, dli) + def add_coqtop_output(self): """Add coqtop's responses to a Sphinx AST 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_undo, 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: - # 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/regen_readme.py b/doc/tools/coqrst/regen_readme.py index e56882a521..0c15d7334c 100755 --- a/doc/tools/coqrst/regen_readme.py +++ b/doc/tools/coqrst/regen_readme.py @@ -10,6 +10,17 @@ SCRIPT_DIR = path.dirname(path.abspath(__file__)) if __name__ == "__main__" and __package__ is None: sys.path.append(path.dirname(SCRIPT_DIR)) +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +if len(sys.argv) == 1: + README_PATH = path.join(SPHINX_DIR, "README.rst") +elif len(sys.argv) == 2: + README_PATH = sys.argv[1] +else: + print ("usage: {} [FILE]".format(sys.argv[0])) + sys.exit(1) + import sphinx from coqrst import coqdomain @@ -23,10 +34,6 @@ def format_docstring(template, obj, *strs): strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) return template.format(*strs) -SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") -README_PATH = path.join(SPHINX_DIR, "README.rst") -README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") - def notation_symbol(d): return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3ff00eaaf3..ddba2edd4a 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. @@ -41,13 +49,10 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - BOOT = True - if os.getenv('COQBOOT') == "no": - BOOT = False self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) - self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color + self.args = (args or []) + ["-color", "on"] * color self.coqtop = None def __enter__(self): @@ -63,7 +68,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 +80,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): |