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.
    <pexpect.pty_spawn.spawn object at 0x7fc8c8b1bc18>
    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: <class 'pexpect.exceptions.EOF'>
    match: None
    match_index: None
    exitstatus: None
    flag_eof: True
    pid: 11150
    child_fd: 5
    closed: False
    timeout: 30
    delimiter: <class 'pexpect.exceptions.EOF'>
    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 <clement.pitclaudel@live.com>

2 files changed, 57 insertions, 35 deletions

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):