Comments in the middle of the code are not accepted by ..rocqtop:: instructions in the sphinx documentation

[kyoDralliam]

Description of the problem

While writing documentation for the reference manual (cf this PR), I wanted to comment some part of a code snippet:

  .. rocqtop:: in

    Ltac2 Type rec 'a backtracking_stream :=
    [ EmptyStream(exn) (* Backtracking failure holding an exception *)
    | ConsStream('a, (exn -> 'a backtracking_stream)) (* Backtracking point with a value 'a as its head and a backtracking handler parameterized by an exception *)].

which yields the following error when building the manual:

$ dune build @refman-html                                                                                                                            
File "doc/dune", lines 25-44, characters 0-546:
25 | (rule
26 |  (targets
27 |   (dir refman-html))
....
42 |   (env_var COQRST_EXTRA))
43 |  (action
44 |   (run env sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))

Extension error:
.../coq/_build/default/doc/sphinx/proof-engine/ltac2.rst:478: Error while sending the following to coqtop:
    Ltac2 Type rec 'a backtracking_stream := [ EmptyStream(exn) (* Backtracking failure holding an exception *)
  coqtop output:
    Rocq < 
  Full error text:
    Timeout exceeded.
    <pexpect.pty_spawn.spawn object at 0x7df7131c6710>
    command: .../coq/_build/install/default/bin/coqtop
    args: [b'.../coq/_build/install/default/bin/coqtop', b'-q', b'-color', b'on']
    buffer (last 100 chars): 'Rocq < '
    before (last 100 chars): 'Rocq < '
    after: <class 'pexpect.exceptions.TIMEOUT'>
    match: None
    match_index: None
    exitstatus: None
    flag_eof: False
    pid: 1201850
    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[^< \r\n]+ < ')

Small Rocq / Coq file to reproduce the bug

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[jfehrle]

IIRC this is not easy to support, which is why it isn't supported.

[SkySkimmer]

The problem seems to be around the algorithm used to split into commands, cf

rocq/doc/tools/coqrst/coqdomain.py

Line 965 in c7e8528

def split_lines(source):

[kyoDralliam]

@jfehrle Thank you for adding support for comment in that PR. Do you remember the rationale for splitting lines after comment ends ?

[jfehrle]

The Python code uses regexes rather than a full parser. Getting it perfect seemed like overkill at the time. For example, as the code notes, nested comments are not supported--they are not regular expressions.