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>

1 files changed, 12 insertions, 6 deletions

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